Model Checking with Graphical Validation Rules

The assurance of quality and reliability of process models and workflows is essential for model driven software development. There are numerous ways to achieve these objectives. One is model checking, through which it can be verified that a model satisfies specific logical rules. The model to be checked is usually given as a finite state machine. Rules have to be specified at the level required by the model checker. In this paper, we develop a visual notation for logical rules at the level of processes and workflows. This enables the business process engineer to use model checking techniques and to produce higher quality business models for subsequent software development. The approach is demonstrated by validating event-driven process chains (EPCs).