汽车，航空航天和其他行业的工程师必须确保越来越复杂的高完整性软件系统的可靠性和质量。为了最大限度地减少可能导致灾难性系统故障，伤害或死亡的软件缺陷，许多这些系统的发展受到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和其他标准的认证过程。金宝app
证明没有错误
Polyspace工具使用带有抽象解释的形式方法来确定运行时错误可能发生的位置，并证明源代码中没有这些错误(参见“抽象解释如何工作”)。
在分析过程中，Polyspace代码验证器识别所有可能由于运行时错误而失败的代码元素和结构。然后，使用抽象的解释，他们将每个元素划分为四种分类中的一种:red-proven fail with a runtime error;gray-unreachable;green被证明没有某些运行时错误;或未经验证的代码，或在某些情况下可能失败的代码。另一种分类(紫色)用于表示编码规则违反(图2)。
如何抽象解释作品
摘要解释是一种用于数学上的正式方法，该方法证明源代码没有某些运行时错误，包括算术溢出，划分为零和缺失的数组访问。
要更好地了解抽象解释，请考虑以下数学问题：
（-5477×6.82÷13）2
没有计算器，需要一些时间来找到这个问题的答案。但是，它立即显而易见的是，答案既不是零也不是任何负数。在评估整个表达之前，最终结果的一些重要特性是已知的。
抽象解释也是如此。通过应用定义分析复杂软件规则的数学定理，它可以在不评估整个问题空间的情况下精确地确定软件的性质。对于复杂的软件来说，分析程序的每个状态可能成为计算上的禁忌，而抽象解释则用数学的方式表示软件的状态抽象那就是解释要确定软件是否满足某些规则或原则，包括可用于识别特定运行时错误或证明其缺席的规则或原则。
执行影响分析
理解一个区域的代码更改如何影响另一个区域的代码操作，对于确保更新不会破坏系统的质量至关重要。Polyspace代码验证器揭示了新功能或对现有功能的重做将如何影响遗留代码。
例如，假设开发团队在实时嵌入式系统中发现了这些代码元素，这些系统被证明可靠，以及在某些条件下无法访问或潜在问题的元素。在下一个构建中，该团队修改了一些现有功能并添加了新功能。PolySpace Code Verifiers使用增量审查，可以加速分析这些更改，例如，识别现在无法访问的原始代码中的任何条件分支。工程师不能再次审查整个版本，而是可以使用基于Web的仪表板来识别从最近更改的编码规则违规，运行时缺陷和死亡代码（图3）。
用静态分析加速开发
Polyspace代码验证器对于早期识别编码规则冲突、运行时缺陷和代码更改引起的问题非常有用。与开发后期发现的问题相比，早期发现的问题更容易解决，成本更低。通过将多空间代码验证集成到开发和测试过程中，团队可以通过将代码审查集中在那些被确定为未经验证或无法访问的领域，进一步加快开发。此外，他们可以通过将Polyspace结果作为工件提交，以获得认证机构要求的验证活动的信用，从而简化DO-178C、ISO 26262或IEC 61508认证过程。Polyspace代码验证器可使用认证和资格鉴定工具包，方便将Polyspace结果用于必须符合认证标准的项目。
