工作流时序约束模型分析与验证方法

为了解决工作流时间建模与时序一致性验证问题,以时序逻辑和模型检查为基础,提出了一种工作流时间建模与时序一致性验证方法.该方法用一阶逻辑描述工作流模型及其时间信息,用时序逻辑描述工作流的时序约束,用模型检查算法对时序约束进行验证与分析.该方法不是针对某一种时序约束提出来的,而是能够验证任何用时序逻辑描述的工作流时序约束.该方法还能够对未通过验证的时序约束提供工作流运行实例作为反例,帮助用户定位模型的问题.以一个工作流时间建模和时序一致性验证的实例证实了所提出方法的有效性.

A Method of Time Constraint Workflow Model Analysis and Verification

In order to describe the temporal aspect of workflow model and verify the temporal consistency,a method based on temporal logic and model checking for modeling and verifying time constraint workflows is presented.By this method,the first order logic is used to model workflow including its basic temporal information, temporal logic is used to model the time constraints,and model checking is used to analyze and verify the temporal consistency.The method can be used to verify any time constraints that can be described by temporal logic.Also the method can offer a counterexample of workflow instance to the time constraint which can not pass the verification. Finally,the method is validated through a case study.