ACM通信

实践

软件模型检查开始流行

文/ Steven P. Miller, Michael W. Whalen, Darren D. Cofer
ACM通讯，2010年2月，第53卷第2期，第58-64页
10.1145/1646353.1646372
评论

虽然正式的方法已经在安全和安全关键系统的开发中使用多年，但它们还没有在软件或系统工程中实现广泛的工业应用。然而，有两个重要的趋势正在使形式化方法的工业应用成为现实。首先是越来越多的人接受嵌入式系统设计中基于模型的开发。MATLAB Simulink等工具⁶以及Esterel Technologies SCADE套件²在航空电子设备和汽车系统的设计中得到广泛应用。这些工具生成的图形模型提供了一种正式的或近乎正式的规范，通常可以进行形式分析。

其次，正式验证工具的功能日益强大，尤其是模型检查器。对于许多类型的模型，它们提供了确定模型是否满足其需求的“按钮”方法。由于这些工具检查输入和状态的所有可能组合，因此它们比测试更有可能发现设计错误。

在这里，我们将描述由Rockwell Collins和明尼苏达大学开发的翻译框架，该框架允许我们将一些最流行的商业建模语言自动转换为各种模型检查器和定理证明器。我们描述了在工业系统上使用这些工具的三个案例研究，这些案例表明，在得到自动化工具的适当支持时，形式化验证可以有效地用于实际系统。

回到顶部

基于模型的开发

基于模型的开发(MBD)指的是使用领域特定的图形化建模语言，这些语言可以在实际系统构建之前执行和分析。这种建模语言的使用允许开发人员创建系统的模型，在他们的桌面上执行它，用自动化工具分析它，并使用它自动生成代码和测试用例。

在本文中，我们使用MBD专门指使用同步数据流语言开发的软件，例如MATLAB Simulink和Esterel Technologies SCADE Suite中的那些语言。同步建模语言在计算步骤的开始锁定它们的输入，计算下一个系统状态及其作为单个原子步骤的输出，并使用数据流信号在组件之间进行通信。这与更通用的建模语言不同，后者包括支持组件的异步执行和使用消息传递的通信。MBD在航空电子设备和汽车行业非常流行，我们发现同步数据流模型特别适合使用模型检查进行自动验证。

模型检查器是正式的验证工具，用于评估模型以确定它是否满足给定的属性集。¹模型检查器将考虑输入和状态的每一种可能组合，使验证等同于对模型的详尽测试。如果某个属性不为真，模型检查器会生成一个反例，显示如何对该属性进行证伪。

有许多类型的模型检查器，每种都有自己的优点和缺点。显式状态模型检查器，如SPIN⁴构造并存储访问过的每个状态的表示。隐式状态(符号)模型检查器使用状态集的逻辑表示(如二进制决策图)来描述满足被评估属性的模型状态空间区域。这种紧凑的表示通常允许符号模型检查器比显式状态模型检查器处理更大的状态空间。我们使用了基于bdd的模型检查器NuSMV⁵分析超过10个的模型¹²⁰可获得的状态。

最近的模型检查器，比如SAL¹¹和证明插件，⁹使用可满足模理论(SMT)求解器，用于推理包含实数和无界数组的无限状态模型。这些检查器使用一种状态转换关系的归纳形式来自动证明一个属性对模型中的所有可执行路径都有效。虽然这些工具可以处理更大类型的模型，但必须编写要检查的属性以支持归纳证明。

回到顶部

翻译器框架

作为NASA航空安全计划(AvSP)的一部分，罗克韦尔柯林斯公司和明尼苏达大学开发了一个翻译器产品系列，弥补了一些最流行的商业建模语言和一些模型检查器和定理证明器之间的差距。⁸中显示了该框架的概述图1．

这些翻译器主要使用Lustre形式化规范语言，^3.但这对用户是隐藏的。转换的起点是MATLAB Simulink/Stateflow或Esterel Technologies SCADE Suite/Safe State Machines中的设计模型。SCADE套件直接生产Lustre模型。可以使用SCADE Suite或Reactis导入Simulink或Stateflow模型¹⁰Rockwell Collins开发的工具和翻译器。为了确保每个Simulink或statflow构造都具有定义良好的语义，转换器将其接受的模型限制为那些可以明确地转换为Lustre的模型。

一旦进入Lustre，规范就会被加载到一个抽象语法树(AST)中，并对其应用许多转换传递。每个转换过程都会产生一个新的Lustre AST，它在语法上更接近于目标规范语言，并保留了原始Lustre规范的语义。这使得所有Lustre类型检查和分析工具都可以在翻译程序开发过程中作为调试辅助工具使用。当AST足够接近目标语言时，将使用漂亮的打印机输出目标规范。

---

模型检查器将考虑输入和状态的每一种可能组合，使验证等同于对模型的详尽测试。如果某个属性不为真，模型检查器会生成一个反例，显示如何对该属性进行证伪。

---

我们将我们的翻译器框架称为产品族，因为大多数转换过程在每种目标语言的翻译器中都被重用。转换传递的重用使得支持新的目标语言变得更加容易;我们在几天内就培养出了新的翻译人员。转换传递的次数取决于源语言和目标语言的相似性，以及要进行的优化的次数。我们的翻译人员从12个到60多个。

翻译器生成适合目标语言的高度优化的规范。例如，当翻译到NuSMV时，翻译器会尽可能地消除冗余的内部状态，这使得它对于基于bdd的模型检查非常有效。当转换为PVS定理证明时，规范针对可读性进行了优化，并支持在PVS中开发证明。在生成可执行的C或Ada代码时，代码会针对目标处理器上的执行速度进行优化。这些优化可以对目标分析工具产生巨大的影响。例如，集成到NuSMV转换器中的优化通道将NuSMV检查一个模型所需的时间从超过29小时减少到不到一秒。

但是，有些优化可以更好地集成到验证工具中，而不是翻译器中。例如，谓词抽象¹是减小可达状态空间大小的一种众所周知的技术，但是在翻译期间自动化它需要我们的翻译器和分析工具之间的紧密交互，以基于反例迭代地细化谓词。由于许多模型检查器已经实现了这种技术，所以我们还没有尝试将其合并到我们的翻译框架中。

我们开发了将模型检查器生成的反例转换为两种格式的工具。第一个是一个简单的电子表格，它显示了模型每个步骤的输入和输出(类似于所附表中提到的步骤)。第二个是一个测试脚本，Reactis工具可以读取该脚本，以便在Reactis模拟器中的反例中向前和向后执行。

我们的翻译框架目前支持用Simulink、statflow和SCADE编写的输入模型。它生成了NuSMV、SAL和provver模型检查器、PVS和ACL2定理证明器以及C和Ada源代码的规范。

回到顶部

一个小例子

为了使这些想法具体化，我们给出了一个非常小的例子，一个简单微波炉的模式逻辑图2．微波炉刚开始启动设置模式。它过渡到运行时的模式开始按钮被按下，然后剩下的步骤烹饪(最初由键盘输入子系统提供)的值大于零。关于过渡到运行模式，控制器进入烹饪或暂停子模式，取决于是否门关闭是真的。在烹饪模式:控制器递减剩下的步骤在每一步上。如果门是打开的烹饪模式或操作者按下清晰的按钮，控制器进入暂停submode。从暂停子模式下，操作符可以返回到烹饪子模式开始门关闭时按下按钮，或退回设置模式，按清晰的按钮。当剩下的步骤减为0时，控制器退出运行模式，返回到设置模式。

由于此模型仅包含布尔值(开始，清除，门关闭)、枚举类型(模式)和两个小整数(剩下的步骤而且烹饪步骤范围从0到639，可以在键盘上输入的最大值)，它非常适合用符号模型检查器(如NuSMV)进行分析。需要检查的一个有价值的属性是，当微波炉烹饪时，门总是关闭的。在细胞毒性t淋巴细胞¹(NuSMV的属性规范语言之一)，它被写成:

将模型转换为NuSMV并检查此属性只需要几秒钟，就会产生如图所示的反例表1．

在反例的第二步中，我们看到的值开始从0变为1，表示按下了开始按钮。同样在步骤2中，门关闭并且剩下的步骤取值为1。结果，微波进入烹饪步骤2中的模式。在第三步，门被打开，但微波炉仍然在里面烹饪模式，违反我们的安全属性。

为了更好地理解这是如何发生的，我们使用Reactis逐级分析生成的反例。这表明，与其从烹饪来暂停当门被打开时，微波炉就发生了过渡烹饪来烹饪的衰减剩下的步骤因为此转换的优先级(优先级1)高于烹饪来暂停(优先级2)更糟糕的是，微波炉会一直开着门烹饪直到剩下的步骤变成了零。改变这两个转换的优先级并重新运行模型检查器会显示，在所有可能的状态下，如果微波炉正在烹饪，门总是关闭的。

虽然这个例子很小，但这两个整数(剩下的步骤而且烹饪步骤)仍然将其可达状态空间推至9.8 × 10⁶州。还要注意，模型检查器并不一定能找到“最佳”反例。实际上，如果剩下的步骤已在步骤2中设置为大于1的值。然而，这个反例非常典型。在我们所研究的生产模型中，很少有反例的长度超过几个步骤。

回到顶部

案例研究

要真正有价值，模型检查必须能够处理更大的问题。这里描述了将我们的工具应用于工业示例的三个案例研究。Miller等人讨论了第四个案例研究。⁷

ADGS-2100 Window Manager。我们的工具最大和最成功的应用之一是ADGS-2100自适应显示和制导系统窗口管理器。¹³在现代飞机上，飞行员主要通过计算机控制的显示面板来了解飞机状态图3．ADGS-2100是罗克韦尔柯林斯公司的产品，为下一代商用飞机提供平视和平视显示器以及显示管理软件。

窗口管理器(WM)确保来自不同应用程序的数据被路由到正确的显示面板。在正常操作中，WM决定根据先导选择显示哪些应用程序。但是，在组件故障的情况下，WM还决定哪些信息是最关键的，并将这些信息从冗余源之一路由到最合适的显示面板。WM对飞机的安全飞行至关重要。如果WM包含逻辑错误，机组人员可能无法获得关键的飞行信息。

虽然WM非常复杂，但在Simulink中只使用布尔值和枚举类型来指定WM，这使得它非常适合使用基于bdd的模型检查器(如NuSMV)进行验证。WM由五个可以独立分析的主要组成部分组成。这五个组件总共包含16,117个原始Simulink块，这些块被分组为4,295个Simulink子系统实例。5个组件的可达状态空间范围为9.8 × 10⁹至1.5 × 10³⁷州。

最终，关于WM的563个属性被开发和检查，并在早期版本的WM模型中发现并纠正了98个错误。这种验证是在设计过程的早期进行的，当时设计还在不断变化。在项目结束时，WM开发人员在每次设计更改后都会检查属性。

CerTA FCS第一阶段。我们的第二个案例研究是由美国空军研究实验室(AFRL)在先进飞行关键系统认证技术(CerTA FCS)项目下赞助的，目的是比较模型检查和测试的有效性。¹²在这项研究中，我们将我们的工具应用于洛克希德·马丁航空航天公司开发的无人机的作战飞行计划(OFP)。OFP是一种自适应飞行控制系统，可以根据飞行条件调整其行为。项目的第一阶段集中于将我们的工具应用于冗余管理(RM)逻辑，它几乎完全基于布尔和枚举类型。

RM逻辑被分解为三个可以单独分析的组件。虽然相对较小(它们总共包含169个原始Simulink块，组织成23个子系统，可达状态空间从2.1 × 10⁴到6.0 × 10¹³)， RM逻辑在OFP中为飞机上的10个控制面中的每个面复制一次，使其成为OFP逻辑的重要组成部分。

为了比较模型检查和测试在发现错误方面的有效性，这个项目有两个独立的验证团队，一个使用测试，一个使用模型检查。正式的验证团队从OFP需求中开发了总共62个属性，并使用NuSMV模型检查器检查了这些属性，在RM逻辑中发现了12个错误。在这12个错误中，4个被洛·马公司列为3级(只有1级和2级会影响飞行安全)，2个被列为4级，2个导致需求变更，1个是冗余的，3个导致软件发布中尚未实现的需求。

以类似的方式，测试团队根据相同的OFP需求开发了一系列测试。尽管测试团队在测试上投入的时间几乎是正式验证团队在模型检查上投入的时间的一半，但测试未能发现任何错误。这样做的主要原因是演示不是一个全面的测试程序。虽然可以通过测试发现其中一些错误，但是发现和修复这些错误的成本要高得多。此外，通过模型检查发现的错误往往是间歇性的，几乎同时的，或者是很难通过测试检测到的故障的组合序列。两个团队的结论是，在发现设计错误方面，模型检查比测试更具成本效益。

CerTa FCS二期。CerTA FCS项目第二阶段的目的是研究模型检验是否可以用于验证大型、数值密集的模型。在这项研究中，翻译框架和模型检查工具被用于验证无人机OFP的效应器搅拌机(EB)逻辑的重要属性，类似于第一阶段的验证。

EB是OFP的核心组件，为飞机的六个控制面生成致动器命令。它是一个庞大而复杂的模型，反复操作一个3 × 6的浮点数矩阵。它输入32个浮点数输入和一个3 × 6的浮点数矩阵，输出一个1 × 6的浮点数矩阵。它包含超过2000个基本的Simulink块，组织成166个Simulink子系统，其中许多是状态流模型。

---

在每个模型修订之后运行一组属性是一种快速而简单的方法，可以查看是否有什么东西被破坏了。我们鼓励我们的开发人员“尽早检查您的模型并经常检查它们”。

---

由于EB广泛使用浮点数和大状态空间，因此不能使用基于bdd的模型检查器(如NuSMV)进行验证。相反，使用Prover Technologies的Prover smt -求解器分析EB。即使使用了Prover的额外功能，也必须解决几个新问题，其中最难的是处理浮点数。

虽然Prover具有用于实数线性算术的强大决策过程和用于整数的位级决策过程，但它没有用于浮点数的决策过程。将浮点数转换为实数被拒绝，因为EB中的许多算术本质上是非线性的。此外，使用实数将掩盖浮点算术错误，如溢出和下溢。

相反，转换器框架被扩展为使用OFP设计人员提供的缩放因子将浮点数转换为定点数。然后使用位移位将固定点数转换为整数以保持其大小。虽然这允许使用Prover的位级整数决策过程来验证EB，但由于精度的损失，结果是不可靠的。但是，如果在验证过的模型中发现了错误，那么在原始模型中就可以很容易地确认它们的存在。这使得验证可以作为一个非常有效的调试步骤，即使它不能保证正确性。

确定要验证哪些属性也是一个难题。EB的需求实际上是为EB和飞机模型的组合指定的，但是同时检查EB和飞机模型超出了Prover Plug-In模型检查器的能力。在与OFP设计人员协商后，验证团队决定验证六个执行器命令是否总是在动态计算的上限和下限之内。违反这些属性将表明EB逻辑中的设计错误。

即使做了这些调整，EB模型还是足够大，以至于必须将其分解为几个层次的组件层次结构。然后使用provver Plug-In验证这个层次结构的叶节点，并使用手动证明手动验证它们的组成。这种方法还确保了不稳定性不会通过循环推理引入，因为Simulink强制原子子系统之间没有循环依赖关系。

最终，通过对这些属性的模型检查，发现并修正了EB设计逻辑中的5个错误。此外，还发现并纠正了一些被防御性设计实践掩盖的潜在错误。

回到顶部

从案例研究中得到的教训

这里描述的案例研究表明，对于许多类型的模型，模型检查可以有效地用于在开发过程的早期发现错误。特别是，即使非常复杂的模型主要由布尔类型和枚举类型组成，也可以使用基于bdd的模型检查器进行验证。我们研究过的每一个工业系统都有很大的部分，要么满足这一限制，要么通过一些改变来满足这一限制。

对于这类模型，这些工具非常简单，开发人员无需经过大量培训就可以常规使用它们。根据我们的经验，一天的培训和低水平的持续指导通常就足够了。这也使得在开发过程的早期，当模型仍在变化时执行模型检查变得切实可行。

在每个模型修订之后运行一组属性是一种快速而简单的方法，可以查看是否有什么东西被破坏了。我们鼓励我们的开发人员“尽早检查您的模型并经常检查它们”。通过避免单元测试和集成测试期间的返工，花费在模型检查上的时间可以恢复几倍。

由于模型检查检查输入和状态的每一个可能的组合，它在发现设计错误方面也比测试更有效，而测试只能检查一小部分可能的输入和状态。正如CerTA FCS第一阶段案例研究所证明的那样，它也可以比测试更具成本效益。

回到顶部

未来的发展方向

进一步研究的方向有很多。正如CerTA FCS第二阶段研究所表明的那样，数值密集的模型仍然对模型检验提出了挑战。基于smt的模型检查器为这些系统的验证提供了希望，但是需要编写可以通过状态转换关系的归纳来验证的属性，这使得开发人员更难使用它们。

大多数用于生成代码的工业模型都大量使用浮点数。其他模型，特别是那些处理空间关系(如导航)的模型，大量使用三角函数和其他超越函数。使用浮点算法和超越函数来检查系统的有效方法将是非常有用的。

确定必须检查多少属性也很困难。我们的经验是，即使检查几个属性也会发现错误，但是检查更多的属性会发现更多的错误。与开发了许多客观覆盖率标准的测试不同，属性的完整性标准似乎不存在。需要开发或测量一组属性的充分性的技术。

正如CerTA FCS第二阶段案例研究中所讨论的，超大型模型的验证可以通过使用子系统的模型检查和更传统的推理来组成子系统来实现。这种方法将模型检验与定理证明相结合，是一种非常有效的大型系统组成验证方法。

回到顶部

致谢

作者要感谢NASA兰利研究中心的Ricky Butler、Celeste Bellcastro和Kelly Hayhurst，明尼苏达大学的Mats Heimdahl、Yunja Choi、Anjali Joshi、Ajitha Rajan、Sanjai Rayadurgam和Jeff Thompson，罗克韦尔柯林斯的Eric Danielson、John Innis、Ray Kamin、David Lempia、Alan Tribble、Lucas Wagner和Matt Wilding, CMU的Bruce Krogh，空军研究实验室的Vince Crum、Wendy Chou、Ray Bortner和David Homan，以及洛克希德·马丁公司的格雷格·塔伦特和沃尔特·斯托姆，感谢他们的贡献和支持。

这项工作由NASA兰利研究中心根据航空安全计划(AvSP)的NCC-01001合同和空军研究实验室根据先进飞行控制系统认证技术(CerTA FCS)合同[88ABW-2009-2730]部分支持。

回到顶部

回到顶部

回到顶部

回到顶部

回到顶部

回到顶部

数字图书馆是由计算机协会出版的。版权所有©2010 ACM, Inc.

---

没有找到条目