Description and Verification of Web Services using LOTOS and CADP

Organisation:	DIS - Universita di Roma "La Sapienza" (ITALY)
Method:	LOTOS
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Domain:	Web Services.
Period:	2004
Size:	about 700 lines of LOTOS
Description:	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.
Conclusions:	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.
Publications:	[Salaun-Ferrara-Chirichiello-04] 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
Contact:	Gwen Salaün INRIA Rhône-Alpes 655, avenue de l'Europe 38330 Montbonnot Saint-Martin FRANCE Tel: +33 (0)4 76 61 53 37 Fax: +33 (0)4 76 61 52 52 Email: Gwen.Salaun@inria.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