A formal approach to modeling and verification of business process collaborations

In the last years we are observing a growing interest in verification of business process models that, despite their lack of formal characterization, are widely adopted in industry and academia. To this aim, a formalization of the execution semantics of business process modeling languages is essential. In this paper, we focus on the OMG standard BPMN 2.0. Specifically, we provide a direct formalization of its semantics in terms of Labeled Transition Systems. This approach permits to avoid possible miss-interpretations, due to the usage of the natural language in the standard specification, and to overcome issues due to the mapping of BPMN to other formal languages, which are equipped with their own semantics. Our operational semantics is given for a relevant subset of BPMN elements focusing on the capability to model collaborations among organizations via message exchange. One of its distinctive aspects is the suitability to model business processes with arbitrary topology. This allows designers to freely specify their processes according to the reality, without the limitation of defining well-structured models. The provided formalization is also implemented by exploiting the capabilities of Maude. This implementation takes a collaboration model as an input and, explores all the model executions. By relying on it, automatic verification of properties related to collaborations has been carried out via the Maude model checker. We illustrate the benefits of our approach by means of a simple, yet realistic, running example concerning a travel booking scenario.