期刊
SCIENCE OF COMPUTER PROGRAMMING
卷 166, 期 -, 页码 35-70出版社
ELSEVIER SCIENCE BV
DOI: 10.1016/j.scico.2018.05.008
关键词
Business process modeling; BPMN collaboration; Operational semantics; Maude; Verification
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. (C) 2018 Elsevier B.V. All rights reserved.
作者
我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。
推荐
暂无数据