[MR08b] Formal modelling and discrete-time analysis of BPEL web
Par Sylvain Rampacek le 2008 à 00h00
[MR08b] Radu Mateescu, Sylvain Rampacek. Formal modelling and discrete-time analysis of BPEL web. International Journal of Simulation and Process Modelling (IJSPM) (extended version), Vol. 4 (Issue 3/4), pp. 183-194, 2008.
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.
Keywords
Web services, formal specification, model checking, exhaustive simulation, process algebra.
