事件-B规范推理工具：GeneSyst解析

# 事件-B 规范推理工具：GeneSyst 解析 ## 1. 活性保存证明义务与迹的定义 在相关系统中，通常需要进行活性保存的证明义务。若系统 S 包含 m 个事件，其精化系统 R 包含 p 个新事件，那么存在如下关系： \[I \land J \Rightarrow (\bigwedge_{i = 1}^{m} Guard(e_{S_{i}}) \Rightarrow (\bigwedge_{i = 1}^{m} Guard(e_{R_{i}}) \lor \bigvee_{i = 1}^{p} Guard(ne_{R_{i}})))\] 精化相关的迹的定义与系统的迹定义方式相同。 ## 2. 符号化标记迁移系统 ### 2.1 符号化迁移系统的定义 符号化标记迁移系统（Symbolic Labelled Transition System，SLTS）是一个四元组 \((N, Init, U, W)\)，具体含义如下： - \(N\) 是状态集合，\(Init\) 是初始状态，且 \(Init \in N\)。 - \(U\) 是形如 \((D, A, e)\) 的标签集合，其中 \(D\) 和 \(A\) 是谓词，\(e\) 是事件名称。 - \(W\) 是迁移关系，\(W \subseteq P(N \times U \times N)\)。 迁移 \((E, (D, A, e), F)\) 表示在状态 \(E\) 下，若谓词 \(D\) 成立，则事件 \(e\) 被启用；从状态 \(E\) 开始，若事件 \(e\) 被启用，且谓词 \(A\) 成立，则系统会到达状态 \(F\)。其中，谓词 \(D\) 称为启用谓词，\(A\) 称为可达性谓词。 状态 \(N\) 被解释为变量 \(x\) 所在变量空间的子集，其解释由函数 \(I\) 给出，使得 \(I(E)\) 是关于自由变量 \(x\) 的谓词，用于刻画 \(E\) 所代表的子集。 ### 2.2 迁移跨越的定义 设 \((E_1, (D, A, e), E_2)\) 是系统 \(S\) 上的 SLTS \(T\) 的一个迁移，给定状态变量 \(x\) 的值 \(x_1\) 和 \(x_2\) 满足系统 \(S\) 的不变式，那么通过该迁移从 \(x_1\) 到 \(x_2\) 的跨越是合法的，当且仅当满足以下条件： 1. \([x := x_1](I(E_1) \land D \land A)\) 2. \([x, x' := x_1, x_2] prdx(Action(e))\) 3. \([x := x_2]I(E_2)\) 这种合法的迁移跨越表示为：\((E_1, x_1) \rightsquigarrow_{(D,A,e)} \rightsquigarrow (E_2, x_2)\) ### 2.3 路径的定义 给定系统 \(S\) 上的符号化标记迁移系统 \(T\)，事件发生序列 \(e_0 \cdots e_{n + 1}\) 是 \(T\) 中的一条路径，当且仅当存在状态列表 \(E_0, \cdots, E_{n + 1} \in N\)（其中 \(E_0 = Init_T\)）和迁移列表 \((D_i, A_i, e_i)\)（\(i \in 0..n\)），使得： \(\exists x_0, \cdots, x_{n + 1} \cdot (\bigwedge_{i = 0}^{n}((E_i, x_i) \rightsquigarrow_{(D_i,A_i,e_i)} \rightsquigarrow (E_{i + 1}, x_{i + 1})))\) \(T\) 的所有有限路径的集合记为 \(Paths(T)\)。 ### 2.4 状态和迁移的构建 为了从事件 - B 系统 \(S\) 和给定的状态集合 \(N\) 计算出 SLTS，需要考虑以下步骤： 1. **构建状态 \(N\)**：考虑变量空间上的谓词列表 \(\{P_1, \cdots, P_n\}\)，要求该集合相对于不变式是完备的，即不变式指定的所有状态都包含在由 \(P_i\) 谓词确定的状态中，即 \(I \Rightarrow \bigvee_{i = 1}^{n} P_i\)。 - SLTS 的状态 \(N = \{Init_S, E_1, \cdots, E_n\}\)，其解释定义为： - \(I(Init_S) = true\) - \(I(E_i) = P_i \land I\)，\(i \in 1..n\) - 记 \(N_1 = N - \{Init_S\}\)，由上述完备性性质和 \(N\) 的定义可得：\(I \Leftrightarrow \bigvee_{i = 1}^{n} I(E_i)\)。 2. **有效迁移的条件**：设 \(S\) 是一个系统，\(E\) 和 \(F\) 是 \(N\) 中的两个状态，\(e\) 是一个事件，那么迁移 \((E, (D, A, e), F)\) 是有效的，当且仅当谓词 \(D\) 和 \(A\) 满足以下条件： - \(I(E) \Rightarrow (D \Leftrightarrow Guard(e))\) - \(I(E) \land Guard(e) \Rightarrow (A \Leftrightarrow \langle Action(e) \rangle I(F))\) 通过应用共轭最弱前置条件的定义，条件 b) 等价于： \(I(E) \land Guard(e) \Rightarrow (A \Leftrightarrow \exists x' \cdot (prdx(Action(e)) \land [x := x']I(F)))\) 所有迁移相对于系统 \(S\) 都有效的 SLTS 称为有效符号化标记迁移系统。 ### 2.5 迹和路径的相等性定理 设 \(S\) 是一个具有不变式 \(I\) 和事件 \(Ev\) 的事件 - B 系统，\(T\) 是根据 \(S\) 构建的有效符号化标记迁移系统，则有： \(Traces(S) = Paths(T)\) 证明过程如下： 要证明对于所有的 \(t\)，\(t \in Paths(T) \Leftrightarrow t \in Traces(S)\)。 路径 \(t = e_0 \cdots e_n\) 对于状态序列 \(E_0, E_1, \cdots, E_{n + 1}\) 是一条路径（根据路径的定义）： \(\exists x_0, \cdots, x_{n + 1} \cdot (\bigwedge_{i = 0}^{n}((E_i, x_i) \rightsquigarrow_{(D_i,A_i,e_i)} \rightsquigarrow (E_{i + 1}, x_{i + 1})))\) 根据迁移跨越的定义，可得： \(\exists x_0, \cdots, x_{n + 1} \cdot (\bigwedge_{i = 0}^{n}([x := x_i](I(E_i) \land D_i \land A_i) \land [x, x' := x_i, x_{i + 1}]prdx(Action(e_i)) \land [x := x_{i + 1}]I(E_{i + 1})))\) 根据有效迁移的条件，可将 \(D_i\) 替换为 \(Guard(e_i)\)，\(A_i\) 替换为 \(\exists x' \cdot (prdx(Action(e_i)) \land [x := x']I(E_{i + 1}))\)，上述公式简化为： \(\exists x_0, \cdots, x_{n + 1} \cdot (\bigwedge_{i = 0}^{n}([x := x_i](I(E_i) \land Guard(e_i)) \land [x, x' := x_i, x_{i + 1}]prdx(Action(e_i)) \land [x := x_{i + 1}]I(E_{i + 1})))\) 需要