最新のリリースでは、このページがまだ翻訳されていません。 このページの最新版は英語でご覧になれます。

Polyspace Code Prover

ソフトウェアでのランタイム エラーの有無の実証

Polyspace® Code Prover™ は安定性の高い静的解析ツールで、C および C++ ソース コード内のオーバーフロー、ゼロ除算、配列の範囲外へのアクセスおよびその他のランタイム エラーの有無が証明されます。プログラムの実行、コード計測またはテスト ケースを必要とすることなく、結果が生成されます。Polyspace Code Prover では、セマンティクスの解析および形式的手法に基づく抽象的な解釈が使用され、ソフトウェアの手続き間のフロー、制御フロー、およびデータ フローの動作が検証されます。また、手書きのコード、生成されたコードまたはその 2 つの組み合わせの検証に使用できます。各コード ステートメントは色分けされ、ランタイム エラーなし、エラーと証明、到達不能、または未証明のいずれかであることが示されます。

Polyspace Code Prover では、変数および関数の戻り値の範囲情報が表示され、指定された範囲限界値を超えた変数を証明できます。コード検証の結果を使用して品質メトリクスを追跡し、ソフトウェア品質目標との一致をチェックできます。Polyspace Code Prover は Eclipse™ IDE と共に使用して、デスクトップ上でコードを検証できます。

業界標準には、IEC Certification Kit (for IEC 61508 and ISO 26262) と DO Qualification Kit (for DO-178) によって対応しています。

Polyspace Code Prover 入門

Polyspace Code Prover の基礎を学ぶ

解析の設定と実行

Polyspace ユーザー インターフェイス、コマンド ラインまたは他の開発環境でのコードのランタイム エラーのチェック

解析結果のレビュー

解析結果のランタイム エラーの調査および修正、検証結果の整理、検証結果の参照

ツールの検定と認定

DO および IEC 認定のための Polyspace Code Prover の検定

Polyspace Code Prover でのトラブルシューティング

Polyspace Code Prover での予期しない問題の解決