Verification and validation of BPEL processes. A proof and animation based approach

International audience; With the aim to provide a complete tool for the web services compositions validation, we have integrated various plugins in a single platform. This platform is based on the Eclipse core and contains the WSDL and BPEL editors plugins~(1), the BPEL2B (2) and B2EXPRESS (3) developed plugins and the various plugins of the RODIN platform (4). Different views are offered by this platform : WSDL and BPEL editors to describe different web services and their orchestration graphically or using the XML syntax, BPEL2B plugin to transform the WSDL/BPEL specifications onto Event-B models, the different plugins of RODIN to perform web services composition validation on the obtained Event-B model and the B2EXPRESS plugin to animate the obtained Event-B model.