Polyspace® 静态代码分析产品采用形式化方法证明在所有可能的控制流和数据流下都没有关键运行错误。包括编码规范、安全漏洞、代码指标和数百条其他软件缺陷的检查。Polyspace Test™ 为嵌入式系统的 C 和 C++ 代码提供了开发、管理和执行单元与集成测试的工具。
Polyspace Access
识别编码缺陷,查看静态分析结果,并监控软件质量指标
Polyspace Bug Finder
检查编码规则、安全标准、代码指标并找出 Bug
Polyspace Bug Finder Server
通过在服务器上运行的静态分析识别软件缺陷
Polyspace Code Prover
无需执行代码即可形式化地证明不存在严重的运行时错误
Polyspace Code Prover Server
证明软件中不存在运行时错误
Polyspace Test
开发、管理和执行嵌入式系统中 C 和 C++ 代码的测试
Polyspace Client for Ada
证明源代码中不存在运行时错误
Polyspace Server for Ada
在计算机集群上执行代码验证并发布指标

使用形式化方法为 C/C++ 和 Ada 代码自动执行静态分析
代码质量
无需测试用例或不执行代码的情况下,找出缺陷并形式化证明不存在严重运行时错误。
功能安全
符合 MISRA、ISO 26262、IEC 61508、DO-178 和 FDA 法规的安全标准和文档合规要求。
网络安全
检查软件安全漏洞,及是否符合 CWE、CERT-C、ISO/IEC 17961 和其他标准。