Polyspace Code Prover

C および C++ 組み込みソフトウェアの検証

Polyspace Code Prover は最高レベルの品質と安全性で動作する必要のあるC および C++ 組み込みソフトウェアのコードを検証します。これは抽象解釈と呼ばれる形式手法を使用して、確実な検証結果を生成します。Polyspace Code Prover はランタイム エラーが発生する可能性のあるコードと、ランタイム エラーがないことが証明されたコードを特定します。ユーザーは Polyspace Code Prover をすべての入力、パス、変数値を徹底的に検証する高度な品質保証プロセスの一部として使用します。Polyspace Code Proverは、コードの各要素のステータスを色分け表示で示します。Simulink® と統合されると、コード レベルのランタイム結果に Simulink モデルまで遡るトレーサビリティを提供します。

Polyspace Code Prover を使用して、次の作業を実行できます。

  • コードの証明 — コードにランタイム エラーがないことを検証
  • 検出漏れのない結果の取得 — すべての潜在的ランタイム エラーを徹底的に特定
  • コードの品質に対する信頼の強化 — 証明済みコードと未証明コードを比較計測

Polyspace Code Prover は、コマンド ラインまたはグラフィカル ユーザー インタ-フェイスから、あるいは Visual Studio® と Eclipse™ へのプラグインを通じてアクセスできます。これを使用して、以下のようなソフトウェア開発ワークフローの重要な作業のすべてを支援することができます。

  • ランタイム エラーの検出
  • 特定のランタイム エラーがないことの証明
  • 変数範囲を判別し範囲限界の違反を確実に排除
  • 適切なソフトウェアの品質目標を確実に達成
  • ランタイム エラーを Simulink ブロックまたは IBM® Rational® Rhapsody® モデルまで追跡
  • 認定用アーティファクトの作成

Polyspace Code Prover は Polyspace Bug Finder と連携して、欠陥を検出し、コーディング規格との準拠性をチェックします。これらの製品は、バグの検出から、コード規則のチェック、ランタイム エラーの証明に至る、開発の初期段階におけるエンド ツー エンドの静的解析機能を提供します。この機能により、最高レベルの品質および安全性で動作する必要のある組み込みソフトウェアの信頼性が確保できます。

Parallel Computing Toolbox™ および MATLAB Distributed Computing Server™ を使用して検証ジョブを並列化することで、コード検証を高速化してコンピューター クラスターにアンロードできます。

次のトピック: ランタイム エラーの検出

製品評価版の入手または製品の購入

評価版 Polyspace Code Prover

評価版ソフトウェアを入手する

モデルとコードのテスト検証

Web セミナーを表示する