访谈： BTC模型检查器（Model Checker）的工作原理

模型检查器（Model Checker）是形式化方法的一部分，涵盖形式化规范、形式化开发、形式化验证和定理证明，属于形式化验证，提供对被测系统的完整数学证明，以确保其符合预期的属性和规范。

BTC EmbeddedPlatform 利用模型检查技术来生成结构化测试数据，实现完整的代码覆盖。此外，它还用于形式化验证，确保形式化需求不会被违反，并为这些需求生成测试用例。这种技术在提高代码质量和验证系统行为方面发挥了重要作用。

现在，让我介绍一下我的同事 Dr. Karsten Scheibler，他是我们创新与技术部门中模型检查主题的专家，也是我们iSAT3模型检查引擎的发明者和开发者。

Wolfgang：嘿，Karsten，谢谢你参加这篇博客文章。你是怎么接触到模型检查的？

Karsten：嗨，Wolfgang，基本上，这得源于我的博士研究，当时的研究主题正是模型检查。

Wolfgang：你在模型检查方面有多年的经验，甚至自己设计并编程了一个模型检查器，那么你会如何向一个从未听说过它的人介绍什么是模型检查器？

Karsten：顾名思义，模型检查是关于检查模型的属性。因此，模型检查器是一种用于执行这些检查的工具。它通过分析系统的抽象（即模型）来代替直接研究系统本身。模型通常由一组状态和一个转换关系组成，描述模型随着时间的推移如何改变其状态。在许多情况下，只考虑离散的时间点，即时间以步骤递增，从时间点 t 到 t+1，转换关系决定模型在 t+1 的状态取决于其在 t 时的状态

Wolfgang：好的，但这听起来还是很抽象。你能举个例子吗？

Karsten：让我用交通灯来说明。当为交通灯创建模型时，模型状态对应于所有可能的绿灯、黄灯和红灯的启用和禁用组合，而转变关系描述了在时间步中哪些灯会被打开或关闭（这个时间步可以是例如一秒）。此外，额外的输入可能以非确定性方式影响系统的行为。在这个例子中，这可能是交通灯旁的一个按钮，用于让行人过马路变成绿灯。这些输入也必须在转变关系中考虑。在检查这个交通灯模型时，一个有趣的属性可能是：“是否不可能进入所有绿灯都亮的状态”。我们可以把违反某个属性的状态称为“坏状态”。

经典测试方法即使包含许多测试用例，也只能覆盖所有可能状态的一个子集，而模型检查能够对所有可能状态进行完整分析。

Wolfgang：所以“坏状态”意味着我要验证的属性被违反了？

Wolfgang：你提到了属性和坏状态，但模型检查器到底做了什么？

Karsten：基本上，模型检查器会跟踪一组可达状态——我们称这组状态为 R。起初，R被初始化为给定的初始状态。接着，模型检查器逐步执行时间步，将系统可能转变到的所有状态加入到 R 中。如果坏状态被添加到 R 中（属性被违反），或在执行时间步时 R 保持不变（属性被证明），模型检查器就会停止。

Wolfgang：你提到模型是对系统的抽象，但在考虑汽车软件时，这样的模型是什么样子的呢？

Karsten：软件本身可以视为系统的形式化描述，因此不需要抽象的模型来表示它。换句话说，软件已经是我们希望验证属性的模型。以一个小的 C 程序为例，可以直接将该程序用作模型检查的对象，以验证其是否满足特定属性。

static int s = 0;void f(int i1, int i2, int i3) {    if (i1 + i2 + i3 == 12345) s++;}

Wolfgang：找到特定的值组合听起来是一个非常复杂的任务。随机自动测试生成方法在这里可能不是最佳选择。模型检查器是如何处理这个任务的呢？

模型检查器以两种方式有效处理这个任务：

1. 逐步赋值和推导：模型检查器逐步为变量赋值，并在每次赋值后推导出进一步的值。例如，在为 i1 和 i2 赋值后，模型检查器会计算满足 if 条件的 i3 的正确值。如果发现某个组合不符合条件，它会将此信息泛化到其他组合，从而减少尝试次数。

2. 紧凑的状态表示：使用特殊的数据结构来表示状态集，保持其紧凑性以执行高效操作，尽可能减少所需的存储空间。

这两种方法可以帮助模型检查器找到有效的输入组合，避免了随机测试的低效率。

Wolfgang：但这是否意味着我们需要处理一个巨大的搜索空间？

Karsten：是的，这就是为什么模型检查器会尽可能地缩减搜索空间。只有当属性在搜索空间的所有值组合中都成立时，才能证明该属性。因此，要么明确测试搜索空间中的所有组合（例如，对于两个32位整数，大小为2^64的搜索空间几乎不可行），要么利用一些最优路径。不同模型检查器利用的最短路径各异，这解释了为什么某些模型检查器在特定程序上表现良好，而另一些可能无法在合理时间内完成。

Wolfgang：如果模型检查器找不到这个最优路径，会发生什么？

Wolfgang：我了解到，模型检查器可以处理并支持测试中的不同用例。它们可以用于生成结构测试数据，实现模型和代码的完整覆盖；可以证明形式需求永远不会被违反；甚至可以从形式需求中生成基于需求的测试用例。那么，模型检查器是如何在这些用例中提供结果的呢？

Karsten：这里的关键在于每个测试用例生成前的准备过程，使模型检查器需要找到一个激励向量。例如，如果需要检查一个程序 P1（通常是你要测试的系统）是否满足某个形式化需求，那么这个需求会被转换成一个程序 P2，然后与 P1 合并成新的程序 P3。请注意，P2 被构造为当需求被违反时将特定变量设置为 1，否则保持为 0。模型检查器的任务是在 P3 中找到一个激励向量，使这个特定变量被设置为 1。如果存在这样的激励向量，说明需求被违反；否则，需求被满足，没有任何输入组合可以违反该需求。

Wolfgang：这些结果听起来都很棒！那么使用这项技术是否也有一些局限性和挑战呢？

Karsten：正如前面提到的，不同的模型检查器在使用的最优路径上有所不同——一个模型检查器可能在特定程序上表现良好，而另一个可能无法在合理时间内终止。可以通过使用不同的模型检查器来缓解这个问题。此外，随着当今多核 CPU 的发展，也可以并行启动多个模型检查器。此外，良好的预处理对性能至关重要——即使是最好的模型检查器，如果所要解决的问题编码不佳，也会表现不理想。

Wolfgang：你认为这项技术会有突破，还是会被另一种可能更高效且能提供类似结果的方法所取代？

Karsten：我认为模型检查将继续存在。此外，我相信未来会看到进一步的改进——例如，更好的预处理等行为。此外，对模型检查用户来说，所谓的突破可能只是模型检查器中现有技术的改进组合。因此我认为，通过模型检测得到的最优路径现在是，将来也会是你最好的朋友！

Wolfgang：非常感谢你，Karsten，为我们提供了关于这项有趣且强大的技术的深入见解。祝你有美好的一天，希望我们能很快再次见到你。

总结

Model Checker是一项自八十年代中期由学术界发起的强大技术。超过20年来，BTC Embedded Systems与这个领域保持着深厚的联系，使这项技术得以应用于全球嵌入式软件开发。我们的另一位同事 Dr. Tino Teige 的文章《The Power of Focus》，也可以帮助大家更好地了解如何将这项技术有效地应用于汽车等特定领域。

总而言之，模型检查在项目中带来了巨大的价值，包括稳健性分析、状态驱动分析、边界值分析和形式化验证等。它为检查的属性提供了数学上验证的信心，并有助于符合 ISO 26262 标准，特别适用于 ASIL C 和 D 的项目。此外，由于这些分析大多数不需要人工干预，它们可以完全自动化，从而减少测试团队的工作量。

9.24【BTC·中国】网络直播研讨会—“你所不知道的CI/CD与Jenkins自动化部署”即将开始，将为您揭示CI/CD与Jenkins的最新技术动态，并通过实操演示帮助您掌握自动化部署的精髓，欢迎联系交流！