提高嵌入式软件质量

操作应用于安全苛刻的航空和军事领域的嵌入式软件时必须高度关注安全问题。为达到可靠性目标，软件开发团队精益求精，力争使这些软件应用符合严格的验证流程并实现零缺陷目标。Edsger Dijkstra有句名言：测试只能发现错误，但不能证明错误不存在。如果测试无法证明不存在严重的运行错误，那么嵌入式软件开发团队如何才能确定其软件没有这些错误呢？基于数学证明的代码验证是值得一试的解决方案。在软件验证方面，可扩展的高性能数学技术在实际应用方面的最新发展十分有用，可实现对软件中不存在运行时错误进行证明。

航空领域的软件应用

高集成系统中的嵌入式软件日益复杂。在军事领域中，用于F-22猛禽战斗机的航空电子软件由170万行代码组成，用于F-35联合攻击战斗机的航空电子软件预计有570万行代码。对于商务班机，波音787飞机飞行控制系统将有大约650万行代码。软件内容不断膨胀，飞机复杂性不断增加，使发生故障的风险也不断加剧，从而使获得高度可信性软件的过程复杂无比。

软件故障风险

研究以往发生的嵌入式设备故障对于理解代码相关的问题大有裨益。例如，一次性使用火箭在测试飞行期间发生的故障归根于代码缺陷。在这种特殊情况下，发射器在发射后不到一分钟的时间内自毁，原因在于：攻角超过规定的安全限度，导致发射器遭遇高气动载荷。

事后调查揭露了故障的根本原因：溢出导致嵌入式软件发生运行错误。在将一个64位浮点数转换为16位有符号整数时，一对决定火箭姿态和位置的冗余惯性参考系统中产生溢出，从而将火箭喷管移到了极端位置。冗余系统的存在不起作用，因为备用系统也发生了同样的问题。

如上所述的运行时错误代表一类特定的软件错误，称作潜伏性故障。这类故障位于代码中，但是除非在特殊条件下运行特定测试，否则在系统测试期间无法检测到这些故障。因此，这些代码表面上能正常运行，但实际上会导致意外的系统故障。以下为若干运行时错误示例：数据未初始化；数组访问越界；空指针解引用；溢出和下溢；计算错误；同时访问共享数据；非法类型转换。

高集成软件验证

按照传统方法，源代码级软件验证涉及代码检查、静态分析和动态测试。每种方法都有缺点。

代码检查仅依赖于检察人员的专业技术，若有大量代码需要检查，则会是一项繁琐的工作。传统的静态分析技术主要依靠模式匹配方法检测不安全的代码模式，但无法证明不存在运行时错误。随着嵌入式软件日益复杂，对所有操作条件进行动态测试已经不太可能，这进一步证明了Edsger Dijkstra的观点：测试只能发现错误，但不能证明错误不存在。

一种新的验证方法称为抽象解释，它以静态分析为基础，使用形式化数学证明，可发现某些运行时错误或证明它们不存在。抽象解释可直接应用于源代码，而无需执行代码。

抽象解释和基于证明的验证方法作为一种基于证明的验证方法，通过在以下问题中将三个大整数相乘可对抽象解释进行说明：–4586×34985×2389=？

虽然手动计算此问题的答案很费时，但是我们可以应用乘法法则确定答案的符号为负。确定此计算的符号就是抽象解释的一种应用。这种技巧使我们不需要对整数执行完成的乘法计算就能够准确地知道最终结果的一些属性，例如符号。利用乘法法则，我们还知道此计算的结果符号不可能为正。采用类似方式可将抽象解释应用到软件符号学中，以证明软件的某些属性。不执行程序本身，

通过验证源代码的某些动态属性，抽象解释在传统静态分析技术和动态测试之间架起桥梁。抽象解释在单个阶段中调查程序的所有可能行为，即所有可能值的组合，以确定如何以及在何种条件下程序会产生某些类别的运行时故障。由于抽象解释与考虑中的操作相关，我们可以用数学方法证明该技术能预测正确的结果，因此它得出的结果被认为是可靠的。

使用抽象解释验证软件

抽象检查可用作静态分析工具，检测并用数学方法证明源代码中不存在某些运行时错误，如溢出、除以零以及数组访问超出边界等。执行此验证无需执行程序、代码插装或测试用例。MathWorks Polyspace代码验证产品使用的便是此类静态分析。向Polyspace产品输入C、C++或Ada源代码。Polyspace产品首先检查源代码，以确定可能出现潜在运行时错误的位置。然后它会生成一份报告，该报告使用颜色编码表示代码中各元素的状态，如图1和表1所示。

图1 Polyspace颜色编码

表1：颜色编码

标为绿色的Polyspace结果表示代码中不存在某些运行时错误。在检测到运行时错误且代码显示为红色、灰色或橙色的情况下，软件开发人员和测试人员可使用验证流程中生成的信息修复发现的运行时错误。