Polyspace Code Prover 入門

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

Polyspace Code Prover では、変数および関数の戻り値の範囲情報も表示され、指定された範囲限界値を超えた変数を証明できます。結果はダッシュボードにパブリッシュできるため、品質メトリクスを追跡して、ソフトウェア品質目標に確実に準拠させることができます。

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

チュートリアル

デスクトップ

• Run Polyspace Code Prover on Desktop
  Check C/C++ code exhaustively for run-time errors.
• Review Code Prover Results in Polyspace Platform User Interface
  Interpret Polyspace Code Prover results, fix code or justify results, manage results.

サーバーおよび Web インターフェイス

• Polyspace Server および Access 製品のクイック スタート ガイド
  プロジェクト、チーム、および組織での、Polyspace 実行を設定するのに必要な作業を確認する。
• サーバーでの Polyspace Code Prover の実行と Web インターフェイスへの結果のアップロード
  コード送信後のランタイム エラーのチェックおよび Web インターフェイスでのレビューのための結果のアップロード。

展開

• Polyspace Code Prover によるソース コード検証
  

  C および C++ コードの検証に Polyspace Code Prover による静的解析がどのように役立つかを理解する。

• Polyspace 製品およびソフトウェア開発ワークフロー
  

  ソフトウェア開発ライフ サイクルで使用できる Polyspace 製品について学ぶ。

• Polyspace Bug Finder と Polyspace Code Prover の違い
  

  Bug Finder と Code Prover の相互補完を調べ、開発ワークフローに各製品を導入するタイミングを判断する。