Verification of Web Service Composition

Organisation:	Université Technique de Belfort-Montbéliard (FRANCE)
Method:	LOTOS
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Domain:	Web Services.
Period:	2010
Size:	n/a
Description:	A Web service is provided by a collection of distributed components, each performing a specific task, that communicate with each other. The process of aggregating the necessary components and communication mechanisms is called Web service composition. Various methods have been proposed for specifying and implementing service composition, but most lack formal semantics and are therefore not directly suitable for formal analysis. This case study examines the use of LOTOS for specifying Web service composition, which is validated using CADP. As an example, the case study uses a field emergency response scenario, modeling the workflow patterns when an accident is reported and police and paramedics are notified. A high-level model of the scenario workflow is created in a UML activity. A detailed model is then created in LOTOS, including a process to correspond to each step in the activity diagram. Properties on the composition were defined in temporal logic, and verified on the LOTOS specification using the EVALUATOR model checker of CADP.
Conclusions:	This case study successfully demonstrates the use of LOTOS to specify a service composition expressed as a workflow, and the use of CADP to verify behavioural properties of the composition, expressed in temporal logic. This approach could be extended, enabling any business process modelling language to be translated to LOTOS.
Publications:	[Dumez-Bakhouya-Gaber-Wack-10] Christophe Dumez, Mohamed Bakhouya, Jaafar Gaber, and Maxime Wack. "Formal Specification and Verification of Service Composition using LOTOS". Proceedings of the 7th ACM International Conference on Pervasive Services ICPS'10. ACM Computer Society Press, July 2010. Available on-line from the CADP Web site in PDF or PostScript [Dumez-10] Christophe Dumez. "Approche dirigée par les modèles pour la spécification, la vérification formelle et la mise en oeuvre de services Web composés". PhD thesis, UTBM, France, August 2010. Available on-line at: http://hal.archives-ouvertes.fr/tel-00515130/ or from the CADP Web site in PDF or PostScript [Dumez-Bakhouya-Gaber-Wack-Lorenz-13] Christophe Dumez, Mohamed Bakhouya, Jaafar Gaber, Maxime Wack, and Pascal Lorenz. "Model-Driven Approach Supporting Formal Verification for Web Service Composition Protocols". Journal of Network and Computer Applications 34 (4), July 2013. Available on-line at: http://www.sciencedirect.com/science/article/pii/S1084804513000180
Contact:	Maxime Wack Laboratoire SeT Université Technique de Belfort-Montbéliard (UTBM) 90010 Belfort Cedex Tel: +33 (0)3 84 58 30 38 E-mail: Maxime.Wack@utbm.fr
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page