Université Technique de Belfort-Montbéliard (FRANCE)
CADP (Construction and Analysis of Distributed Processes)
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.
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.
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
Université Technique de Belfort-Montbéliard (UTBM)
90010 Belfort Cedex
Tel: +33 (0)3 84 58 30 38
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|