想象一下，你正在教机器人如何驾驶汽车。你有两种主要方法：
- “严谨工程师”方式（基于模型的测试）：你编写一份复杂的数学蓝图，涵盖每一条可能的道路、每一种天气状况和每一个交通信号灯。它极其精确，覆盖所有场景，但只有数学家才能读懂。如果你想向老板展示机器人会做什么，你必须将数学内容重新翻译回英语，这既困难又容易出错。
- “讲故事者”方式（行为驱动开发）：你编写一个故事：“给定汽车在道路上，当信号灯变红时，那么汽车停下。”每个人都懂。它易于编写和阅读，但它就像只为某一天编写的食谱。如果你想测试每一种可能的交通信号灯时序，你就必须编写成千上万个独立的故事，这会变成一堆杂乱无章、难以管理的纸张。
问题：
在现实世界中，公司既想要“严谨工程师”的精确性，又想要“讲故事者”的可读性。通常，他们不得不二者选其一。如果选择故事，就会遗漏隐藏的缺陷；如果选择数学，就无人能理解测试内容。
解决方案：PICKLES
本文作者创建了一个名为PICKLES（用于测试场景的精确输入与控制流关键词语言）的新框架。可以将 PICKLES 想象为一座连接故事与数学的“通用翻译器”。
以下是其工作原理，使用一个简单的类比：
1. “智能食谱”（语言）
与其编写关于一辆特定汽车在一个特定红灯处停车的故事，PICKLES 允许你编写一个“智能食谱”。
- 旧方式：“汽车在主干道的红灯处停下。”（过于具体）。
- PICKLES 方式：“汽车在任何红灯处停下，前提是信号灯为红色且汽车正在行驶。”
- 魔力所在：你可以定义诸如“信号灯可以是红色到绿色之间的任何颜色”或“汽车速度可以是 0 到 100 之间的任何值”这样的规则。这称为参数化。它将单个故事转化为一条规则，一次性覆盖成千上万种可能性。
2. “自动架构师”（翻译）
一旦你用纯英语（使用类似于流行的 Gherkin 语言的格式）编写了这些“智能食谱”，PICKLES 工具就会充当“自动架构师”。
- 它读取你的英语规则。
- 它在幕后即时构建一个形式化模型（复杂的数学地图）。
- 这张地图极其详尽，知晓系统可能采取的所有路径，甚至包括你未明确写出的路径。
3. “主地图”（组合故事）
在传统测试中，你分别测试故事 A，然后故事 B，然后故事 C。
- 缺陷：故事 A 可能有效，故事 B 也可能有效，但如果你先执行 A 再执行 B，系统可能会崩溃。传统故事往往遗漏这些“握手”错误。
- PICKLES 的修复：该工具将所有独立的故事缝合成一张巨大的“主地图”。它弄清楚故事 A 如何连接到故事 B，以及故事 B 如何连接到故事 C。它构建了系统随时间行为的完整图景，而不仅仅是孤立时刻的行为。
4. “反向翻译”（可读结果）
这是最巧妙的部分。该工具利用主地图自动生成数百个具体的测试用例。
- 通常，这些测试会以令人困惑的数学代码形式呈现。
- PICKLES 将这些数学结果翻译回英语故事。
- 因此，测试人员会得到一份报告，内容是：“这是一个具体的测试：汽车以 50 英里/小时行驶，信号灯在 2.5 秒时变红。汽车正确停下了。”
- 人类可以阅读、理解并验证它，尽管繁重的计算工作是由数学引擎完成的。
现实世界测试（交通系统）
作者在 Technolution 公司使用的一个真实交通管理系统上测试了该方法。
- 设置：他们采用了关于交通传感器检测故障探测器的现有故事。
- 结果：
- 使用旧的“讲故事者”方法（逐个运行故事），他们仅测试了约**30%**的潜在系统行为。
- 使用 PICKLES（组合故事并利用数学引擎），他们实现了系统逻辑的100% 覆盖。
- 他们无需编写数百个新故事。他们只需通过添加变量（如“任何车道”或“任何位置”）使原始故事变得更“智能”，并让工具完成其余工作。
为何这很重要
PICKLES 允许非技术人员（如项目经理或业务分析师）用无歧义且数学严谨的纯英语编写需求。它确保：
- 无人困惑：需求对每个人都很清晰。
- 无隐藏缺陷：数学引擎能发现人类可能遗漏的边界情况。
- 减少工作量：你只需编写更少的故事即可测试更多场景。
简而言之，PICKLES 就像给机器人一本故事书，这本书足够智能，能理解故事的每一种可能变体，解决其中的数学问题，然后用清晰的纯英语向你写出一份报告。
以下是论文《PICKLES：一种用于需求规范与基于模型测试的自然语言框架》的详细技术总结。
1. 问题陈述
本文探讨了工业软件测试（尤其是安全关键系统）中存在的一个关键矛盾：
- 基于模型测试（MBT）的局限性： 虽然 MBT 通过形式化模型提供了严谨、系统且高覆盖率的测试，但其采用受到定义和维护这些模型难度的阻碍。这些模型通常需要专业知识，对非技术利益相关者缺乏可读性，并造成沟通障碍。
- 行为驱动开发（BDD）的局限性： BDD 使用人类可读的自然语言场景（Given-When-Then）来促进协作。然而，BDD 依赖于具体示例，这往往导致：
- 歧义与不完整： 自然语言可能含糊不清。
- 覆盖率低： 测试孤立的示例往往遗漏边缘案例和复杂的交互序列。
- 维护成本： 大量具体的测试用例套件昂贵且难以维护和更新。
核心挑战： 如何在保留 BDD 的可访问性、可读性和利益相关者协作优势的同时，实现 MBT 的精确性和高覆盖率，而无需让从业者在这两者之间做出选择。
2. 方法论：PICKLES 框架
作者提出了 PICKLES（用于测试场景的精确输入与控制流关键词语言），这是一个通过双向翻译流程连接 BDD 与 MBT 的框架。
A. 领域特定语言（PicklesDSL）
Pickles 扩展了标准的 Gherkin 语法（Given-When-Then），引入了形式化构造以消除歧义：
- 变量设置： 一个前导块，其中变量被显式类型化（例如：整数、布尔值、数组、结构体）并分配定义域/范围（例如：
[1, 3]，{AV, PART_AV}）。
- 参数化： 步骤可以引用变量，并使用逻辑运算符（AND, OR）和量词（至少、至多、恰好）包含守卫块（条件）。
- 结构：
Given：定义前置条件和初始状态守卫。When：定义带有参数和守卫的输入交互。Then：定义预期输出和验证守卫。
B. 形式语义：符号转换系统（STS）
该框架将 PicklesDSL 规范转换为符号转换系统（STS），这是一种扩展了数据构造的标记转换系统形式化方法。
- 翻译（规范 → STS）：
- 每个 Pickles 场景映射到一个部分 STS。
Given 子句变为初始守卫。When 子句变为输入开关（转换）。Then 子句变为输出开关。- 变量和守卫被映射到 STS 参数、位置变量和逻辑谓词。
- 模型组合：
- 单个场景 STS 被组合成一个主模型（Master Model）。
- 选择组合（⋈）： 合并多个场景的初始状态，允许任何场景开始。
- 顺序组合（▹）： 将一个 STS 的汇点（结束）状态连接到其他 STS 的初始状态，从而生成结合多个场景的长执行轨迹。
C. 测试生成与反向翻译
- 测试生成： 将标准 MBT 算法（具体旨在实现 100% 开关覆盖率）应用于主模型，以生成形式化测试用例（具有特定参数值的开关序列）。
- 反向翻译（STS → Pickles）： 将形式化测试用例翻译回 PicklesDSL 语法。
- 输入值在
When 步骤中显式定义。
- 输出值被替换为原始的
Then 守卫，以验证被测系统（SUT）的行为。
- 结果是可执行的、人类可读的测试用例，兼容标准 BDD 工具（例如 Cucumber）。
3. 主要贡献
- PicklesDSL： 一种新的领域特定语言，保留了 Gherkin 结构，但增加了显式的变量类型化、定义域定义和控制流约束，确保规范的无歧义性。
- 双向翻译： PicklesDSL 与符号转换系统（STS）之间的形式化映射，允许在人类可读的需求与形式化模型之间无缝转换。
- 主模型组合： 一种将来自单个场景的部分 STS 自动组合成统一主模型的方法，能够发现孤立场景遗漏的复杂交互缺陷。
- 原型实现： 一个基于 Python 的工具（使用 Lark 解析器），自动化了翻译、组合和反向翻译过程。
- 工业验证： 将该框架应用于 Technolution 公司的一个真实世界交通管理组件。
4. 结果
该框架通过涉及交通管理系统组件的案例研究进行了评估。结果显示，与使用相同手动定义场景的传统 BDD 方法相比，取得了显著改进：
- 转换覆盖率：
- 传统 BDD： 孤立执行场景仅覆盖了约 30% 的可能系统转换。
- Pickles： 通过组合场景并从主模型生成测试，覆盖率提升至 100%。这代表了 70 个百分点 的改进。
- 输入覆盖率：
- 使用硬编码值的传统 BDD 仅测试了极小部分可能的输入。
- Pickles 通过利用变量定义域和边界分析，为单个场景（场景 02）表示了 112 种不同的输入可能性，否则这需要数百个手动测试用例。研究表明，与具体的 BDD 示例相比，输入覆盖率提高了 98.5%。
- 效率： 手动实现 100% 转换覆盖率至少需要七个不同的测试轨迹。Pickles 仅用四个输入场景就实现了这一目标，显著减少了人工努力和维护成本。
5. 意义
PICKLES 框架代表了使基于模型测试对工业从业者更具可访问性的重要一步：
- 弥合差距： 它成功消除了可读性与精确性之间的权衡。利益相关者可以用自然语言协作制定需求，而系统自动确保形式化严谨性。
- 测试左移： 通过实现场景的自动组合，它允许在开发生命周期的更早阶段进行集成和系统级测试，检测孤立单元测试遗漏的交互缺陷。
- 可维护性： 需求变更（例如变量范围）会自动传播到所有生成的测试用例中，减少了与大型 BDD 套件相关的维护负担。
- 可解释性： 与黑盒形式化模型不同，生成的测试用例保持为人类可读的 Pickles 格式，使得向非技术管理人员和审计人员解释测试结果更加容易。
总之，PICKLES 证明，通过将自然语言规范建立在形式语义之上并利用自动模型组合，组织可以在不牺牲 BDD 协作优势的情况下实现 MBT 的高可靠性。
每周获取最佳 computer science 论文。
受到斯坦福、剑桥和法国科学院研究人员的信赖。
请查收邮箱确认订阅。
出了点问题，再试一次？
无垃圾邮件，随时退订。