Authors: Elie Fares, Jean-Paul Bodeveix, Mamoun Filali
Tags: 2011, conceptual modeling
Web services are increasingly becoming a major part of our daily lives. Many web services composition languages have been developed to describe the way a group of distributed web services interact with each other. In this matter, BPEL is one of the highly used composition languages. In this work, we are interested in verifying BPEL processes. Several works have addressed this issue before, but to our knowledge, a formalism that captures both the behavioral and the timing aspects of all the constructs of BPEL 2.0 does not exist. In this paper, we introduce a verification framework for timed BPEL models. We show how the relative and the absolute time of BPEL can be treated. We also give examples of temporal and timed properties that are supported in our framework. The verification is based on a transformation of all the BPEL constructs to the process algebra language, FIACRE.Read the full paper here: https://link.springer.com/chapter/10.1007/978-3-642-21759-3_19
