模型驱动测试工具综述

### 模型驱动测试工具综述 #### 1. 基于状态空间搜索的测试 在状态空间搜索测试中，使用 ProB 工具从初始状态开始对有限状态机（FSM）进行遍历，以生成一组操作序列。在生成的序列中，FSM 中的每个操作实例至少出现一次，每个这样的 B 操作序列构成后续实现的一个测试用例。 #### 2. 特定编程语言的测试扩展 ##### 2.1 Spec# Spec# 是 C# 编程语言的扩展，它允许对不同的构造进行规范定义，如前置和后置条件、非空类型以及更高级的数据抽象。这些规范会成为程序执行的一部分，在运行时进行动态检查，以确保程序与其规范的一致性。这为程序员提供了一种编写和验证断言/方法契约的方式。 ##### 2.2 Spec Explorer Spec Explorer 为用 Spec# 编写的模型程序提供在线和离线测试。模型程序定义了抽象状态机（ASM）的状态变量和更新规则。ASM 是一种状态机，在每一步计算机器变量的一组更新，并同时提交所有更新。机器的状态由每一步变量的值定义，而状态之间的转换是对满足给定前置条件的模型程序方法的调用。该工具使用接口自动机理论，测试用例生成可以看作是被测系统（SUT）和测试生成器之间的一个游戏。测试用例生成算法从系统的初始状态开始，在每个状态下，等待 SUT 执行可观察事件，否则执行模型中前置条件为真的可控方法之一，直到系统达到接受状态。此时，每个测试用例就是抽象状态机的一个操作序列。通过对 ASM 进行动画模拟，可以得到对应特定测试用例的测试序列结束时的状态。将 ASM 的 Java 实现与相同的测试用例和得到的状态进行关联执行，如果两个状态匹配，则表示实现通过了测试。 ##### 2.3 AsmL 抽象状态机语言（AsmL）融合了抽象状态机范式和 .NET 语言运行时系统。它可以与任何 .NET 语言集成，支持元建模，允许对模型中的非确定性进行编程探索，从而实现各种状态探索算法，包括显式状态模型检查、测试生成和测试评估。AsmL 工具环境通过显式状态模型检查技术探索 AsmL 模型的状态空间来生成 FSM。从初始状态开始，启用的动作被触发，产生一组后继状态，然后继续探索。如果方法的前置条件在当前状态为真，则该动作被启用。从 FSM 可以生成测试用例（即调用序列），用于对模型和实现进行一致性测试，实现可以用任何 .NET 语言编写。为了实现这一点，在中间代码级别重写实现程序集，插入回调监控方法到运行时验证引擎。每次调用监控方法时，其参数和输出结果会传播到一致性测试管理器。在每个当前可能的模型状态下，调用相应的模型方法，这些调用的结果状态构成下一组模型状态。如果这组状态为空，则一致性测试失败。 #### 3. ProTest 生成测试用例 以咖啡/茶自动售货机为例，ProTest 生成测试用例包括以下五个步骤： 1. **识别因素**：在 B 机器中，因素（或变量）是在执行过程中可以满足不同条件的“项”。对于咖啡/茶自动售货机，因素包括所选饮料、提供的饮料、投入的硬币和找零。 2. **确定每个因素的级别**：对于每个因素，确定感兴趣的级别，即我们打算测试的变量的可能不同值。例如，所选饮料可以为空（未选择饮料）、茶或咖啡，用户可以投入 0 到 5 个硬币。 3. **建立约束**：根据每个因素的给定级别，确定一系列表示因素之间不可行关系的约束。约束规则为：“如果 <因素 A> 处于 <级别 1>，则 <因素 B> 不能处于 <级别 2>”。对于咖啡/茶自动售货机，确定了 19 个约束。 4. **输入先前的运行情况**：可以通过元组 <所选饮料, 硬币, 找零, 提供的饮料> 指定先前的测试尝试，用于减少工具提供的测试总数。对于咖啡/茶自动售货机，未指定此类先前运行情况。 5. **生成所有双向组合**：ProTest 将为步骤 1 到 4 描述的模型生成测试用例。对于咖啡/茶自动售货机，工具自动从 101 种可能的输入组合中生成 85 个测试用例。 以下是咖啡/茶自动售货机因素和级别的表格： | 因素 | 级别 | | ---- | ---- | | 所选饮料 | 空、茶、咖啡 | | 投入的硬币 | 0 - 5 个 | | 找零 | 多种可能值 | | 提供的饮料 | 茶、咖啡等 | 下面是 ProTest 生成测试用例的流程图： ```mermaid graph TD; A[识别因素] --> B[确定每个因素的级别]; B --> C[建立约束]; C --> D[输入先前的运行情况]; D --> E[生成所有双向组合]; ``` #### 4. 基于转换的符号