Pattern-Based Model Checking for Dynamic Analysis of Workflow Processes with Temporal Constraints

The current fast-changing business environment requires workflow management systems to provide the ability of dynamic analysis when processes are edited or updated at both design time and execution time. In this paper, based on model checking we present a new approach of dynamic analysis on temporal properties after changes at design time and execution time. Our approach firstly records and analyzes the patterns by edit operations of processes. Secondly, the processes are automatically maintained by corresponding rules in UPPAAL. Finally, temporal constraints are checked by UPPAAL in background mode, and the results are reported to designers immediately. We apply the approach in a real business scenario to illustrate its advantages: practicable, flexible and efficient.