Polyspace Server for Ada

 

Polyspace Server for Ada

在计算机集群上执行代码验证并发布指标

Polyspace Server for Ada

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

详尽检查每个 Ada83 或 Ada95 代码操作的运行时正确性。识别无论运行时条件如何都永远不会遇到运行时错误的语句。在事件跟踪、变量值范围和与发现相关的调用树的支持下,分析运行时漏洞。Polyspace Server for Ada 使用形式化方法来检测其他测试手段无法找出的错误。在不执行代码的情况下,针对所有可能的输入分析全部代码路径。

自动化并集成到开发运营一体化中

将分析集成的代码作为现有开发运营一体化工作流和工具的一部分,以此支持现代软件开发实践。Polyspace Server for Ada 可与流行的持续集成工具(如 Jenkins 和 Bamboo®)协同工作。

改进软件设计和代码理解

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

优化软件性能

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

分析全局变量用法

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

静态应用程序安全性测试

通过详尽地对潜在的易受攻击的 Ada 语句进行压力测试,如内存访问、缓冲区溢出或数值溢出,证明应用程序没有严重的安全漏洞。对 20 条 CWE 弱点规则的支持。利用 Polyspace Server for Ada 生成的结果来补充或取代模糊测试,转而关注易受攻击的操作。

改进和补充稳健性和功能测试

使用 Polyspace Server for Ada,通过将测试重点放在证明不安全的语句(如除以零或溢出)上来改进稳健性测试。利用控制流和数据流分析以及计算出的函数参数和全局变量范围,使用 Polyspace Server for Ada 提供的结果来创建和维护边界测试与分区测试。

管理静态分析项目并监控项目质量

组织您的 Ada 静态代码分析项目,以使用 Polyspace Access 支持开发团队和工作流。使用控制板上显示的信息来监控软件质量、项目状态、缺陷数量和代码指标。

Polyspace 产品系列

Polyspace 产品通过在整个开发生命周期中测试和监控软件质量来保证关键代码的安全。

Polyspace Access

识别编码缺陷,查看静态分析结果,并监控软件质量指标

Polyspace Code Prover Server

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

Polyspace Bug Finder

运用静态分析找出软件 Bug

Polyspace Test

开发、管理和执行嵌入式系统中 C 和 C++ 代码的测试

Polyspace Bug Finder Server

通过在服务器上运行的静态分析识别软件缺陷

Polyspace Client for Ada

证明源代码中不存在运行时错误

Polyspace Code Prover

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

Polyspace Server for Ada

在计算机集群上执行代码验证并发布指标