【摘要】 工作流的属性规约语言需要具有高表达力以及基于状态和事件的推理能力。本文提出了一种时态逻辑规约语言E-CTL~*,该语言集成了状态和事件,能够精确和直觉地表示验证的属性。工作流的畅通性验证无论在时间上还是空间上代价都是非常高的,状态空间爆炸是验证的主要困难所在。利用E-CTL~*描述畅通性,可以使用存在的符号化模型检测工具验证畅通性,在一定程度上克服了状态爆炸问题。同时模型检测技术给出失效路径的优点可以引导我们纠正工作流的错误。工作流的变动需要具有正确性。从时态逻辑的角度讨论了变动正确性问题,得出了保持变动正确性的一般特征。更多还原

【Abstract】 Specification languages for workflow need to combine practical algorithmic efficiency with high expressive power and the ability to reason about both states and events. We address this question by defining a new temporal logic E-CTL~* which integrates both state-based and event-based properties and allows us to represent properties precisely and naturally. The verification of throughness of workflow logic is very expensive both in time and space. The state ex- plosion is the main difficulty. Describing the throughness by E-CTL~* allows us to use symbolic model checkers to veri- fy the thronghness. Therefore the state explosion can be overcame efficiently. When the throughness is not satisfied by the workflow, model checking can give a counterexample which can guide us to correct the workflow. The change of workflow needs to keep thronghness. We discuss the correctness of change based on temporal logic E-CTL~* and obtain the character of correct change.更多还原