Formal Modeling and Discrete-Time Analysis of BPEL Web Services - Inria - Institut national de recherche en sciences et technologies du numérique Access content directly
Journal Articles International Journal of Simulation and Process Modelling Year : 2008

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.
Fichier principal
Vignette du fichier
Mateescu-Rampacek-08-b.pdf (450.51 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

inria-00381551 , version 1 (05-05-2009)

Identifiers

Cite

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

Altmetric

Share

Gmail Facebook X LinkedIn More