このページの内容は最新ではありません。最新版の英語を参照するには、ここをクリックします。

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) によって対応しています。

チュートリアル

デスクトップ

• デスクトップでの PolyspaceCode Prover の実行
  C/C++ コードのランタイム エラーを網羅的にチェックする。
• Polyspace Code Prover 解析結果のレビュー
  Polyspace Code Prover の結果の解釈、コードの修正、結果の正当化、結果の管理を行う。

Polyspace Platform ユーザー インターフェイス

• Polyspace Platform: A Unified Platform for Static Analysis and Dynamic Testing
  Polyspace Platform is an integrated environment for static analysis and testing of C/C++ code with Polyspace products.
• Benefits and Limitations of Switching to Polyspace Platform User Interface
  Import projects created in older user interface, run tests or static analysis on imported projects.
• Run Polyspace Code Prover in Polyspace Platform User Interface
  Check C/C++ code exhaustively for run-time errors.
• Review Polyspace Code Prover Analysis 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 Access Web インターフェイスでの重大度による順位付けと結果の割り当て (Polyspace Access)
  ダッシュボードに移動する、結果をフィルターする、問題をチーム メンバーに割り当てる。
• Polyspace Code Prover Server の結果を含む電子メール通知の送信
  Polyspace の結果へのリンクが記載されている添付ファイルを含む電子メールを開発者に送信する。
• Polyspace Access Web インターフェイスでの割り当てられた結果の表示 (Polyspace Access)
  自分に割り当てられた結果を確認する。

デスクトップからサーバー

• デスクトップからローカルでホストされているサーバーへの Code Prover 解析の送信
  Polyspace 解析の負荷をローカルでホストされているサーバーに移し、デスクトップでダウンロードした結果をレビューする。

展開

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

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

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

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

• Polyspace Bug Finder と Polyspace Code Prover の違い
  

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

• Polyspace Bug Finder と Polyspace Code Prover の両方を使用したワークフロー
  

  Bug Finder と Code Prover の解析をソフトウェア開発ワークフローに組み込む。