Polyspace Code Prover Server は、C コードおよび C++ コードのオーバーフロー、ゼロ除算、範囲外の配列アクセス、その他の特定のランタイムエラーが存在しないことを証明する、堅固な静的解析エンジンです。マルチスレッドコードを含む、起こりうるすべての制御フローおよびデータフローに手続き間解析を行い、各演算を、常に安全、常にエラー、到達不能、脆弱のいずれかとして識別します。Polyspace Code Prover Server は、コードセグメントについて、ランタイムエラーが存在しない、エラーが証明されている、到達不能である、または未証明であるものを識別します。
Polyspace Code Prover Server は、サーバークラスのマシンで実行し、Jenkins® などのツールを使用して、自動検証のためにビルドおよび継続的インテグレーション システムに統合できます。解析結果は Polyspace Access に公開して、問題の重大度による順位付けと解決に使用できます。
業界標準のサポートは、IEC Certification Kit (for IEC 61508 and ISO 26262) および DO Qualification Kit (for DO-178) により対応しています。
重大なランタイムエラーが存在しないことを証明
コードを実行せずに、可能性のあるすべての入力に対してすべてのコードパスを解析します。ランタイム条件にかかわらず、ランタイムエラーが決して発生しないステートメントを特定し、それ以外の注意が必要なステートメントを検出します。
DevOps 自動化および統合
既存の DevOps ワークフローやツールにプラグインで組み込むことにより、最新のソフトウェア開発手法をサポートします。Polyspace® は、Jenkins や Bamboo® などの広く使用されている継続的インテグレーション ツールと連携します。
あらゆるプラットフォームでの静的コード解析の実行
オンプレミスまたはクラウドのオートメーション サーバーで Polyspace Code Prover Server を実行します。MathWorks 参照アーキテクチャを使用して、Docker、AWS®、Azure® などのプラットフォームに展開します。
認証サポート
業界標準の認証プロセスを完了するために必要なアーティファクトを作成します。IEC 61508 および ISO 26262 の最高機能安全水準の TÜV SÜD 認証を取得しています。DO-178C 検定をサポートしています。
グローバル変数の使用の解析
グローバル変数の読み取り/書き込み操作によって生じる問題のデバッグにかかる時間を削減します。保護されていない共有変数と使用されていない変数を特定します。
静的アプリケーション セキュリティ テスト
バッファー オーバーフロー、メモリアクセス、数値オーバーフローなどの重大なセキュリティの脆弱性が存在しないことを証明します。コードを実行せずに、すべてのコードパスと入力でコードを解析することにより、ファズテストの必要性を削減します。
影響分析
指定されたグローバル変数やローカル変数が他の変数や特定のステートメントに与える影響を形式的に追跡し、検証します。OBD 関連ソフトウェアに関する CARB からの要件を満たすための信号解析、ISO 26262 のコンテキストで干渉がないことの証明、およびキャリブレーション パラメーターの影響分析を行います。ソフトウェア セキュリティのコンテキストでは、汚染解析を実行し、機密データフローを追跡します。
製品リソース:
Polyspace 製品ファミリ
Polyspace 製品は、 開発ライフサイクル全体でソフトウェア品質をテストおよび監視することにより、重要なコードを安全かつセキュアにします。
Polyspace Access
コーディングの欠陥の特定、静的解析結果のレビュー、ソフトウェア品質メトリクスの監視
Polyspace Code Prover Server
ソフトウェアにランタイムエラーが存在しないことを証明
Polyspace Bug Finder
静的解析を使用したソフトウェアのバグの特定
Polyspace Test
組み込みシステムにおける C および C++ コードのテストを開発、管理、実行
Polyspace Bug Finder Server
サーバー コンピューターで実行する静的解析によりソフトウェアの欠陥を特定
Polyspace Client for Ada
ソースコードにランタイムエラーが存在しないことを証明
Polyspace Code Prover
ソフトウェアにランタイムエラーが存在しないことを証明
Polyspace Server for Ada
コンピューター クラスターでコード検証を実行し、メトリクスを公開