Abstract: To ensure the consistency of business process design models and business requirements, based on the researches on finite automata model, a quantitative method was proposed in this paper to deal with the construction and verification of business process models. First, the extended conditioned deterministic finite automata were used to describe business process design models and linear temporal logic was used to represent business requirements. Furthermore, the algorithms for transforming the business process design models into automata models and the automata model into Promela were presented. Finally, based on the model checking method, the consistency of the design models and properties were verified with the Spin, if the system models could not satisfy the property, a counter-example and the execution path could be found. Experimental results show that the proposed method is useful in ensuring the correctness of business process design.