Abstract: In the practical operation environment of an enterprise, there generally exist multiple parallel working processes, thus having resource conflicts among them. It is very important to model and verify dynamically the consistency of temporal constraints of multi-process with resource conflicts. Based on real time model checking technique，a dynamic checking method of temporal constraints for multi-process of workflows is proposed. Multi-process of workflows is modeled by using a time automata, and the temporal constraints to be checked are transformed as the queries of observer time automata models. When temporal constraints are checked, the models are updated according to the known temporal information, and temporal constraints are checked. The method is practicable, because it not only can deal with the modeling and analyzing of multi-process with resource constraints, but also is flexible, namely when the temporal constraints are modified, the corresponding observer time automata is changed. Furthermore, there are some tools and software of real-time model checking to support it.

Key words: Dynamic checking, Multi-process, Real-time model checking, Temporal constraint, Time automata