时序逻辑在有效性控制中的应用研究

Controling Validity Using Temporal Logic

工作流系统中的活动是与时间有着紧密联系的,如何保证恰当的活动在恰当时间被执行是工作流系统中的关键问题。探讨了如何利用时序逻辑来解决上述问题,提出了工作流系统中有效性的概念,给出了基于时序逻辑的有效性约束模型,并利用模型检测技术提供了验证有效性约束的方法,最后给出一个实例说明该方法的正确性。

The activities are closely related with time in workflow systems. How to guarantee that the activity is executed at a appropriate time has became the crucial problem in workflow systems. In this paper, temporal logic is used to solve this problem. Firstly, the concept of validity in workflow system is presented. Then it proposes a model of validity constraint based on temporal logic and the method to verify the validity constraint of the model. Finally, a instance is used for showing the validity of the method.