作者投稿和查稿 主编审稿 专家审稿 编委审稿 远程编辑

计算机工程 ›› 2011, Vol. 37 ›› Issue (23): 60-62. doi: 10.3969/j.issn.1000-3428.2011.23.020

• 软件技术与数据库 • 上一篇    下一篇

基于π演算的工作流模型检验

刘 峰,陈笑蓉   

  1. 刘峰,陈笑蓉
  • 收稿日期:2011-06-29 出版日期:2011-12-05 发布日期:2011-12-05
  • 作者简介:刘 峰(1980-),男,讲师,主研方向:软件工程形式化;陈笑蓉,教授
  • 基金资助:
    贵州省工业攻关计划基金资助项目(黔科合GY字[2010] 3077)

Workflow Model Checking Based on π Calculus

LIU Feng, CHEN Xiao-rong   

  1. LIU Feng, CHEN Xiao-rong
  • Received:2011-06-29 Online:2011-12-05 Published:2011-12-05

摘要: 为保证工作流模型语义的正确性,提出一种基于π演算的工作流模型语义性质检验方法。采用π演算的一个子集πN演算描述工作流模型,证明该模型的反应关系能够终止,构造有限反应迁移图算法,利用NuSMV检验工作流模型是否满足线性时序逻辑性质。实验结果证明了该检验方法的有效性。

关键词: π演算, 工作流模型, 模型检验, 时序逻辑

Abstract: In order to verify the semantic correctness of workflow model, a method to check semantic properties of workflow model using π calculus is presented. A subset of π calculus, named πN calculus, is adopted to formally describe workflow model. The termination of reaction relation of structure sound workflow model is proved. An algorithm for constructing finite reaction transfer diagram is presented. Then the model checker NuSMV is used to check whether a workflow model satisfies some semantic properties expressed as the character of linear sequential logic. Experimental results prove that this method is effective.

Key words: π calculus, workflow model, model checking, sequential logic

中图分类号: