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.
Type de document :
Article dans une revue
International Journal of Simulation and Process Modelling, Inderscience, 2008, 〈10.1504/IJSPM.2008.023680〉
Liste complète des métadonnées

Littérature citée [29 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00381551
Contributeur : Radu Mateescu <>
Soumis le : mardi 5 mai 2009 - 17:58:02
Dernière modification le : jeudi 11 octobre 2018 - 08:48:03
Document(s) archivé(s) le : jeudi 30 juin 2011 - 11:26:17

Fichier

Mateescu-Rampacek-08-b.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

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〉

Partager

Métriques

Consultations de la notice

394

Téléchargements de fichiers

177