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

摘要：

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

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

所属期刊栏目：36

分类号：TP311(计算技术、计算机技术)

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

在线出版日期：2017-01-13（万方平台首次上网日期，不代表论文的发表时间）

页码：1147-1153