Paper 1
Stepwise development of formal models for web services compositions. Modelling and property verificationAuthors: Idir Ait-Sadoune and Yamine Ait-Ameur |
AbstractThe ability to compose existing services to provide more complex features is one of the main bene ts of Service Oriented Architec- ture (SOA). This services composition process, especially Web services, is generally de ned by a choreography or an orchestration of atomic services. These compositions are seen as a state transition system de- scribing the communication protocol between the participating services. The services description languages, expressing these compositions, su er from the lack of formal semantics and the ambiguities in the de nition of their constructors in the standards de ning these languages. The tools associated with these languages do not o er 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 veri cation 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 re nement to structure a BPEL develop- ment. 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. |