Design of a BPEL verification tool

Abstract

The objective of this paper is to define a formal framework for expressing a BPEL transformation based semantics of BPEL constructs. Our main contribution is twofold. First, the transformation patterns are specified in a language close to the target's realtime verification language FIACRE. Since they are expressed at the level of the concrete syntax, with respect to the tool designer, they are formal and better readable than if they were expressed at the abstract syntax level. Second, the transformation automatically produces a structured model in the form of an abstract syntax tree. This is achieved by using the language Camlp4 that allows us to define meta extensions to the targeted specification language which in turn supports the expression of transformation patterns. Furthermore, thanks to the use of FIACRE, we get a model checking-based verification support. © 2012 Springer-Verlag.