Polyspace Code Prover は、あらゆる入力に対するコードパスを解析し、C/C++ コードにおけるオーバーフロー、ゼロ除算、配列外アクセスといったランタイムエラーの有無を確認できます。また、制御やデータフローに関する解析結果を提供し、タスク (スレッド) 間で共有されるグローバル変数への同時アクセスの正当性も検証できます。
Polyspace Code Prover は、形式手法に基づく抽象解釈を用いた静的解析により、プログラム実行、コード計測、テストケースを必要とせずに結果を生成します。結果はソースコード上にインラインで表示され、色分けされた検出情報、変数の範囲、コードナビゲーション機能とともに確認できるため、わかりやすく、すぐに活用できます。Polyspace Code Prover は、手書きの C/C++ コードから Simulink や AI アシスタントで生成されたコードまで、あらゆる組み合わせで使用できます。
IEC Certification Kit (IEC 61508/ISO 26262) と DO Qualification Kit (DO-178) により、業界標準にも対応しています。
重大なランタイムエラーが存在しないことを証明
コードを実行せずに、可能性のあるすべての入力に対してすべてのコードパスを解析します。ランタイム条件にかかわらず、ランタイムエラーが決して発生しないステートメントを特定し、それ以外の注意が必要なステートメントを検出します。
ソフトウェアのパフォーマンスの最適化
ゼロ除算やオーバーフローなどについて安全かつセキュアな演算を特定することで、防衛的コードを削除します。あらゆる実行パスを介しても到達できないコード分岐を検出します。ロジックやプログラム構造のエラーを検出し、それらを削除することで、メモリフットプリントを縮小します。
グローバル変数の使用の解析
タスクやスレッドで共有される変数など、グローバル変数の読み取り/書き込み操作のデバッグに費やす時間を短縮します。
同時アクセスグラフを使用して、データレースの問題につながる制御フローおよびデータフローを理解します。コードを最適化するために、使用していないグローバル変数を特定します。
認証サポート
業界標準の認証プロセスを完了するために必要なアーティファクトを作成します。IEC 61508 および ISO 26262 規格に準拠した使用のための、TÜV SÜD 認証を取得しています。DO-178C プロセスには、レポートとアーティファクトを使用します。
Simulink および Stateflow との統合
生成されたコードに対して解析を実行し、得られた調査結果をソースの Simulink モデルブロックおよび Stateflow チャートにトレースできます。Simulink 環境から Polyspace® 解析を起動します。
デスクトップでの対話形式の解析
ソフトウェア プロジェクト全体またはサブセットに対して静的コード解析を実行します。デスクトップツールを使用してレポートを作成し、結果を確認して問題を重大度により順位付けします。
デバッガーに似たビューを使用して、ランタイムエラーにつながる各ステートメント内をステップバイステップで移動し、複雑なバグの根本原因を見つけます。60 以上の C および C++ コンパイラのネイティブサポートと、プロジェクトのビルドシステムから抽出された Polyspace 解析の自動セットアップを使用して、プロジェクトを整理し構成できます。
静的アプリケーション セキュリティ テスト
バッファー オーバーフロー、メモリアクセス、数値オーバーフローなどの重大なセキュリティの脆弱性が存在しないことを証明します。コードを実行せずに、すべてのコードパスと入力でコードを解析することにより、ファズテストの必要性を削減します。
製品リソース:
Polyspace 製品ファミリ
Polyspace 製品は、 開発ライフサイクル全体でソフトウェア品質をテストおよび監視することにより、重要なコードを安全かつセキュアにします。
Polyspace Access
コーディングの欠陥の特定、静的解析結果のレビュー、ソフトウェア品質メトリクスの監視
Polyspace Copilot
Polyspace 向けに最適化された AI アシスタント。
Polyspace Test
組み込みシステムにおける C および C++ コードのテストを開発、管理、実行
Polyspace as You Code
IDE 上でコーディング規約違反やソフトウェアの脆弱性を特定します。
Polyspace Bug Finder
静的解析を使用したソフトウェアのバグの特定
Polyspace Code Prover Server
CI パイプラインへの重要な C および C++ コードステートメントを継続的かつ網羅的に検証します。
Polyspace Bug Finder Server
サーバー コンピューターで実行する静的解析によりソフトウェアの欠陥を特定
Polyspace Client for Ada
ソースコードにランタイムエラーが存在しないことを証明
Polyspace Code Prover
形式的手法を用いて、最も重要な C および C++ ステートメントを網羅的に検証します。
Polyspace Server for Ada
コンピューター クラスターでコード検証を実行し、メトリクスを公開