Formal modelling and discrete-time analysis of BPEL web services. (10th March 2009)

• Record Type: Journal Article
• Authors: Mateescu, Radu; Rampacek, Sylvain
• Is Part Of: International journal of simulation and process modelling. Volume 4:Number 3/4(2008)
• Page Start: 183
• Page End: 194
• Publication Date: 2009-03-10
• Subjects: web services -- formal specification -- model checking -- exhaustive simulation -- process algebra -- formal modelling -- discrete-time analysis -- service oriented architecture -- SOA -- BPEL language -- BPEL semantics -- GPS navigation -- global positioning systems; Management -- Computer simulation -- Periodicals; Mathematical models -- Periodicals; Operations research -- Periodicals; Simulation methods -- Periodicals; 003.05
• Languages: English
• ISSNs: 1740-2123

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 modelling and analysis of web services described in the BPEL language. The discrete-time transition systems modelling the behaviour of BPEL descriptions are obtained by an exhaustive simulation based on a formalisation of BPEL semantics using the Algebra of Timed Processes (ATP). These models are then analysed 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.