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 benets of Service Oriented Architec- ture (SOA). This services composition process, especially Web services, is generally dened 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, suer from the lack of formal semantics and the ambiguities in the denition of their constructors in the standards dening these languages. The tools associated with these languages do not oer 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 verication 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 renement 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. |