基于时态逻辑的工作流分析

摘要

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