A Correct-by-Construction Model for Verifying Transactional Composite Services Configuration

Reusability is a central concept of Web services as it allows for the construction of composite Web services at a lower cost/effort. Web services offer diverse functional capabilities (e.g., ticket purchase, hotel booking) and inherent transactional properties. However, due to the lack of an explicit and formal description of these functional and transactional perspectives, the correctness of the transactional reliability and functional properties cannot be verified. The composite Web service reliability is computed using a set of transactional requirements defined by designers throughout the Accepted Termination States (ATS) concept. The main objective of this article is to introduce a formal model of the Web service configuration and its correctness requirements that permit to ensure the correct Web service execution from functional and transactional points of view. For that purpose, we developed a Correct Configuration Model for Transactional Composite Services (CCM4TCS) using the Event-B method. This model is used to formally validate the consistency of composite Web service configuration’s properties and requirements. It allows also to check the correctness of ATS constraints that we use as reliability parameters. The correctness and the validation of our model are ensured by discharging proof obligations and by animating the specification using the ProB model-checker.