Abstract: The analysis of the correctness and rationality of a workflow model plays an important role in the research of the workflow techniques and successful implementation of the workflow management. The necessary timing constraints what should be considered in a workflow model are studied. Workflow nets are extended with time constraints as timing constraint workflow net (TCWF-net). After the model mapping method from a workflow model built by a graphic process modeling language extended with time information to a TCWF-net is proposed, the schedulability verification and synthesis of a TCWF-net is discussed in detail.

Key words: Model verification, Petri nets, Schedulability, Temporal dependency, Timing constraint, Workflow model