业务流程的形式化设计与验证

针对如何保证业务流程设计模型与业务需求的一致性问题，在研究有限自动机模型的基础上，提出了一种业务流程的自动机模型构建和验证方法.采用扩展的带约束条件的确定有限自动机对业务流程设计模型进行形式化描述，使用线性时序逻辑表示业务需求，分别给出业务流程设计模型到自动机模型和自动机模型到Promela描述的转换算法，并通过模型检测技术，使用Spin工具验证设计模型是否满足需求性质.若不满足性质，则能够获得反例执行的路径.实例分析表明，该方法可用于业务流程设计的正确性验证. 

Formal Design and Verification of Business Processes

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.