软件测试与系统验证技术：从Z规格说明到PLTL属性保留

### 软件测试与系统验证技术：从Z规格说明到PLTL属性保留 在软件开发过程中，测试与验证是确保系统质量和可靠性的关键环节。本文将介绍两种重要的技术方法，一种是从Z规格说明自动生成信息以支持分类树方法进行测试用例生成，另一种是在反应式系统中验证动态属性并证明精化关系能保留命题线性时态逻辑（PLTL）属性。 #### 从Z规格说明自动生成信息 在测试用例生成中，分类树方法是一种常用的技术。传统方法可能会遇到组合爆炸的问题，而这里介绍的方法可以部分自动化地从Z规格说明生成分类树，避免了这一问题。 该方法利用两种信息来源：模式的签名和其中包含的谓词。对于输入或状态变量的每种类型，可以设计一些标准分区。例如，对于整数，可以分为小于零的整数、零和大于零的整数。 算法会识别规格说明中涉及描述操作前置条件（定义谓词）或确定应用哪种行为（分区谓词）的谓词。定义谓词为每个测试用例提供前置条件，分区谓词用于形成分类树的节点。 此外，还定义了谓词的测试上下文。给定规格说明S中的分区谓词p，p在S中的测试上下文确定了为使p的值相关而必须做出的其他选择。这有助于测试人员避免一些没有意义的抽象测试用例，提高测试效率和有效性。 例如，有这样一个条件： ```plaintext outward date? ≥ current date? ∧ travel period? = offpeak ``` 其中第一个谓词是定义谓词。如果为分类方面 `r? = OAP` 选择了类 `True`，那么对于分类方面 `travel period? = offpeak` 也应该选择类 `True`。这意味着测试人员不需要有 `r? = OAP` 为 `True` 且 `travel period? = offpeak` 为 `False` 的抽象测试用例。 下面是该方法的主要步骤： 1. **信息提取**：从Z规格说明中提取模式的签名和谓词。 2. **分区设计**：为输入或状态变量的每种类型设计标准分区。 3. **谓词识别**：使用算法识别定义谓词和分区谓词。 4. **分类树生成**：利用定义谓词和分区谓词生成分类树。 5. **测试上下文应用**：根据谓词的测试上下文，避免无效的抽象测试用例。 #### 反应式系统中PLTL属性的保留 在反应式系统的设计和验证中，动态属性的引入是必要的。这里使用B事件系统结合命题线性时态逻辑（PLTL）公式来指定反应式系统。 ##### 1. 基本概念 - **原子命题**：设V是一组变量，原子命题是形如 `xi = dj` 的公式，其中 `xi` 属于V，`dj` 属于 `Dom(xi)`。 - **状态命题**：状态命题由原子命题通过逻辑或和逻辑非组合而成。 - **带标签的转换系统（LTS）**：一个LTS由五元组 `(Q, Q0, L, T, l)` 定义，其中Q是状态集，Q0是初始状态集，L是转换标签集，T是转换关系，l是从状态到状态命题的单射映射。 - **B事件系统**：一个B事件系统是五元组 `(E, V, I, Init, D)`，其中E是事件标签的有限集，V是变量的有限集，I是定义事件系统不变量的状态命题，Init是定义系统初始状态的替换，D是每个事件对应的广义替换集。 ##### 2. 从B事件系统到带标签的转换系统 为了将B事件系统转换为带标签的转换系统，需要定义最弱前置条件和共轭最弱前置条件。 - **最弱前置条件**：设S是广义替换，sp是状态命题，`[S]sp` 是S建立sp的最弱前置条件。 - **共轭最弱前置条件**：`< S > sp = ¬[S]¬sp` 定义了S可能建立sp的共轭最弱前置条件。 通过以下规则构建转换系统： - **