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

发布时间：2018-01-10 11:05

本文关键词：业务流程的形式化设计与验证　出处：《北京理工大学学报》2016年11期 　论文类型：期刊论文

【摘要】：针对如何保证业务流程设计模型与业务需求的一致性问题,在研究有限自动机模型的基础上,提出了一种业务流程的自动机模型构建和验证方法.采用扩展的带约束条件的确定有限自动机对业务流程设计模型进行形式化描述,使用线性时序逻辑表示业务需求,分别给出业务流程设计模型到自动机模型和自动机模型到Promela描述的转换算法,并通过模型检测技术,使用Spin工具验证设计模型是否满足需求性质.若不满足性质,则能够获得反例执行的路径.实例分析表明,该方法可用于业务流程设计的正确性验证.
[Abstract]:Aiming at how to ensure the consistency between the business process design model and the business requirements, the finite automata model is studied. In this paper, an automaton model construction and verification method for business process is proposed, and an extended deterministic finite automaton with constraints is used to formalize the business process design model. The business requirements are expressed by linear sequential logic, and the conversion algorithms from business process design model to automata model and automata model to Promela description are given respectively, and the model checking technology is adopted. The Spin tool is used to verify whether the design model satisfies the requirement property. If the property is not satisfied, the path of execution can be obtained. The example analysis shows that the method can be used to verify the correctness of business process design.
【作者单位】：西北大学信息科学与技术学院;中航工业西安航空计算技术研究所;西安电子科技大学计算机学院;
【基金】：国家自然科学基金资助项目(61502365,61272117) 中央高校基本科研业务费专项资金项目(K5051303005)
【分类号】：TP311.52
【正文快照】： 业务流程由存在于企业价值链条上的一系列活动及其之间的关系构成,是企业提高效率和增加效益的重要手段.为了增强业务流程的可靠性,保证设计结果的正确性,避免未经过有效验证的流程设计被开发、测试、甚至交付使用,造成返工修改,浪费大量的人力和物力,可应用形式化方法进行模

【相似文献】