Sylvain Rampacek

Exposé lors du séminaire de l’équipe VASY de l’INRIA à Monthieux, du 10 au 13 Juin 2008 : « Formal Modeling and Discrete-Time Analysis of BPEL Web Services » (travail réalisé avec Radu Mateescu).

Résumé : 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.