Polyspace Code Prover

更新

 

Polyspace Code Prover

ソフトウェアにランタイムエラーがないことを証明

Polyspace Code Prover™ は、C ソースコードおよび C++ ソースコードに、オーバーフロー、ゼロ除算、範囲外の配列アクセス、その他のランタイムエラーがないことを証明する堅牢な静的解析ツールです。プログラムの実行、コード計測、テストケースの作成を行う必要なく、結果を生成します。Polyspace Code Prover は、形式手法に基づいたセマンティック解析と抽象解釈を使用して、ソフトウェアの手続き間、制御、データフローの動作を検証します。手書きのコード、生成されたコード、またはその 2 つの組み合わせを検証するために使用できます。各コードステートメントは、ランタイムエラーがないこと、失敗であること、到達不能であること、または未証明であることを示すために色分けされています。

Polyspace Code Prover は、変数および関数の戻り値の範囲情報を表示し、どの変数が指定された範囲制限を超えているかを証明できます。コードの検証結果を使用して、品質の指標を追跡し、ソフトウェア品質目標との適合性を確認できます。Polyspace Code Prover を Eclipse™ IDE とともに使用して、デスクトップのコードを検証できます。

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

形式数学を使用してコードを検証

検出漏れのない高レベルの品質と安全性を実現します。

重大なランタイムエラーがないことを証明

ランタイム条件にかかわらず、ランタイムエラーが発生しない C/C++ コードおよび Ada コード操作を識別します。

ランタイムエラーの検出

他のテスト手段では検出できないエラーを検出

コードを実行せずに、可能性のあるすべての入力に対してすべてのコードパスを解析します。

呼び出し階層。

認証アーティファクトを作成

業界標準に基づいたプロジェクトの認証プロセスを完了させます。

DO Qualification Kit。

コードの理解と改善

コードのレビュー、デバッグ、堅牢性のテストにかかる時間を削減します。

問題の根本原因を把握し、設計を改善

ソフトウェア内の制御およびデータフローを検証し、変数や演算子に関連する範囲情報を表示します。

すべてのランタイム条件について考えられる範囲を表示するツールヒント。

意図しないソフトウェアの動作を防止

実行パスを介して到達できないすべてのコードセクションと、ロジックおよびプログラム構造のエラーを検索します。

デッドコードを検索。

Simulink モデルへのコード検証結果をトレース

生成されたコードの結果を検証し、Simulink のソースモデルブロックへの検証結果をトレースします。

Simulink モデルへのコード検証結果のトレース。

Polyspace Code Prover Server を使用すると、コード検証を自動化できます。

コード変更の解析を早期かつ頻繁に実行することで、継続的な統合を可能にします。

コード検証プロセスの自動化

Polyspace Code Prover Server™ を使用して、Jenkins や Bamboo などのビルド自動化ツールによって、サーバークラスのマシンで Polyspace Code Prover 静的解析エンジンを実行します。

コード検証プロセスの自動化。

共同レビューの結果を通知およびアップロード

問題を重大度により順位付けして解決できるように、自動的に欠陥をコンポーネントの所有者に割り当て、メール通知を送信し、検証結果を Polyspace Code Prover Access にアップロードします。

Polyspace Code Prover の検証結果を記載したメール通知を送信。

Polyspace Code Prover Access を使用した共同レビュー

検証結果と品質の指標をソフトウェア開発チームと共有します。

問題を重大度により順位付けして解決できるように、Polyspace Code Prover の検証結果を確認

Polyspace Code Prover Access™ では、中央リポジトリに格納されている Polyspace コード検証結果および品質の指標に対する Web ブラウザー インターフェイスが提供されます。Web ブラウザーのナビゲーションツールを使用して、コード検証結果を調査します。この結果はコードと一緒に表示されます。

ランタイムエラーの検出

プロジェクト品質とソフトウェア品質目標

ダッシュボードには、ソフトウェアの品質、プロジェクト ステータス、欠陥の数、コードメトリクス、ソフトウェア品質目標を監視するために使用できる情報が表示されます。

プロジェクト概要のダッシュボード。

すでに使用しているバグ追跡ツールと統合

Web ブラウザー インタフェースを使用して、Jira などのバグ追跡ツールでチケットを作成し割り当てます。

チケットを作成。

新機能

プロジェクトの承認の管理

プロジェクトへのアクセスに関する承認ポリシーを作成および実施

AUTOSAR サポート

AUTOSAR の仕様とコードの実装において、ランタイムの不一致があるかどうかを確認

スタックサイズの計算

C プログラムと個々の関数による最大のスタック使用量を判定

ビルドシステムからの設定

ビルドシステムから Polyspace 設定モジュールを自動的に生成

マルチタスキング コード検証設定

周期タスクおよびプリエンプトできない割り込みを検証オプションとして直接指定

これらの機能および対応する関数の詳細については、リリースノートを参照してください。

無料評価版を入手する

30 日間の無料評価版はこちら

今すぐダウンロード

あなたは学生ですか?

MATLAB および Simulink 学生向けソフトウェアの入手

詳細を見る