Accelerating the pace of engineering and science

Polyspace Code Prover

主要特性

  • 可证明 C 和 C++ 代码中不存在某些运行时错误
  • 直接以代码颜色来区分运行时错误
  • 计算变量和函数返回值的范围信息
  • 识别超出指定范围限制的变量
  • 计算各种质量指标用于跟踪是否符合软件质量目标
  • 提供网络控制面板显示代码指标和质量状态
  • 审核检查流程向导帮助分析结果和运行时错误状态
  • 以图形化方式显示变量的读取和写入
Run-time error results displayed by Polyspace Code Prover.
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 结合使用,可以查找缺陷并检查代码是否符合编码标准。这两款产品一起提供了可用于早期开发阶段的端到端静态分析功能,包括缺陷查找、代码规则检查和验证。该功能确保了嵌入式软件的可靠性,符合最高水平的质量和安全性要求。

借助 Parallel Computing Toolbox™MATLAB Distributed Computing Server™ ,您可以加速代码验证,将验证任务分发至计算机集群。

检测运行时错误

Polyspace Code Prover 将抽象释义与静态代码分析结合使用,以识别和诊断溢出、被零除和指针越界等运行时错误。这项技术可以完整而全面验证所有运行时情况,并为每项代码自动提供诊断报告,包括已证明、已失败、无法达到或未经证明诊断。在 Polyspace Code Prover 生成的验证结果中,每一项 C 或 C++ 运算均采用颜色编码表示其状态:

绿色: 已证明没有运行时错误
红色:已证明在每次运行时都有错误
灰色:已证明无法达到(可能表示存在功能性问题)
橙色:未经证明,在某些情况下可能有错

Color-coded run-time error attributes identified by Polyspace Code Prover.

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

检测到的错误包括:

  • 溢出、下溢、被零除和其他运算错误
  • 数组访问超出边界和非法引用指针
  • Always true/Always false 语句
  • 未初始化的类成员 (C++)
  • 读取对未初始化数据
  • 访问空 this 指针 (C++)
  • 死代码
  • 与对象编程、继承和异常处理有关的动态错误 (C++)

查看范围信息

Polyspace Code Prover 跟踪整个代码的控制逻辑和数据流,并显示与变量和运算符相关联的范围信息。将光标放到运算符或变量上,便会有一条提示消息显示范围信息。形式化方法又称为抽象释义,可以确定精确的范围信息,以便证明软件是否存在某些运行时错误。您可以使用这种范围信息来调试软件,确保某些变量或运算不违反指定的范围限制。

在下面的示例中,Polyspace Code Prover 已确定除法运算左侧操作数的范围是 -1701 至 3276;右侧操作数是 9。除后的结果范围是 -189 至 364。

Tooltip displaying the possible ranges for all run time conditions.
工具提示显示所有运行条件的可能范围。

您可以使用调用层次结构和调用流程图来进一步来显示控制流。

Call flow graph displaying the order of function calls in an interprocedural analysis.

在某过程间分析中的函数调用顺序。

跟踪软件质量指标

您可以定义一个集中式的质量模型,来跟踪运行时错误、代码复杂度和编码违规。使用这些指标,可以在代码从首次迭代到最终交付的完善过程中,持续跟踪预定义的软件质量目标。通过衡量代码质量改进率,Polyspace Code Prover 使开发人员、测试人员和项目经理能够致力于编写和交付高质量的代码。

Software quality metrics displayed via web browser.

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

依据代码验证结果回溯至 Simulink 模型

您可以使用 Polyspace Code Prover 验证生成的代码或混合代码(后者包含生成的代码和手写代码)。自动生成的代码的代码级缺陷检测结果会回溯至 Simulink 型。您可以识别模型的可靠部分;更正导致代码错误的设计问题。您还可以识别生成的代码与手写代码之间接口的潜在问题。例如,将手写 S 函数代码与生成的代码混合,可能因接口信号范围不当而产生运行时错误。

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

Tracing code verification results to the Simulink model.

将代码验证结果回溯至 Simulink 模型。

实现代码验证流程自动化

通过将 Polyspace 整合到构建流程中,您可以将 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 以及其他格式。。

DO Qualification Kit contents.

提供认证和审核工具包。

Understanding Compliance to the MISRA C 2012 Coding Guidelines

观看网上技术交流会录像