简介
　　在当今众多的行业中，软件是应用的基础。飞机、汽车、工业机械和医疗器械中都包含所谓的嵌入式软件之类的各种专用软件。这种软件直接负责执行各种关键任务，因此必须具有高质量，而且必须经过全面的测试以验证其是否如期执行。
　　在这类关键的系统中控制工程网版权所有，即便是使用软件执行简单操作也可能具有风险。不妨以一个需要加法运算的算法为例，如果底层的 32 位微控制器没有浮点单元，则需谨慎设计，以免发生溢出情况。请看以下代码中的运算：
　　int32_t a控制工程网版权所有, b, c;  /* declare signed 32bit integer variables */
　　…
　　c = a + b;  /* add variables */
　　由于可能发生溢出，c = a + b 运算容易产生风险。如果求和生成的结果大于 231-1，结果将不适合 32 位变量 c，从而导致求和不正确。但微处理器并不发出导致软件行为不正常的错误或警报。
　　软件开发人员和验证工程师需要对其制作的软件的质量负最终责任。尽管开发人员可以采用各种人工方式来量化软件的质量，但这些方式并非一应俱全。自动化工具则可以提供更统一且在某些情况下更加强大的技术来制作出高质量的软件，一项名为静态代码分析的自动化技术便是其中之一。
　　静态代码分析
　　静态代码分析也称为源代码分析或静态分析，是一种用于分析源代码质量和可靠性的软件验证活动。这种分析使得软件开发人员和测试人员能够识别并诊断溢出、被零除和非法间接引用指针等错误。通过静态代码分析生成的指标提供了一种衡量和提升软件质量的方法。与其他验证技术相反，执行静态代码分析无需执行程序、开发测试用例或编译软件程序。
　　您可以将静态代码分析视为一个超级强大的代码复查过程，在此过程中会分析代码执行路径，理解变量范围并通过演绎方法了解变量的并行访问路径。
　　静态代码分析工具的开发方式有多种，其中包括代码样式检查等简单检查到复杂的形式化方法等。简单的静态代码分析技术可生成能够表明软件质量的指标，或尝试识别软件程序中的错误。这些简单的技术非常快速，可迅速产生结果，但是也会出现漏报和误报。如果出现漏报，静态代码分析程序就会遗漏源代码中真正的错误。误报则是错误地识别出的错误。对于软件开发人员和验证工程师来说控制工程网版权所有，这两种情况都是有问题的。漏报会使人误以为无错而沾沾自喜，而发布的产品中却含有缺陷。误报会延迟软件的制作，并造成不必要的返工，从而可能会降低软件的性能或软件的内存占用。
　　下面的示例显示的是简单的静态代码分析技术的应用。请看以下代码段：
　　int32_t a控制工程网版权所有, b; /* declare variables */
　　a = 0;
　　b = 12/a;  /* divide operation */
　　简单的静态代码分析技术会快速发现运算 b = 12/a 中的被零除的错误。编译程序会识别此错误并在编译时对其进行标记。现在看看下面一段复杂的代码：
　　int32_t main_func (int32_t x, int32_t y) { /* x and y are full range values */
　　int32_t a控制工程网版权所有, b, c;
　　a = function1(x); /* function 1 and 2 may return */
　　b = function2(y); /* full range values          */
　　c = b/a;  /* divide operation */
　　return c;
　　}
　　让我们假设 function1 和 function2 会执行复杂的算法和数学计算。在这种情况下，c = b/a 运算很可能会发生被零除的情况，但简单的静态代码分析技术不一定能识别出这种情况是否会发生以及会在什么情况下发生。它们最多只能指出可能发生被零除的情况，但无法确切地说明什么条件下会发生这种情况。如果被零除的情况实际上不会发生，这种情况就称为误报。
　　形式化方法简介
　　现代的静态代码分析将形式化方法与查错技术融为一体。采用这种方法的工具不仅会尝试发现源代码中的错误，而且它们会尝试证明不存在某些重大错误。形式化方法可应用理论计算机科学基础知识来解决软件中的难题。形式化方法技术的一个示例是抽象释义CONTROL ENGINEERING China版权所有，这是一种严格的数学方法，用于证实软件中不存在可检测到的运行时错误。
　　抽象释义依赖于广泛数学理论基础，用以定义各种复杂的动态系统的分析规则。抽象释义能够以更一般的形式来表示程序的状态并提供相应的处理规则CONTROL ENGINEERING China版权所有，而不是分析程序的每个状态。要获得抽象的数学解释，需要分析软件程序的语义。不过这种想法并不算新颖，而是源自于 20 世纪 70 年代发展的理论。最初实施而产生的算法令代码的大小成指数增长。更为新颖的算法解决了这种指数增长的问题，而当运行在当今的处理器上时，就使形式化方法的应用更为实用。
　　下面等式中的三角运算有助于解释抽象释义。请看下面的弧度方程，其中 x 为实数：
　　y = sin(2.14) + cos(0.53) + x2
　　对于给定值 x，不借助计算器而以手工方式来求取该方程的解并非易事。然而，如果问及计算的正负，您可以应用三角和代数的法则获得结果为正。这是正确的，因为对于 x<pi，sin(x) >0；而对于 x<pi/2，cos(x) > 0。因此，该方程的值始终为正实数，而结果既不为负也不为零。您可以使用三角法则准确地确定该方程的某些属性，无需了解全部细节便可正确地阐明真实的结果。
　　您可以借助上述抽象原则将抽象释义用于静态代码分析，以识别和诊断溢出、被零除和指针越界等运行时错误。由此过程生成的指标则可提供一种衡量和提升软件质量的方法。如果利用抽象释义来检测运行时错误，则可以完整而全面地针对每项运算来提供"已证明"、"已失败"、"无法访问"、"未经证明"等诊断。
　　基于形式化方法的静态代码分析示例
　　将形式化方法用于抽象释义的静态代码分析工具示例是 MathWorks 的 Polyspace? 代码验证工具。此代码验证工具可使用以 C、C++ 或 Ada 编程语言编写的源文件，以识别何处会发生某种运行时错误并证明其不存在。验证过程首先从识别源代码文件中可能因运行时错误而失败的地方开始。然后该工具会使用抽象释义将所有错误分类为"未经证明"，接下来尝试证明代码会失败、无法访问或证明不会失败。该工具可使用图 1 中所示的颜色编码方案来识别代码中运算的状态。

图 1：Polyspace 颜色编码显示代码中运算的状态，工具提示显示变量范围信息。

　　以绿色标示的代码元素已经过证明不存在溢出、被零除和非法间接引用指针等运行时错误，以及其他运行时错误。以红色标示的运算显示 Polyspace 已检测到运行时错误的地方。在某些情况下可能会失败的运算被标为橙色。无法执行的代码元素或条件分支（不活动代码或无法访问的代码）则标为灰色。
　　接下来，请看 Polyspace 如何分析之前显示的代码段的结果。如图 2 所示，Polyspace 会将除运算标记为绿色，表示此代码运算将不会导致被零除错误（因为变量 a 的范围为 43…727，而绝不会为零）。详细的过程间静态代码分析可通过抽象释义来确定此变量绝不会等于零。

图 2：Polyspace 结果。

　　结论
　　通过形式化方法（抽象释义）强化的静态代码分析可以用作提升高完整性软件系统中使用的嵌入式软件质量的重要工具。涉及此类静态代码分析工具的软件开发过程有助于改进相应过程。采用这种方法可以帮助软件开发人员和验证工程师评估其软件产品的质量和安全性。
　　作者简介：
　　Jay Abraham 是负责 Polyspace 代码验证产品的产品营销经理。其专长领域是用于验证重要嵌入式应用程序的软件工具。他有着 20 年的工作经验，期间在 Magma Design Automation 和 Wind River Systems 等开发硬件、软件工具和嵌入式操作系统的公司从事工程和设计；他的第一份工作是在 IBM 担任微处理器设计师。Jay 拥有雪城大学计算机工程学学士学位和波士顿大学电子工程学硕士学位。