电子服务与工作流的形式验证

### 电子服务与工作流的形式验证 #### 1. 引言 电子服务的失败可能会产生巨大的影响。一个简单的电子服务也可能包含多个并发运行的进程，如库存管理、电子支付和在线促销等，这使得电子服务的设计过程变得越来越复杂。设计错误可能源于对共享数据的交错访问、进程间的同步、规范的动态变化，以及程序员对业务逻辑规范的误解和误读。因此，开发合适的工具来辅助电子服务规范的设计是一个有趣的问题。本文旨在研究和开发用于电子服务质量设计的通用验证技术。 与分析工作流系统性能模型的研究不同，本文的主要目标是验证工作流规范的逻辑正确性，例如数据的一致性、避免不安全的系统状态以及满足某些业务约束。工作流规范的验证问题已经在多个上下文中进行了研究，例如将模型检查应用于Mentor工作流规范、使用基于Petri网的结构进行验证等。然而，直接考虑结构和执行的验证更为准确和理想，这也是本文的主要关注点。 在早期验证Vortex规范的工作中，研究了两种不同的方法：一是用有限状态模型近似规范，并使用符号模型检查器（SMV）验证属性；二是用无限状态模型规范，并使用无限状态验证工具，如Action Verifier。但要使验证过程实用，还需要新的技术。 电子服务模型和决策流语言Vortex的一个主要区别是，新进程会根据不可预测的事件动态创建。本文的一个重点是研究针对这种动态进程实例化的验证技术。为此，提出使用pid量化约束来符号化表示可能无限数量的系统状态，并使用存在量词来推理进程ID。还开发了相应的算法来计算预条件（pre）运算符，这对模型检查中的不动点计算至关重要。 #### 2. 简单电子服务模型 为了便于研究验证问题，引入了一个简化的电子服务模型。该模型捕捉了大多数流行工作流系统的特征，同时又足够简单以进行形式验证。在这个模型中，允许进程的动态实例化、具有无限域的数据类型、并发进程间的共享全局变量以及灵活的进程间同步。 简单电子服务模型的正式定义如下：一个简单电子服务模式由固定数量的模块模式组成，这些模块模式可以通过访问全局变量相互通信。全局变量可以是布尔型、枚举型或整数型，整数型的域是无限的。在电子服务模式的执行过程中，模块模式可以动态地实例化多次，且实例化次数可能是无界的，这些实例称为模块实例或简称为进程。每个模块模式可以有固定数量的局部变量，局部变量也可以是布尔型、枚举型或整数型。如果每个进程的局部变量都有有限的域，则可以应用计数抽象来推理无界数量的进程。模块的逻辑由一系列转换规则定义，每个转换规则采用“if条件 then 动作”的形式。如果条件满足，则执行动作；否则，动作自动被阻止。动作可以是对变量的赋值的合取，也可以是实例化新进程的命令。由于模型检查器的限制，动作和条件中出现的表达式被限制为线性的。全局变量可以被所有进程访问，而局部变量只能被其所属进程访问。 以下是一个简单电子服务模型的示例： ```plaintext Global: Integer a=0; Module A ( Integer pcInit ) Integer pc=pcInit; Transition Rules: t1: if pc=0 then pc’=1 ∧ a’=a+1; EndModule Property: EF (a=2) Module main () Transition Rules: t2: new A (0); EndModule ``` 在这个示例中，有两个模块模式`main`和`A`。`main`模块中的转换规则`t2`实例化一个新的`A`类型的进程，并将其局部变量`pc`初始化为0。`A`模块模式中的转换规则`t1`将全局变量`a`加1，并将其局部变量`pc`推进到1。`t2`和`t1`的副本（由`A`的实例拥有）并行运行。显然，我们可以实例化超过两个`A`进程，并满足CTL属性`EF(a = 2)`（最终`a`将达到2）。 #### 3. 验证具有有限数量进程的系统 本部分讨论具有有限进程的工作流系统的验证。首先简要回顾模型检查技术和时态逻辑，然后介绍三种不同的方法（有限状态、无限状态模型检查和谓词抽象）来验证工作流规范，并展示基于系统特征开发的几种优化技术，最后比较这些方法的优缺点。 ##### 3.1 模型检查 Pnueli在一篇具有里程碑意义的论文中指出，时态逻辑对于指定程序（尤其是反应式系统）的正确性非常有用。时态逻辑具有表达“最终”和“始终”等概念的强大运算符，在指定随时间变化的行为方面优于Hoare逻辑。从70年代后期开始，出现了许多时态逻辑的变体，例如线性时态逻辑（LTL）和计算树逻辑（CTL）。在本文的其余部分，使用CTL及其扩展来指定工作流程序的期望属性。 在CTL公式中，时态运算符（如`X`（下一状态）、`F`（最终）和`G`（全局））必须紧跟路径量词`A`（对于所有路径）或`E`（存在一条路径）。例如，对于一个两进程系统，互斥属性可以表示为`AG¬(pc1=cs ∧ pc2=cs)`，进度属性可以表示为`AG(pc1=wait ⇒ AF(pc1=cs)) ∧ AG(pc2=wait ⇒ AF(pc2=cs))`。当进程数量未预先确定时，可以使用量词增强CTL，例如互斥属性可以表示为`AG(∀p1≠p2¬(pc[p1]=cs ∧ pc[p2]=cs))`。 模型检查技术有两种类型：显式状态模型检查和符号模型检查。在实践中，更倾向于使用符号模型检查，因为系统状态可以更紧凑地表示，从而可以验证更大的系统。对于有限状态系统，二进制决策图（BDD）是最流行的状态编码形式；对于无限状态系统，使用Presburger公式。 以下是CTL验证算法的简要回顾：假设一个工作流程序被正式建模为一个转换系统`T = (S, I, R)`，其中`S