Polyspace Code Prover

重要更新

 

Polyspace Code Prover

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

Polyspace Code Prover 是一款可靠的静态分析工具,可以证明在 C 和 C++ 源代码中不存在溢出、被零除、数组访问越界和其他运行时错误。不需要执行程序、代码插装或测试用例即可产生结果。Polyspace Code Prover 使用基于形式化方法的语义分析和抽象解释,验证软件进程间、控制流和数据流行为。您可以用它来验证手写代码、生成的代码或两者的组合。每个代码语句都有颜色编码,表明是否无运行时错误、证明有缺陷、不可达或未经证明。

Polyspace Code Prover 显示变量和函数返回值的范围信息,并且可以证明哪些变量超出指定范围限制。代码验证结果可用来跟踪质量指标,并检查是否符合您的软件质量目标。Polyspace Code Prover 可与 Eclipse™ IDE 配合使用,在您的桌面上验证代码。

通过 IEC Certification Kit(符合 ISO 26262 和 IEC 61508)和 DO Qualification Kit(符合 DO-178),可提供对行业标准的支持。

使用形式化数学验证代码

实现无漏报的高质量水平和高安全级别

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

识别无论运行时条件如何都永远不会遇到运行时错误的 C/C++ 和 Ada 代码

检测运行时错误

检测其他测试手段无法找出的错误

根据所有可能的输入,在不执行代码的情况下分析所有代码路径。

调用层次结构。

理解和改进代码

减少在代码审查、调试和鲁棒性测试上花费的时间。

了解问题的根本原因并改进设计

检查通过软件的控制流和数据流,查看与变量和运算符相关的范围信息。

显示所有运行时条件下可能范围的提示框。

防止非预期软件行为

查找通过任何执行路径都无法访问的所有代码段以及逻辑和程序结构上的错误。

查找死代码。

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

对生成的代码运行验证,并将验证结果追溯到 Simulink 中的源模型块。

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

利用 Polyspace Code Prover Server 自动进行代码验证

通过尽早、经常对代码变更进行分析,实现持续集成。

自动化代码验证流程

使用 Polyspace Code Prover Server™, 在带有构建自动化工具(如 Jenkins 和 Bamboo)的服务器级机器上运行 Polyspace Code Prover 静态分析引擎。

自动化代码验证流程。

通知并上传结果以供协同审查

将缺陷自动分配给组件所有者,发送电子邮件通知,并将结果上传到 Polyspace Code Prover Access,以便鉴别和解决问题。

发送附带 Polyspace Code Prover 结果的电子邮件通知。

借助 Polyspace Code Prover Access 进行协同审查

与软件开发团队共享验证结果和质量指标。

查看 Polyspace Code Prover 结果以鉴别和解决问题

Polyspace Code Prover Access™ 提供 Web 浏览器界面,以便查看存储在中央存储库中的 Polyspace 代码验证结果和质量指标。 使用 Web 浏览器中的导航工具,检查随代码一起显示的代码验证结果。

检测运行时错误

项目质量和软件质量目标

控制板上显示的信息可用来监控软件质量、项目状态、缺陷数量、代码指标和软件质量目标。

项目概览控制板。

与您已经使用的缺陷跟踪工具集成

使用 Web 浏览器界面,在缺陷跟踪工具(如 Jira)中创建和分配工单。

创建工单。

最新特性

项目授权管理

创建和实施项目访问权的授权策略

AUTOSAR 支持

检查 AUTOSAR 规范与代码实现之间的运行时不匹配

堆栈大小计算

确定 C 程序和各个函数使用的最大堆栈

通过编译系统进行配置

通过编译系统自动生成 Polyspace 配置模块

多任务代码验证设置

将循环任务和非抢占式中断直接指定为验证选项

关于这些特性和相应函数的详细信息,请参阅发行说明

获取免费试用版

30 天探索触手可及。

马上下载

准备购买?

获取详细价格和并探索相关产品。

您是学生吗?

获得 MATLAB 和 Simulink 学生版软件。

了解更多