定时CSP与Object-Z的融合及应用

# 定时CSP与Object - Z的融合及应用 ## 1. 定时失效模型与属性验证 在定时系统的研究中，对于像电梯系统这样的复杂系统，我们可以使用定时失效模型来解释和分析Object - Z组件。在这个模型中，未定时事件的启用对应着定时框架中的最终提供，即它可能不会立即提供，但不会永远被拒绝。例如，`WAIT t3; SetTarget → STOP` 这个定时进程与未定时进程 `SetTarget → STOP` 是一致的。 ### 1.1 可验证的属性类型 对于集成的Object - Z/定时CSP规范，我们可以验证至少三种类型的属性： - 未定时属性：与时间无关的属性。 - 定时轨迹属性：关于事件发生顺序和时间的属性。 - 定时失效属性：涉及事件拒绝和发生情况的属性。 这些属性可以用定时失效的谓词来表示，使用CSP中熟悉的符号 `P sat S(s, ℵ)`，表示对于所有 `(s, ℵ) ∈ TF[[P]]`，`S(s, ℵ)` 都成立。对于形式为 `P∥C` 的集成规范，我们可以按组件验证属性，使用以下规则： ```plaintext P sat S1(s, ℵ) C sat S2(s, ℵ) P∥C sat ∃ℵ1, ℵ2 • S1(s, ℵ1) ∧ S2(s, ℵ2) ∧ ℵ = ℵ1 ∪ ℵ2 ``` ### 1.2 属性的翻译 未定时属性可以通过一定的规则转换为定时解释。例如，如果Object - Z组件 `C` 满足基于轨迹的属性 `C sat S(tr)`，那么该属性可以转换为定时解释 `[[C]]t sat #s < ∞ ⇒ S(strip(s))`。同样，基于轨迹和失效的属性也可以进行转换。 ### 1.3 具体属性验证示例 - **电梯门开闭交替属性**：可以表示为 `TLiftSys sat s ↓{Close} ≤ s ↓{Open} ≤ s ↓{Close} + 1`，通过验证 `Lift sat s ↓{Close} ≤ s ↓{Open} ≤ s ↓{Close}+1` 来证明。 - **外部目标设置时间限制属性**：`s = ⟨⟩ ⇒ SetTarget ∈ σ(ℵ|↾t3)`，`Lift` 和 `Con` 组件不满足该属性，但 `TOrder` 组件满足，因此整个同步过程也满足。 - **目标设置后关门可用性属性**：`door open(s) ∧ got target(s) ⇒ (Close ̸ ∈ σ(ℵ↿(end(s ↾InternalTarget) + t5)) ∨ Close ̸ ∈ σ(ℵ↿(end(s ↾SetTarget) + t5)))`，虽然 `Lift` 组件可能不满足，但整个规范仍然满足该属性。 ## 2. 精化 在CSP中，精化是根据失效和发散来定义的。对于集成的Object - Z和CSP规范，我们可以使用状态模拟来进行组件级的精化。当结合定时CSP和Object - Z时，我们关心的是Object - Z组件的状态精化是否意味着定时失效精化。 ### 2.1 精化的定义 在CSP中，如果 `failures C ⊆ failures A` 且 `divergences C ⊆ divergences A`，则 `C` 是 `A` 的精化。对于Object - Z组件，由于其发散为空，我们只需要考虑失效。 ### 2.2 定时失效精化的证明 假设进程 `P2` 是 `P1` 的失效 - 发散精化，我们要证明 `[[P2]]f ⊆ [[P1]]f`。对于有限的失效情况，我们可以通过分析轨迹和失效集合来证明。例如，对于失效 `(s, ℵ) = (s, [t, ∞) × X )`，因为 `F[[P2]] ⊆ F[[P1]]`，所以 `X ∈ F[[P1]]`，进而可以得出 `(s, ℵ) ∈ [[P1]]f`。 ### 2.3 精化的意义 这意味着我们可以使用标准的状态模拟方法来精化Object - Z组件，并且知道它们的定时解释也是相互精化的。 ## 3. 两事件模型 在CSP和Object - Z的标准假设中，事件和操作是瞬时的，但在定时上下文中，我们有时需要考虑操作的持续时间。两事件模型是处理操作和事件持续时间的一种简单方法。 ##