A Proof Based Approach for Modelling and VerifyingWeb Services Compositions

The Web services composition defines a process that involves various independent Web services to perform a complex function. This process is described with a standard language (BPEL) and executed by tools supporting this language. This kind of languages describes the behavior of different distributed services together, but it does not support the verification nor the validation of behavioral requirements.In our work, we are interested in the formal validation of Web services composition. Formal models are extracted from BPEL specifications and checked. Most previous work is based on Web services composition formalizations using Petri nets,process algebra or transition systems. The model checking technique is set-up to validate such descriptions.In this paper, we present a proof and refinement based approach for the formal representation, verification and validation of Web services compositions using the Event_B method.