汽车、航空航天和其他行业的工程师必须确保日益复杂的高完整性软件系统的可靠性和质量。为了最小化可能导致灾难性系统故障、伤害或死亡的软件缺陷，许多此类系统的开发都由诸如DO-178C、ISO 26262和IEC 61508等标准进行管理。
为了提高代码质量，许多开发和测试团队使用Polyspace进行静态代码分析，以补充传统的软件验证活动®代码验证器，它使用带有抽象解释的形式方法来验证C、c++或Ada代码。这种方法使工程团队能够:
- 度量代码复杂度并验证代码标准的符合性
- 通过正式的方法证明，软件不会因为某些类型的运行时错误而失败
- 执行更改影响分析，以确定更改一个区域的代码如何影响另一个区域的代码的可靠性或功能
多空间码验证器的静态码分析
静态代码分析自动化耗时且容易出错的手动代码审查过程。与需要执行软件的动态测试不同，静态代码分析直接在源代码上执行，使质量检查能够在代码准备好集成和测试之前开始。在分析期间，Polyspace工具计算复杂性度量并检查代码是否符合开发标准，包括MISRA C®， MISRA c++和JSF++。
Polyspace采用了复杂的形式方法，可以对代码进行深入分析。不太高级的静态分析工具执行基本的检查，例如验证变量是否已初始化，并且更有可能产生假阳性和假阴性。当这些类型的工具无法识别错误时，产生的假阴性会给团队一种错误的安全感，并可能导致软件的部署不带错误。相反，假阳性会浪费时间，因为它们迫使团队进行不必要的审查或实现不必要的更改。
因为Polyspace代码验证器基于正式的方法，并且可以证明代码没有某些运行时错误，所以它们在需要安全或可靠性认证的开发项目中特别有价值。认证机构可以审查Polyspace的结果，以验证该软件在数学上已被证明没有这些错误。
衡量代码复杂度和检查代码标准的遵从性
代码度量，例如圈复杂度，在评估高完整性系统中的软件质量时提供了有价值的视角。通过量化线性独立路径或决策逻辑的数量，这些指标提供了对功能和软件组件复杂性的洞察。Polyspace工具提供了圈复杂度和其他代码复杂度指标，工程师可以使用这些指标来评估软件的每个版本。基于web的仪表板提供了指标的概述，以及访问更详细的结果。通过为代码复杂度设置阈值，团队可以清楚地看到什么时候没有达到某些软件质量目标。
编码标准经常处理某些语言赋予软件开发人员的广泛范围所产生的问题。像C和c++这样的语言允许非常复杂的编码结构。例如，在C语言中，以下解引用指针的代码是有效的:
* * * * *指针= 100;
虽然这行代码可以编译，但是调用一个指针解引用五次的操作的场景是不太可能的，而且风险更大。
诸如MISRA建立的编码标准是为了通过消除风险和不适宜的复杂代码来提高软件质量而开发的。例如，这些标准禁止使用指针访问固定大小的数组，因为该操作存在从数组边界外的内存中读取或写入的风险。
Polyspace代码验证器检查是否符合代码标准，如MISRA。如果不需要完整的MISRA编码规则集，工程师可以配置Polyspace代码验证器来检查规则的一个子集。Polyspace代码复杂性和代码规则遵从性报告可以用作工件，以支持DO-178C、ISO 26262和其他标准的认证过程。万博1manbetx
证明没有错误
Polyspace工具使用带有抽象解释的形式方法来确定运行时错误可能发生的位置，并证明源代码中没有这些错误(参见“抽象解释如何工作”)。
在分析过程中，Polyspace代码验证器识别所有可能由于运行时错误而失败的代码元素和结构。然后，使用抽象的解释，他们将每个元素划分为四种分类中的一种:red-proven fail with a runtime error;gray-unreachable;green被证明没有某些运行时错误;或未经验证的代码，或在某些情况下可能失败的代码。另一种分类(紫色)用于表示编码规则违反(图2)。
抽象解释的工作原理
抽象解释是一种形式的方法，用于从数学上证明源代码不存在某些运行时错误，包括算术溢出、除零和超出边界的数组访问。
为了更好地理解抽象解释，考虑以下数学问题:
(-5477 × 6.82 ÷ 13)2
如果没有计算器，要找出这道题的答案就得花些时间。然而，显而易见的是，答案既不是零，也不是任何负数。在对整个表达式求值之前，最终结果的一些重要性质是已知的。
抽象解释也是如此。通过应用定义分析复杂软件规则的数学定理，它可以在不评估整个问题空间的情况下精确地确定软件的性质。对于复杂的软件来说，分析程序的每个状态可能成为计算上的禁忌，而抽象解释则用数学的方式表示软件的状态抽象,然后解释确定软件是否满足某些规则或原则，包括那些可用于识别特定运行时错误或证明它们不存在的规则或原则。
执行影响分析
理解一个区域的代码更改如何影响另一个区域的代码操作，对于确保更新不会破坏系统的质量至关重要。Polyspace代码验证器揭示了新功能或对现有功能的重做将如何影响遗留代码。
例如，假设一个开发团队已经在一个实时嵌入式系统中确定了那些被证明是可靠的代码元素，以及那些在某些条件下不可访问或可能存在问题的元素。在下一个版本中，团队修改了一些现有的功能并添加了新的功能。Polyspace代码验证器可以加速对这些更改的分析，例如，使用增量审查来识别原始代码中现在无法访问的任何条件分支。工程师可以使用基于web的仪表板来识别编码规则违反、运行时缺陷和最新更改导致的死代码，而不是重新检查整个构建(图3)。
用静态分析加速开发
Polyspace代码验证器对于早期识别代码规则违反、运行时缺陷和代码更改引起的问题非常有用。与开发后期发现的问题相比，早期发现的问题更容易解决，成本也更低。将Polyspace代码验证器集成到开发和测试过程中，团队可以通过将代码审查集中在那些被确定为未经验证或不可访问的区域，从而进一步加速开发。此外，他们还可以简化DO-178C、ISO 26262或IEC 61508认证过程，将Polyspace结果作为工件提交，以获得认证机构所需的验证活动的信用。Polyspace代码验证者可获得认证和资格认证套件，方便Polyspace结果用于必须符合认证标准的项目。
