An Automated Framework for BPMN Model Verification Achieving Branch Coverage

Abstract

BPMN model is used in software development process that the procedural logics of software are described in term of graphical representation. Formal verification using colored Petri net (CPN) can be used to prove whether a designed BPMN model is frees of undesirable properties such as deadlock and unreachable task, and meets user requirements or not. Although there are many researches providing the transformation rules and frameworks for automating and verifying the CPN model, the CPN markings determination covering all execution paths is quite cumbersome. This paper proposes an automated BPMN verification framework that integrates the BPMN modeling tool and the CPN model checker together. The designed BPMN model is transformed into a CPN model and control flow graph (CFG). The CFG is used to create the execution paths and to find the interleaved activities. The interleaved activities are then considered for creating the CPN port places and markings by an applying of the branch coverage testing technique. Behaviors of the CPN model are analyzed by using a state space analysis based on the CPN model and automated markings. Our framework has been implemented as an Eclipse BPMN modeler plugin, and it is tested with the five case studies. The results show that our framework is practical. It can automate the CPN models from the BPMN model and guide the designers regarding the CPN markings determination to achieve branch coverage criteria.