An Automated Framework for BPMN Model Verification Achieving Branch Coverage
Keywords:BPMN, colored Petri net, model checking, formal verification, software model
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.
Authors who publish with Engineering Journal agree to transfer all copyright rights in and to the above work to the Engineering Journal (EJ)'s Editorial Board so that EJ's Editorial Board shall have the right to publish the work for nonprofit use in any media or form. In return, authors retain: (1) all proprietary rights other than copyright; (2) re-use of all or part of the above paper in their other work; (3) right to reproduce or authorize others to reproduce the above paper for authors' personal use or for company use if the source and EJ's copyright notice is indicated, and if the reproduction is not made for the purpose of sale.