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

Formal Design and Verification of Business Processes

作　　者：丁明[1,2] 张书玲[1] 张琛[3] 

机构地区：[1]西北大学信息科学与技术学院,陕西西安710127 [2]中航工业西安航空计算技术研究所,陕西西安710119 [3]西安电子科技大学计算机学院,陕西西安710071

出　　处：《北京理工大学学报》2016年第11期1147-1153,共7页Transactions of Beijing Institute of Technology

基　　金：国家自然科学基金资助项目(61502365;61272117);中央高校基本科研业务费专项资金项目(K5051303005)

摘　　要：针对如何保证业务流程设计模型与业务需求的一致性问题,在研究有限自动机模型的基础上,提出了一种业务流程的自动机模型构建和验证方法.采用扩展的带约束条件的确定有限自动机对业务流程设计模型进行形式化描述,使用线性时序逻辑表示业务需求,分别给出业务流程设计模型到自动机模型和自动机模型到Promela描述的转换算法,并通过模型检测技术,使用Spin工具验证设计模型是否满足需求性质.若不满足性质,则能够获得反例执行的路径.实例分析表明,该方法可用于业务流程设计的正确性验证.To ensure the consistency of business process design models and business requirements,based on the researches on finite automata model,aquantitative 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.

关 键 词：业务流程 确定有限自动机 模型检测 线性时序逻辑 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]