Contracts and Protocols for Web Services

Organisation:	University of Montréal (Canada)
Functionality:	Specifying and analyzing web service descriptions
Tools used:	CADP (Construction and Analysis of Distributed Processes) BPWS4J
Period:	2005
Description:	Web services are emerging as a key infrastructure for providing inter-operation between applications and systems and for providing support for the deployment of e-commerce business processes. One important issue for ensuring the growth of Web services is having ways of describing the available Web services in a precise way. One possible step towards providing semantic information for Web services is through the use of formal contract specifications based on pre/post-conditions. The use of pre/post-conditions, however, is not sufficient to describe the semantic of a group of related operations, for example, to describe the legal sequences in which these operations can/should be used. Although business process description languages like BPEL4WS or WSCI can express such descriptions, these are procedural descriptions, not necessarily appropriate for specification purpose. We present one possible way in which such descriptions could be provided for Web services, using path expressions that can show the order in which the various operations of a Web service can and should be invoked. The Web service descriptions extended with path expressions can be formally verified by developing a connection to a state-of-the-art verification toolbox such as CADP. This connection could work in the following way: Using the BPWS4J tool and its API, a business process P expressed in BPEL4WS is parsed and analyzed, and the various Web services used by P are identified. For each key service, the appropriate (slice of) flow of control within P is analyzed and an algebraic process model in LOTOS representing this flow is generated. The path expression describing the protocol of a service is translated into an appropriate regular alternation-free mu-calculus formula. Conformance of the abstract model of P with the service's protocol is then verified on the LOTOS description using the EVALUATOR model checker of CADP. Additionally, the Web service descriptions can be instrumented in order to achieve a run-time monitoring able to check dynamically the pre/post conditions of contracts.
Conclusions:	Existing formal specification and verification technology can provide a useful way of analyzing Web services, by developing appropriate connections between Web service description languages and process algebraic languages. The development of Web services could also benefit from the same kind of conceptual tools, such as contracts, available in other areas of software development.
Publications:	[Tremblay-Chae-05] Guy Tremblay and Junghyun Chae. "Toward Specifying Contracts and Protocols for Web Services". In Rachida Dssouli and Hadedh Mili, editors, Proceedings of the 1st Montréal Conference on e-Technologies MCeTech'2005 (Montréal, Canada), IEEE Computer Society Press, pp. 73-85, January 2005. Full version available on-line from http://www.info2.uqam.ca/~tremblay/TremblayCha05.pdf or from the CADP Web site in PDF or PostScript [Mili-Tremblay-Obaid-Tamrout-Caillot-05] Hafedh Mili, Guy Tremblay, Abdel Obaid, Radhouane Ben Tamrout, and Elisabeth Caillot. "Adding Semantics to Web Service Descriptions". Technical report, Université de Québec à Montréal, February 2005. Full version available from the CADP Web site in PDF or PostScript
Contact:	Guy Tremblay Dépt. d'informatique Université du Québec à Montréal C.P. 8888, Succ. Centre-Ville Montréal, QC, H3C 3P8, Canada Tel: (514) 987-3000, poste 8213 Fax: (514) 987-8477 Email: tremblay.guy@uqam.ca
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