Title: Formal modelling and discrete-time analysis of BPEL web services

Authors: Radu Mateescu, Sylvain Rampacek

Addresses: INRIA/VASY project-team, Centre de Recherche Grenoble – Rhone-Alpes, 655, avenue de l'Europe, Montbonnot, F-38334, Saint Ismier Cedex, France. ' LE2I, Faculte des Sciences Mirande, Aile de l'Ingenieur, Universite de Bourgogne, BP 47870, F-21078 Dijon Cedex, France

Abstract: Web services are increasingly used for building enterprise information systems according to the Service Oriented Architecture (SOA) paradigm. We propose in this paper a tool-equipped methodology allowing the formal modelling and analysis of web services described in the BPEL language. The discrete-time transition systems modelling the behaviour of BPEL descriptions are obtained by an exhaustive simulation based on a formalisation of BPEL semantics using the Algebra of Timed Processes (ATP). These models are then analysed by model checking value-based temporal logic properties using the CADP toolbox. The approach is illustrated with the design of a web service for GPS navigation.

Keywords: web services; formal specification; model checking; exhaustive simulation; process algebra; formal modelling; discrete-time analysis; service oriented architecture; SOA; BPEL language; BPEL semantics; GPS navigation; global positioning systems.

DOI: 10.1504/IJSPM.2008.023680

International Journal of Simulation and Process Modelling, 2008 Vol.4 No.3/4, pp.183 - 194

Published online: 07 Mar 2009 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article