Polyspace Code Prover

 

Polyspace Code Prover

证明软件中不存在运行时错误

证明不存在严重的运行时错误

根据所有可能的输入,在不执行代码的情况下分析所有代码路径。识别无论运行时条件如何都永远不会遇到运行时错误的语句,并找出其他需要注意的语句。

改进软件设计和代码理解

检查 C/C++ 代码中的控制流和数据流,查看与变量和运算符相关联的范围信息。

优化软件性能

通过识别安全可靠的运算(如除以零和溢出)来删除防御性代码。检测无法通过任何执行路径到达的代码分支。找出逻辑和程序结构中的错误,删除它们以减少内存占用。

分析全局变量用法

减少调试全局变量(包括任务或线程共享的变量)的读/写操作所花费的时间。
使用并发访问图了解可能导致数据竞争问题的控制流和数据流。识别未使用的全局变量以进行代码优化。

认证支持

创建完成行业标准认证过程所需的交付物。经 TÜV 南德认证,符合 IEC 61508 和 ISO 26262 标准。使用为 DO-178C 流程准备的报告和交付物。

Simulink 和 Stateflow 集成

对生成的代码运行分析,并将您的发现追溯到源 Simulink 模型模块和 Stateflow 图。从 Simulink 环境中启动 Polyspace® 分析。

在桌面端进行交互式分析

对整个或部分软件项目运行静态代码分析。使用桌面工具生成报告,并对结果进行审核和分类。
使用类似调试器的视图步进运行时错误之前的每个语句,以找到复杂 Bug 的根本原因。组织和配置您的项目。Polyspace Code Prover 原生支持 60 多种 C 和 C++ 编译器,以及自动设置从项目的编译系统中提取的 Polyspace 分析。

静态应用程序安全性测试

证明不存在严重的安全漏洞,例如缓冲区溢出、内存访问溢出和数值溢出。通过在不执行代码的情况下分析所有代码路径和输入下的代码,减少对模糊测试的需求。

影响分析

正式跟踪和验证指定的全局或局部变量对其他变量或特定语句的影响。执行信号分析以满足 CARB 对 OBD 相关软件的要求,证明在满足 ISO 26262 标准的同时不受干扰,并分析标定参数的影响。在软件安全方面,执行污点分析和跟踪敏感数据流。

有兴趣了解 Polyspace Code Prover?