基于Petri网的位置敏感工作流建模与正确性验证方法

摘要：

　　针对移动业务过程中对位置信息建模和分析的需求，结合目前已有的工作流建模方法，提出一种针对位置敏感工作流进行建模和正确性验证的方法。该模型以工作流网为基础，结合6种描述位置之间关系的原语，以位置约束的形式定义业务流程中的位置信息及其与活动之间的关系，然后基于Petri网的状态可达图得出对所建立模型进行正确性检查的方法。基于ProM平台开发了一个位置敏感工作流的建模工具，验证了所提建模方法的可行性和算法的正确性。

关键词： 工作流 信息建模 Petri网 形式验证

作者: 张力 赵炯 贾伟昊 刘英博

作者单位: 清华大学 软件学院,北京 100084 清华大学计算机科学与技术系,北京 100084

会议类型: 国内会议

会议名称: 第二届中国业务过程管理大会

会议地点: 北京

会议语种:中文

页码: 1747-1756

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