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

Abstract

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.

Cite this work

No public copy is stored for this record, so only the metadata is cited.

Stored only when both papers are in the corpus — 20 citations exist upstream.

Papers that cite the same references — the relational fallback while embeddings are still backfilling.