HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

Formal Modeling and Discrete-Time Analysis of BPEL Web Services

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 :
Conference papers
Complete list of metadata

Cited literature [27 references]  Display  Hide  Download

Contributor : Radu Mateescu Connect in order to contact the contributor
Submitted on : Friday, September 5, 2008 - 4:01:47 PM
Last modification on : Friday, May 20, 2022 - 9:06:04 AM
Long-term archiving on: : Tuesday, June 28, 2011 - 4:31:33 PM


Files produced by the author(s)



Radu Mateescu, Sylvain Rampacek. Formal Modeling and Discrete-Time Analysis of BPEL Web Services. EOMAS 2008, Jun 2008, Montpellier, France. pp.179-193, ⟨10.1007/978-3-540-68644-6_13⟩. ⟨inria-00319100⟩



Record views


Files downloads