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

摘要：

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

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

所属期刊栏目：37

分类号：N945.12(系统科学)

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

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

页数：共3页

页码：60-62