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.
International Journal of Simulation and Process Modelling, 2008 Vol.4 No.3/4, pp.183 - 194
Available online: 07 Mar 2009 *Full-text access for editors Access for subscribers Purchase this article Comment on this article