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

Polyspace 検証の動作

Polyspace^® ソフトウェアは、"静的検証" を使用してランタイムエラーがないことを証明します。静的検証は、実際にプログラムを実行せずにプログラムの動的プロパティを引き出します。これは、検証が特定のテストケースに依存しないという点で、実行時デバッグなどの他の手法とは大きく異なります。Polyspace 検証で得られた動的プロパティは、ソフトウェアのあらゆる実行に当てはまります。

静的検証とは

静的検証は広義の用語であり、プログラムを実行せずにプログラムの動的プロパティを引き出すすべてのツールに当てはまります。しかし、ほとんどの静的検証ツールは、間違っている可能性がある構造を検索しながら、ソフトウェアの複雑さだけを検証します。Polyspace 検証では、ほぼすべてのランタイムエラーと想定されるグローバル共有データとのアクセス競合を特定する、深いレベルの検証を行います。

Polyspace 検証は、ソフトウェアの操作とデータの典型的な近似を使用して、検証対象のソフトウェアを近似することで動作します。

たとえば、以下のコードについて考えます。

for (i=0 ; i<1000 ; ++i)
{    tab[i] = foo(i); 
}

変数 i が tab の範囲を超えていないかチェックするための従来のアプローチは、i が取り得るそれぞれの値を列挙することです。その場合、1,000 回のチェックが必要になります。

静的検証アプローチでは、変数 i は領域変動によってモデル化されます。たとえば、i のモデルは、それが静的な間隔 [0..999] に属するというものです(データの複雑さに応じて、凸多面体、整数格子、さらに詳細なモデルもこの目的で使用されます)。

当然のこととして、近似では情報が失われることになります。たとえば、i がループの各サイクルでインクリメントされるという情報は失われます。しかし、重要な事実は、値域エラーが発生しないことを確実にするためにこの情報は必要ないということです。i の領域変動が tab の範囲よりも小さいということを証明するだけで十分です。その証明には 1 つのチェックしか必要とされず、したがって、従来のアプローチよりも効率良くゲインが比較されます。

静的なコード検証には厳密解があります。しかし、考えられるすべてのテストケースの列挙が必要になるため、この厳密解は実用的ではありません。結果的に、有用なツールには近似が必要です。

網羅性

網羅性の点では何も失われません。その理由は、Polyspace 検証が、過大近似を実行することで動作するためです。言い換えれば、プログラム変数の計算された変動領域は、実際の変動領域のスーパーセットになります。結果として、Polyspace はチェックを必要とするランタイムエラー項目を検証します。

PolyspaceCode Prover 検証の価値

Polyspace 検証は、以下の役に立ちます。

ソフトウェアの信頼性の向上
開発時間の短縮
開発プロセスの改善

ソフトウェアの信頼性の向上

Polyspace ソフトウェアにより、コードの正しさが証明され、ランタイムエラーが特定されるため、C/C++ アプリケーションの信頼性が高まります。Polyspace ソフトウェアは、高度な検証手法を使用して、ソースコードを徹底的に検証します。

Polyspace ソフトウェアは、コードのすべての実行を検証するので、次のようなコードを特定できます。

エラーがない
常にエラーがある
到達不能
エラーの可能性がある

この情報により、コードにどの程度のランタイムエラーがないかを知り、エラーを修正することでコードの信頼性を高めることができます。

また、Polyspace 検証ソフトウェアを使用して、MISRA C™、MISRA™ C++ または JSF^® C++ 規格などの確立されたコーディング規約に各自のコードが準拠しているかどうかチェックすることで、コードの品質を改善することもできます。¹

開発時間の短縮

Polyspace ソフトウェアを使用すると、検証プロセスを自動化し、検証結果を効率的に確認できるため、開発時間が短縮されます。開発プロセスのどの時点でも使用できます。ただし、コーディングの初期の段階で使用することで、修正コストが小さいうちにエラーを見つけることができます。

Polyspace ソフトウェアを使用して、コンパイル前にソースコードを検証します。ソースコードを検証するには、プロジェクトで検証パラメーターを設定し、検証を実行し、結果を確認します。このプロセスは、手動による方法を使用したり、コードの変更やテストケースの実行が必要なツールを使用するよりも、はるかに短い時間で済みます。

結果の色分けは、エラーをすばやく認識するのに役立ちます。ソースコード内のエラーの正確な場所を確認できるので、デバッグ時間が短くなります。エラーを修正した後は、再度簡単に検証を実行できます。

Polyspace 検証ソフトウェアにより、時間を効果的に使うことができます。コードのエラーがない部分がわかっているので、証明されたコード (レッドコード) またはエラーが存在する可能性があるコード (オレンジコード) に集中することができます。

エラーが存在する可能性があるコード (オレンジコード) の確認には時間がかかる場合がありますが、Polyspace ソフトウェアはレビュープロセスに役立ちます。フィルターを使用して、特定のタイプのエラーに焦点を当てたり、確認が必要なコードをソフトウェアで特定することができます。

開発プロセスの改善

Polyspace ソフトウェアを使用すると、検証パラメーターと結果を容易に共有でき、開発チームと連携して製品の信頼性を向上させることができます。検証パラメーターが設定されると、開発者は同じアプリケーションの他のファイルでもそれらを再利用できます。

Polyspace 検証ソフトウェアでは、開発プロセス全体を通じてコード検証がサポートされます。

個々の開発者は、初期のコーディング段階でランタイムエラーを見つけて修正できます。
品質保証エンジニアは、アプリケーション全体の信頼性をチェックできます。
管理者は、検証結果からレポートを生成することにより、アプリケーションの信頼性を監視できます。

参考

トピック

¹ MISRA and MISRA C are registered trademarks of MISRA Ltd., held on behalf of the MISRA Consortium.