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

Workflow Model Checking Based on π Calculus

作　　者：刘峰[1] 陈笑蓉[1] 

机构地区：[1]贵州大学计算机科学与信息学院,贵阳550025

出　　处：《计算机工程》2011年第23期60-62,共3页Computer Engineering

基　　金：贵州省工业攻关计划基金资助项目(黔科合GY字[2010]3077)

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

关 键 词：Π演算 工作流模型 模型检验 时序逻辑 

分 类 号：N945.12[自然科学总论—系统科学]