Process Model Validation - Transforming Process Models to Extended Checking Models

Process and workflow models are typical means to describe the dynamic activities of a system. Therefore, it is of high interest to validate these models. Many kinds of (business) rules, best practices, patterns, legal regulations may serve as specifications which the models have to fulfill. An already established technique to validate models of dynamic activities is inodel checking. In model checking the requirements are expressed by temporal logic. Temporal logic allows describing temporal dependencies. The models to be verified by model checkers are automata. In this context the question is how to transform process or workflow models into automata and how to specify the temporal logic in the way that the semantic of the process models is considered sufficiently. In our paper we present three approach to transform process models to checkable automata. We use the example of ARTS Event-driven Process Chains. In particular, the third approach introduces specializers enabling semantic-rich requirement specifications. This reduces the gap between process models (consisting of different model element types) and verification models.