技术文章和通讯

用静态代码分析提高软件质量

作者:Jay Abraham, MathWorks


汽车、航空航天和其他行业的工程师必须确保日益复杂的高完整性软件系统的可靠性和质量。为了尽量减少可能导致灾难性系统故障、伤害或死亡的软件缺陷,许多这些系统的开发都遵循诸如DO-178C、ISO 26262和IEC 61508等标准。

为了提高代码质量,许多开发和测试团队使用Polyspace使用静态代码分析来补充传统的软件验证活动®代码验证器,它使用带抽象解释的形式化方法来验证C、c++或Ada代码。这种方法使工程团队能够:

  • 度量代码的复杂性并验证代码标准的符合性
  • 通过形式化的方法,证明软件不会因为某些类型的运行时错误而失败
  • 执行变更影响分析,以确定一个区域的变更代码如何影响另一个区域的代码的可靠性或功能

使用多空间代码验证器的静态代码分析

静态代码分析自动化耗时且容易出错的手动代码评审过程。与需要执行软件的动态测试不同,静态代码分析直接在源代码上执行,允许在代码准备好集成和测试之前开始质量检查。在分析过程中,Polyspace工具计算复杂性指标,并检查代码是否符合开发标准,包括MISRA C®MISRA c++和JSF++。

Polyspace采用复杂的形式化方法,支持对代码进行深入分析。不太先进的静态分析工具执行基本的检查,例如验证变量是否已初始化,并且更有可能产生假阳性和假阴性。当这些类型的工具不能识别错误时,产生的假阴性会给团队一种错误的安全感,并可能导致在部署软件时错误没有改变。相反,假阳性浪费时间,因为它们迫使团队进行不必要的评审或实现不必要的更改。

因为Polyspace代码验证器基于形式化的方法,可以证明代码没有某些运行时错误,所以它们在需要安全性或可靠性认证的开发项目中特别有价值。认证机构可以检查Polyspace的结果,以验证该软件在数学上已经被证明没有这些错误。

测量代码复杂度和检查编码标准的符合性

在评估高完整性系统中的软件质量时,诸如圈复杂度之类的代码度量提供了一个有价值的视角。通过量化线性无关路径或决策逻辑的数量,这些度量提供了对功能和软件组件复杂性的洞察。Polyspace工具提供圈复杂度和其他代码复杂度度量,工程师可以使用这些度量来评估软件的每个版本。一个基于web的指示板提供了度量的概述,以及对更详细结果的访问。通过为代码复杂度设置阈值,团队可以清楚地看到什么时候某些软件质量目标没有得到满足。

图1。用于跟踪软件质量的基于web的仪表盘。
图1。用于跟踪软件质量的基于web的仪表盘。

编码标准经常解决一些问题,这些问题源于某些语言给予软件开发人员的广泛自由度。像C和c++这样的语言允许非常复杂的编码结构。例如,在C语言中,以下代码对指针进行解引用是有效的:

*****指针= 100;

尽管这行代码可以编译,但调用五次解引用指针的操作的场景不太可能出现,而且容易出现风险。

MISRA建立的编码标准是为了通过消除风险和不明智的复杂代码来提高软件质量。例如,这些标准禁止使用指针访问固定大小的数组,因为这种操作存在向数组边界外的内存进行读写的风险。

Polyspace代码验证器检查是否符合MISRA等代码标准。如果不需要MISRA编码规则的完整集,工程师可以配置Polyspace代码验证器来检查规则的一个子集。Polyspace代码复杂度和代码规则遵从性报告可以用作工件,以支持DO-178C、ISO 26262和其他标准的认证过程。金宝app

证明没有错误

Polyspace工具使用带有抽象解释的形式化方法来确定运行时错误可能发生的位置,并证明源代码中没有这些错误(参见“抽象解释如何工作”)。

在分析过程中,Polyspace代码验证器识别所有可能因运行时错误而失败的代码元素和结构。然后,使用抽象的解释,他们给每个元素分配四种分类之一:红色证明失败,运行时错误;gray-unreachable;绿色证明没有某些运行时错误;或者橙色——未经验证,或者在某些情况下可能失败的代码。一个附加的分类,紫色,用来表示编码规则的违反(图2)。

图2。多元空间验证报告。
图2。多元空间验证报告。颜色编码表示源代码中各个操作的状态。

抽象解释如何起作用

抽象解释是一种形式化的方法,用于从数学上证明源代码没有某些运行时错误,包括算术溢出、除零和越界数组访问。

为了更好地理解抽象解释,考虑下面的数学问题:

(-5477 × 6.82 ÷ 13)2

如果没有计算器,要花些时间才能找到这道题的答案。然而,很明显,答案既不是零,也不是任何负数。在对整个表达式求值之前,就知道了最终结果的一些重要属性。

抽象解释的工作原理与此类似。通过应用定义了分析复杂软件规则的数学定理,它可以精确地确定软件的属性,而无需评估整个问题空间。抽象解释代替了分析程序的每个状态,这对复杂的软件来说是计算上的阻碍,它以数学的形式表示软件的状态抽象就是这样解释确定软件是否满足某些规则或原则,包括那些可用于识别特定运行时错误或证明其不存在的规则或原则。

执行影响分析

了解一个区域的代码更改如何影响另一个区域的代码操作,对于确保更新不会破坏系统的质量至关重要。多元空间代码验证器揭示了新功能或对现有功能的重做将如何影响遗留代码。

例如,假设一个开发团队已经在实时嵌入式系统中确定了那些被证明是可靠的代码元素,以及那些在某些条件下不可访问或可能有问题的元素。在下一个构建中,团队修改了一些现有的功能并添加了新的功能。Polyspace代码验证器可以加速这些更改的分析,例如,使用增量检查来识别原始代码中现在不可访问的任何条件分支。工程师不需要再次检查整个构建,而是可以使用基于web的仪表板来识别编码规则违反、运行时缺陷,以及由于最近的更改而导致的死代码(图3)。

图3。比较当前构建和前一个构建的结果的Web指示板。
图3。比较当前构建和前一个构建的结果的Web指示板。

用静态分析加速开发

多空间代码验证器对于早期识别编码规则违反、运行时缺陷和由代码更改引起的问题是非常宝贵的。与开发后期发现的问题相比,早期发现的问题更容易解决,成本也更低。通过将Polyspace代码验证器集成到开发和测试过程中,团队可以通过将他们的代码审查集中在那些被确定为未经验证或无法到达的领域来进一步加速开发。此外,他们可以通过提交Polyspace结果作为构件来简化DO-178C、ISO 26262或IEC 61508认证过程,以获得认证机构所需的验证活动的学分。Polyspace代码验证者可使用认证和资格验证套件,促进Polyspace结果在必须满足认证标准的项目中使用。

发布于2012 - 92063v00

查看相关功能的文章

查看相关行业文章