Abstract: With the rapid development of Internet technology,the demand for business process modeling of complex system is increasing.In order to verify the correctness of the business process model with time constraints,this paper put forward a kind of graph decomposition algorithm based on node switching rules,which transforms the business process model into execution trace set and transforms the execution trace set to Prolog.That is to say,the trace of nodes,gateway and time constraints are all converted into Prolog fact.This paper put forward an algorithm that transforms the business process model to Prolog language and transforms the duration time pattern,cycle time pattern and fixed time pattern into Prolog rules,supporting the validation of the business process model on three time patterns.Finally,a medical process instance with time constraints was verified.

Key words: Time constraints,Time pattern,Business process model,Verification method