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

获取试用版软件

Comprehensive Static Analysis Using Polyspace Products

观看网上技术交流会录像