Stepwise development of formal models for web services compositions: Modelling and property verification

Abstract

The ability to compose existing services to provide more complex features is one of the main benefits of Service Oriented Architecture (SOA). This services composition process, especially Web services, is generally defined by a choreography or an orchestration of atomic services. These compositions are seen as a state transition system describing the communication protocol between the participating services. The services description languages, expressing these compositions, suffer from the lack of formal semantics and the ambiguities in the definition of their constructors in the standards defining these languages. The tools associated with these languages do not offer the possibility to formally verify and validate the behaviour and the properties of the obtained composed service. Our work focuses on the formal modelling and verification of the web services composition described by the BPEL standard using the Event-B method. The proposed approach formalizes the static and the dynamic parts of BPEL, and uses the refinement to structure a BPEL development. The theorem-proving technique is set-up to verify the properties. A one-to-one link is guaranteed between BPEL elements and their Event-B formalization. This correspondence provides assistance for developers to improve the quality of the obtained BPEL process. This approach is implemented in the BPEL2B tool. © 2013 Springer-Verlag Berlin Heidelberg.