主要特性

  • 检验 C 和 C++ 代码中是否存在某些运行时错误
  • 直接在代码中使用颜色编码指示运行时错误
  • 计算变量和函数返回值的范围信息
  • 识别超出指定范围限制的变量
  • 跟踪是否符合软件质量目标的质量指标
  • 提供代码指标和质量状态的基于 Web 的仪表板
  • 用于结果和运行时错误状态分类的向导式审核检查流程
  • 以图形化方式显示变量的读取和写入

Polyspace Code Prover 显示的运行时错误结果。


验证 C 和 C++ 嵌入式软件

Polyspace Code Prover 执行 C 和 C++ 嵌入式软件的代码验证,该嵌入式软件需要执行最高质量和安全等级。它是一款可靠的静态分析工具,其使用一种被称为抽象解释形式化方法技术生成可靠的验证结果。Polyspace Code Prover 可识别出可能出现运行时错误的位置以及经过证实不存在运行时错误的代码。您可以将 Polyspace Code Prover 用作高质量保证流程的一部分,从而对输入值、路径和变量值之间所有可能的组合进行穷尽的验证。Polyspace Code Prover 使用颜色编码来指示代码中每个元素的状态。它与 Simulink® 进行集成,从而将代码级运行结果追溯回 Simulink 模型。

您可以借助 Polyspace Code Prover 执行以下操作:

  • 检验代码 — 验证代码中是否存在运行时错误
  • 获取无漏报结果 — 全面识别出所有潜在的运行时错误
  • 对代码的质量充满信心 — 度量已检验和未经过检验的代码

您可从命令行、图形用户界面或通过 Visual Studio® 和 Eclipse™ 插件访问 Polyspace Code Prover。您可以将其用于支持软件开发流程中的所有关键活动,包括:

  • 检测被零除等运行时错误
  • 检验是否存在缓冲区溢出等危及安全的运行时错误
  • 确定变量的范围并确保符合范围限制
  • 确保达到适当的软件质量目标
  • 将运行时错误追溯到 Simulink 模块或 IBM® Rational® Rhapsody® 模型
  • 创建认证套件

Polyspace Code Prover 与 Polyspace Bug Finder 协作,以查找源代码中被零除或危及安全的缓冲区溢出等关键性安全缺陷,并检查是否符合 MISRA 等编码规范。这些产品为早期开发提供端到端的静态分析功能,包括错误查找、编码规范检查和运行时错误的检验。该功能确保了必须按照最高质量和安全等级运行的嵌入式软件的可靠性。

您可利用 Parallel Computing Toolbox™MATLAB Distributed Computing Server™ 提交验证作业,以加快验证的速度并将代码验证作业分载到计算机群集上。


检测运行时错误

Polyspace Code Prover 将抽象解释用于静态代码分析,以检验、识别和诊断运算溢出、被零除和缓冲区溢出等运行时错误。该技术可完整全面地验证所有可能的运行条件,并自动为每项代码运算提供“已证明”、“存在缺陷”、“不可达”、“未经证明”诊断。在 Polyspace Code Prover 生成的验证结果中,每一项 C 或 C++ 运算都用颜色编码,以指示其状态:

绿色: 经过证实不存在运行时错误
红色: 经过证实每次执行运算时都存在缺陷
灰色: 经过证实不可达(可能表示功能问题)
橙色: 未经证实的运算,可能在某些条件下存在缺陷

检测出的错误包括:

  • 算术溢出、下溢、被零除和其他算术错误
  • 缓冲区溢出和非法解除引用指针
  • 总是 True/False 的语句
  • 未初始化的类成员 (C++)
  • 读取访问未初始化的数据
  • 访问空指针 (C++)
  • 死代码
  • 与对象编程、继承和异常处理相关的动态错误 (C++)

Polyspace Code Prover 识别出的运行时错误属性。


查看范围信息

Polyspace Code Prover 可跟踪软件中的控制和数据流并显示与变量和运算符相关的范围信息。将鼠标置于运算符或变量上,便会显示说明范围信息的提示框。称为抽象解释形式化方法可准确确定范围信息,从而证明软件不存在某些运行时错误,如被零除和缓冲区溢出。您可使用此范围信息准确跟踪控制和数据流,以调试软件或确保某些变量或运算不违反指定的范围限制。

在以下示例中,Polyspace Code Prover 确定出除法运算的左侧操作数介于 -1701 到 3276 之间,右侧操作数为 9。进行除法运算后得出的结果范围为 -189 到 364。

可使用调用层次结构和调用流图形将控制流进一步可视化,或查看全局变量数据的访问情况

Explore gallery (3 images)


跟踪软件质量指标

您可定义一个集中质量模型来跟踪运行时错误、代码复杂度,以及编码违规情况。使用这些指标,您可以在从第一次迭代到最终交付版本的代码演化过程中跟踪达到预定义的软件质量目标的进度。通过测量代码质量的改进速度,Polyspace Code Prover 使开发人员、测试人员和项目经理能够确定目标并交付高质量代码。

通过 Web 浏览器显示的软件质量指标。


可使用 Polyspace Code Prover 验证生成的代码或混合代码(同时包含自动生成代码和手写代码)。自动生成的代码中产生的代码级缺陷可追溯到 Simulink 中的模型。您可以确定模型的哪一部分是可靠的,然后纠正会导致代码中的错误的设计问题。还可以确定生成的代码与手写代码的接口之间的潜在问题。例如,将手写的 S-Function 代码与生成的代码混合在一起可能导致一个问题,即接口中不正确的信号范围导致运行时错误。

Polyspace Code Prover 还支持将运行时结果追溯到 dSPACE® TargetLink® 模块和 IBM Rational Rhapsody 模型。

将代码验证结果追溯到 Simulink 模型。


自动化代码验证流程

可将 Polyspace Code Prover 整合到构建过程中,将其用作持续集成流程的一部分。您可以自动调度验证作业并设置电子邮件通知。可以指派 Polyspace Code Prover 将验证作业发布到集群计算机上(使用 MATLAB Distributed Computing Server),并在结果生成后收到电子邮件提醒。结果包含与上一版本代码相比的不同之处,这是服务器自动计算出的。

您可定义这些分析的频率、需要用于代码库特定部分的质量模型以及用户接收生成结果的电子邮件地址。此外,还可以定义自动验证需要涵盖构建过程的哪些特性。


创建认证套件

您可以在认证过程中结合使用 Polyspace Bug Finder 和 Polyspace Code Prover 与 IEC Certification Kit(符合 IEC 61508 和 ISO 26262)DO Qualification Kit(符合 DO-178B),对基于这些行业标准的项目进行认证。

报告和认证结果显示代码的最终质量,突出显示已经审查的部分,生成代码指标,并记录编码规则的应用和运行时错误状态。可采用多种格式创建这些报告,如 PDF、HTML、RTF 等。

现已提供 Certification Kit 和 Qualification Kit。