Formal Transaction Modeling and Verification for an Adaptable Web Service Orchestration

The integrity of Web service orchestration is one of the most relevant characters in the development of compositions. Particularly, transactions that include a set of activities which are performed by partner services. However, due to the complexity of these activities, several failures can occur during the execution leading to violate transactional properties. Therefore, the selfadaptive behavior is a feature which designers need to include in their orchestration process in order to improve the reliability of these properties. In this paper, we propose a development process of adaptable transactional Web services that makes use of Colored Petri Net (CPN) formalism to model Web service orchestration under adaptive transaction constraints, ASK-Computational Tree Logic (ASK-CTL) is used to formally define transactions properties; and Model Checking technique, that is available in the software CPN Tools, is used to verify the defined properties. An example of a bookstore process is given to illustrate our proposal.