6533b7defe1ef96bd127673a

RESEARCH PRODUCT

Formal Modeling and Discrete-Time Analysis of BPEL Web Services

Radu MateescuSylvain Rampacek

subject

Model checking[ INFO.INFO-MO ] Computer Science [cs]/Modeling and SimulationKnowledge representation and reasoningcomputer.internet_protocolComputer science0211 other engineering and technologies[INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE][ INFO.INFO-SE ] Computer Science [cs]/Software Engineering [cs.SE]02 engineering and technologycomputer.software_genre01 natural sciencesACM : D.: Software/D.2: SOFTWARE ENGINEERING/D.2.4: Software/Program Verification/D.2.4.3: Formal methodsFormal specificationACM: D.: Software/D.2: SOFTWARE ENGINEERING/D.2.4: Software/Program Verification/D.2.4.3: Formal methodsACM : D.: Software/D.2: SOFTWARE ENGINEERING/D.2.4: Software/Program Verification/D.2.4.4: Model checking0202 electrical engineering electronic engineering information engineeringTemporal logicEnterprise information systemFormal verification021103 operations researchDatabase010405 organic chemistrybusiness.industryApplied Mathematics020207 software engineeringService-oriented architectureSystems modeling[INFO.INFO-MO]Computer Science [cs]/Modeling and Simulation0104 chemical sciencesComputer Science ApplicationsACM: D.: Software/D.2: SOFTWARE ENGINEERING/D.2.4: Software/Program Verification/D.2.4.4: Model checkingBusiness Process Execution LanguageModeling and Simulation020201 artificial intelligence & image processingWeb serviceSoftware engineeringbusinesscomputer

description

International audience; 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.

yearjournalcountryeditionlanguage
2008-06-01
https://doi.org/10.1007/978-3-540-68644-6_13