期刊
JOURNAL OF SYSTEMS AND SOFTWARE
卷 180, 期 -, 页码 -出版社
ELSEVIER SCIENCE INC
DOI: 10.1016/j.jss.2021.111007
关键词
BPMN; Collaboration; Verification; Model checking; Statistical model checking
资金
- PRIN project SEDUCE [2017TWRCNB]
- PRIN project Fluidware [2017KRC7KT]
BPMN collaboration models are important but lack of effective verification capabilities may impact software quality. BProVe is a novel verification approach combining different model checking techniques, highlighting the importance and complementarity of supported verification strategies.
BPMN collaboration models have acquired increasing relevance in software development since they shorten the communication gap between domain experts and IT specialists and permit clarifying the characteristics of software systems needed to provide automatic support for the activities of complex organizations. Nonetheless, the lack of effective formal verification capabilities can hinder the full adoption of the BPMN standard by IT specialists, as it prevents precisely check the satisfaction of behavioral properties, with negative impacts on the quality of the software. To address these issues, this paper proposes BProVe, a novel verification approach for BPMN collaborations. This combines both standard model checking techniques, through the MAUDE's LTL model checker, and statistical model checking techniques, through the statistical analyzer MULTIVESTA. The latter makes BProVe effective also on those scenarios suffering from the state-space explosion problem, made even more acute by the presence of asynchronous message exchanges. To support the adoption of the BProVe approach, we propose a complete web-based tool-chain that allows for BPMN modeling, verification, and result exploration. The feasibility of BProVe has been validated both on synthetically-generated models and on models retrieved from two public repositories. The performed validation highlighted the importance and complementarity of the two supported verification strategies. (C) 2021 Elsevier Inc. All rights reserved.
作者
我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。
推荐
暂无数据