An approach to construct formal model of business process model from BPMN workflow patterns

The business process model is commonly created as a fundamental high level analysis model. The BPMN is one of the well known and widely used to represent the business process model. Recently, the BPMN workflow patterns are proposed as standardized business process model building blocks. The BPMN workflow patterns also provide the business analysts the common patterns of solutions to various workflow activities in practical way. The verification of BPMN workflow patterns is also essential to provide the better testing strategy in the software development. The infeasible path of the business process will be detected beforehand in the early stages of the software process. The formal model of business process will help either simulate the possible paths or verify the exhaustive search of the infeasible cases. However, the formal model is manually written and difficult to construct. In this paper, we propose an approach to construct formal model of business process model from given BPMN workflow patterns - basic control-flow patterns, and how to systematically generate the PROMELA. The BPMN control-flow patterns are extracted and translated into the PROMELA template. The resulting formal model in PROMELA is finally generated and correctly simulated in SPIN.