This research project focuses on the formal analysis of BPMN models. Its main goal is to detect control and data flow errors as well as business rules violations in models conceived with the BPMN standard. The latter was not provided with a mathematical background, which limits the models analysis to informal approaches such as observation and inspection.
We based our contributions on three analysis axes:
- Control Flow Analysis: in this axis, we proposed a formal semantics of BPMN in terms of a mapping to Time Petri Nets (TPN). After the translation of BPMN models to TPN, the verification is done to ensure that some functional properties are satisfied by the model under investigation, namely liveness and reach ability properties. The main advantage of our approach is that it takes into account the time components in modeling Business process models;
- Data Flow Analysis: in this axis, we proposed an approach based on the Data Record concept. The latter suggests a method that locates the stage where thedata flow anomaly (missing, redundant, lost and inconsistent data) has taken place as well as the source of data flow problem. Therefore the designer can easily correct the anomaly in order to get the BPMN model free of data flow errors. The model’s data flow problems are detected using an algorithm specific for the BPMN standard;
- Business Rules Analysis: in this axis, we employ the Business Rule Language semantics. The latter proposes a new approach that uses Business Rule Language/Process Schema to express several common types of business rules that could be verified by a Depth First Search algorithm adapted for the BPMN standard.
All the contributions have been implemented in an Eclipse plugin called”BPMNP rocess analysis”.
Keywords : BPM, BPMN, V&V, TPN, Data Record, Data flow anti-patterns, Depth First Search, Business Rules Language, Eclipse Plugin.