Formal approach for compliance rules checking in business process models

The business process models should comply with a set of rules describing the operations, policies and constraints that an organization must respect under financial authorities. However, the large number of rules and their frequency of changes make the traditionally used manual compliance checking a time-consuming task. As a result an automated compliance checking should be adopted. This paper proposes a formal approach for automated compliance checking. It proposes to map BPMN models directly to finite state machines (i.e., Kripke structures) and to express the compliance rules in a graphical language for better understandability. Subsequently, these are translated into linear temporal logic formulae for their integration. The compliance of business process models can be verified by means of model checking technology. The main goal is to increase the efficiency of the deployment of business process models while minimizing the risks and cost of the compliance inspection.