Sidi Mohamed ben Abdellah University, Fez (MOROCCO)
CADP (Construction and Analysis of Distributed Processes)
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.
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.
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 VASY FTP site in PDF or PostScript
LIPI (Laboratoire d'Informatique et de Physique Interdisciplinaire)
Sidi Mohamed ben Abdellah University
B.P. 2202 - Route d'Imouzzer
|Further remarks:||This tool, amongst others, is described on the CADP Web Page: http://cadp.inria.fr|