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

Workflow Model Checking Based on π Calculus

为保证工作流模型语义的正确性,提出一种基于π演算的工作流模型语义性质检验方法。采用π演算的一个子集π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.