Umeå University's logo

In complex information systems, it is often crucial to evaluate whether a sequence of activities obtained from a system log complies with behavioural rules. This process of evaluation is called conformance checking, and the most classical approach to specifying the behavioural rules is in the form of flow chartlike process diagrams, e.g., in the Business Process Model and Notation (BPMN) language. Traditionally, control flow constraints are extracted using Petri net replay-based approaches. Though, with the use of industrial process query languages such as Signavio Analytics Language (SIGNAL) that allows for temporal row matching, the possibility of performing conformance checking using temporal constraints opens up. To this end, this thesis presents a parser for extracting control-flow objects from BPMN-based business process models and a compiler for generating both linear temporal logic-like rules as well as SIGNAL queries. The parser succeeds at parsing all industry models and most academic models; the exceptions in the latter case can presumably be traced back to edge cases and unidiomatic modelling. The constraints generated by the compiler are in some, but not in all cases, identical to constraints extracted via Petri net replay as an intermediate step, indicating some differences in the formal interpretation of BPMN control flow. In conclusion, the implementation and evaluation of the parser and compiler indicate that it is feasible to move directly from business user-oriented process models to declarative, query language-based constraints, cutting out the Petri net-replay middleman and hence facilitating elegant and more efficient process data querying.