Formal Specification of Web Services Composition using LOTOS

Organisation:	Sidi Mohamed ben Abdellah University, Fez (MOROCCO)
Functionality:	Web Services.
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Period:	2016
Description:	The composition of Web services, that is the combination of several services to obtain new features, becomes more and more popular and present a necessary stage for the realization of the collaboration inter-companies (B2B). To implement this collaboration, a developer has to elaborate a specification which allows the modeling of the global behavior of the system, to verify formally this model to assure the quality of the system, then pass to the implementation of the composed service. Many languages, such as BPMN (Business Process Modeling Notation) and BPEL (Business Process Execution Language), have been proposed to specify and implement Web services composition. However, their lack of well-defined formal semantics does not support formal verification. As a consequence, the validation of Web service composition remains a complicated task. This work proposes an approach for specifying, verifying, and implementing Web services based on formal methods. The Web services to be composed are described using the MARDS model (Multi-Agent Reactive Decisional System) and the BPMN notation. This description is translated to LOTOS, then validated using the CADP tools, and finally implemented by generating BPEL executable code from the BPMN specification. The proposed approach is illustrated by the design and implementation of a composed Web service for travel organisation.
Conclusions:	Web services can be described conveniently using the BPMN notation, but this language is often criticized for its lack of formality. The proposed solution is based on transforming the BPMN model into a formal specification. The process algebra LOTOS has been selected as target language, due to the formal verification features provided by the CADP tools.
Publications:	[Adadi-Berrada-Chenouni-16] Nouha Adadi and Mohammed Berrada and Driss Chenouni. "Formal Specification of Web Services Composition Using LOTOS". International Journal of Computer Technology and Applications 7(5):636-642, September 2016. Available on line at: http://www.ijcta.com/documents/volumes/vol7issue5/ijcta2016070501.pdf or from the CADP Web site in PDF or PostScript [Adadi-Berrada-Chenouni-Bounabat-17] Nouha Adadi, Mohammed Berrada, Driss Chenouni, and Bouchaïb Bounabat. "Proposition of Web Services Composition Approach Basing of Model-Driven Approach and Multi-Agent Systems". Computer Modelling and New Technologies 21(3):12-19, February 2017. Available on line at: http://www.cmnt.lv/upload-files/ns_40art02_CMNT2103_Adadi.pdf or from the CADP Web site in PDF or PostScript
Contact:	Mohammed Berrada LIPI (Laboratoire d'Informatique et de Physique Interdisciplinaire) Sidi Mohamed ben Abdellah University B.P. 2202 - Route d'Imouzzer Fez MOROCCO Email: mohammed.berrada@gmail.com
Further remarks:	This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software

Back to the CADP research tools page