Skip to Main content Skip to Navigation
Journal articles

Formal Modeling and Discrete-Time Analysis of BPEL Web Services

Radu Mateescu 1 Sylvain Rampacek 2
1 VASY - System validation - Research and applications
Inria Grenoble - Rhône-Alpes, LIG [2007-2015] - Laboratoire d'Informatique de Grenoble [2007-2015]
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 modeling and analysis of Web services described in the BPEL language. The discrete-time transition systems modeling the behavior of BPEL descriptions are obtained by an exhaustive simulation based on a formalization of BPEL semantics using the Algebra of Timed Processes (ATP). These models are then analyzed 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.
Document type :
Journal articles
Complete list of metadatas

Cited literature [29 references]  Display  Hide  Download
Contributor : Radu Mateescu <>
Submitted on : Tuesday, May 5, 2009 - 5:58:02 PM
Last modification on : Friday, July 17, 2020 - 2:54:04 PM
Long-term archiving on: : Thursday, June 30, 2011 - 11:26:17 AM


Files produced by the author(s)



Radu Mateescu, Sylvain Rampacek. Formal Modeling and Discrete-Time Analysis of BPEL Web Services. International Journal of Simulation and Process Modelling, Inderscience, 2008, ⟨10.1504/IJSPM.2008.023680⟩. ⟨inria-00381551⟩



Record views


Files downloads