DIS - Universita di Roma "La Sapienza" (ITALY)
CADP (Construction and Analysis of Distributed Processes)
about 700 lines of LOTOS
Web services are distributed and independent pieces of code solving
specific tasks which communicate with each other by exchanging
messages. It is now becoming widely accepted that formal methods
provide an adequate framework to address many issues raised in the web
services area. Process algebras are especially suitable
to describe, compose and reason on web services at an abstract level.
This case-study shows that LOTOS and CADP provide powerful means to describe and reason on web services. Indeed, LOTOS makes it possible to specify dynamic behaviours, but also data descriptions, allowing a much finer (less abstract) level of specification, which is clearly needed in some cases. This was illustrated on several examples, such as a negotiation problem in which both data and dynamic aspects have to be dealt with. Negotiation issues appear when several participants (customers and providers) have to interact in order to reach an agreement that is beneficial to all of them. In addition, some guidelines were defined to encode abstract specifications of services written using LOTOS into executable web services implemented with the business process execution language BPEL.
To ensure trustworthy negotiation steps, the LOTOS specification of web services is analysed using tools of the CADP toolbox, in particular OCIS for interactive simulation and EVALUATOR for model checking safety and liveness properties.
This work shows that LOTOS and CADP can be used to specify and verify
within reasonable amounts of time (tens of minutes) realistic
configurations studies of web services, involving in the case of
negotiation among many customers and providers.
Gwen Salaün, Andrea Ferrara, and Antonella Chirichiello.
"Negotiation among Web Services using LOTOS/CADP." In Liang-Jie Zhang
(editor), Proceedings of the European Conference on Web Services
ECOWS'04 (Erfurt, Germany), Lecture Notes in Computer Science,
vol. 3250, pp. 198-212, Springer Verlag, September 2004.
Available from the CADP Web site in PDF or PostScript
[Chirichiello-Salaun-05] Antonella Chirichiello and Gwen SalaŁn. "Encoding Abstract Descriptions into Executable Web Services: Towards a Formal Development Negotiation among Web Services using LOTOS/CADP." In Proceedings of the 2005 IEEE/WIC/ACM International Conference on Web Intelligence WI'2005 (CompiŤgne, France), September 2005.
Available on-line from http://cadp.inria.fr/publications/Chirichiello-Salaun-05.html
655, avenue de l'Europe
38330 Montbonnot Saint-Martin
Tel: +33 (0)4 76 61 53 37
Fax: +33 (0)4 76 61 52 52
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|