AUTOSAR コードに対する Polyspace の結果のレビュー

このトピックでは、Polyspace® でのコンポーネント ベースの AUTOSAR コード検証方法について説明します。統合解析方法については、Polyspace で AUTOSAR コードのコンポーネント ベースの解析と統合解析のどちらかを選択するを参照してください。

このチュートリアルでは、AUTOSAR 固有のコードの Polyspace Code Prover™ 結果を開いて、ARXML のデータ制約違反を強調表示する結果を解釈する方法を説明します。

Code Prover は、AUTOSAR ソフトウェア コンポーネントのコード実装に ARXML 仕様との不一致がないかどうかをチェックします。たとえば、RTE 関数の引数が ARXML で定義されている制約範囲から外れた値を取る場合、解析によって潜在的な問題のフラグが設定されます。

このチュートリアルの手順に従うには、polyspaceroot\polyspace\examples\doc_cxx\polyspace_autosar に含まれるデモ ファイルに対して Polyspace を実行します。このチュートリアルに含まれる情報を使用して AUTOSAR 固有の結果をレビューします。解析実行に関するヘルプは、AUTOSAR コードに対する Polyspace の実行を参照してください。

結果を開く

Polyspace ユーザー インターフェイスで解析を実行する場合、それぞれの結果を直接開くことができます。開く結果をダブルクリックします。

スクリプトを使用して解析を実行する場合、解析後に次のいくつかの方法で結果を開くことができます。

  • Web ブラウザーでプロジェクト フォルダーのファイル psar_project.xhtml を開きます。すべてのソフトウェア コンポーネントの結果の概要を確認し、各ソフトウェア コンポーネントの結果に移動します。詳細については、すべてのソフトウェア コンポーネントの結果の概要の確認を参照してください。

  • Polyspace ユーザー インターフェイスでプロジェクト フォルダーのファイル psar_project.psprj を開きます。[プロジェクト ブラウザー] ペインで各結果を開きます。

  • 個別の結果ファイルが格納されているフォルダーに移動します。Polyspace ユーザー インターフェイスで結果ファイル (拡張子 .pscp) を開きます。

    結果ファイルはプロジェクト フォルダーの AUTOSAR サブフォルダーに保存されています。各結果へのパスは、ソフトウェア コンポーネントの内部動作の完全修飾名に従います。たとえば、完全修飾名が pkg.component.bhv の場合、結果は AUTOSAR\pkg\component\bhv\verification に格納されます (Polyspace ユーザー インターフェイスで検証を実行した場合、最終的なサブフォルダーは CP_Result です)。

すべてのソフトウェア コンポーネントの結果の概要の確認

特定の結果セットを開く前に、すべてのソフトウェア コンポーネントの結果の概要を確認する必要がある場合があります。次のいずれかを行います。

結果を簡単に理解するには、最初の方法を使用します。

ファイル psar_project.xhtml で、左上隅の アイコンをクリックします。左側のペインで、[Behaviors] をクリックします。内部動作が抽出されたすべてのソフトウェア コンポーネントのリストを確認できます。

このリストをフィルター処理して、関心があるソフトウェア コンポーネントのみを表示できます。特定のソフトウェア コンポーネントを表示するには、関心があるソフトウェア コンポーネントの完全修飾名を検索ボックスに入力します。

正規表現を入力して、複数のコンポーネントを表示することもできます。たとえば、pkg.tst002.swc001 で始まる完全修飾名をもつすべてのコンポーネントを表示するには、次の表現を入力します。

^pkg.tst002.swc001.*

[検索] をクリックします。右側のリストに、クエリしたソフトウェア コンポーネントのみが表示されます。

他の基準に基づいてコンポーネントを除外することもできます。

  • 検証の成功または失敗

    検証が完了したソフトウェア コンポーネントのみを表示するには、[error status] フィルターをクリックしてクリアします。

  • 特定の種類の結果 (レッド チェックなど) の有無

    レッド チェックをもつソフトウェア コンポーネントのみを表示するには、[red] フィルター自体を除く、[red] フィルターを含む行のすべてをクリックします。

ソフトウェア コンポーネントのランナブルとソース ファイルの表示

各ソフトウェア コンポーネントについてプロジェクト フォルダーのファイル psar_project.xhtml で次の情報を確認できます (前の図を参照してください)。

  • 解析に関するこのソフトウェア コンポーネントの状態。つまり、そのソフトウェア コンポーネント仕様が解析され、ソース コードが抽出された後、Code Prover によって解析されたかどうか。

    Code Prover 解析が完了したことを確認するには、セクション [Verification of extracted implementation code] で、次のステートメントを探します。

    State after last command execution: updated.

  • このソフトウェア コンポーネントによって提供されている関数と、使用されている Rte_ 関数。

    このリストを表示するには、次のリンクをクリックします。

    See key autosar definition for this behavior

  • ソフトウェア コンポーネントに含まれるランナブルのグラフィカル ビュー。グラフィカル ビューには以下が示されます。

    • ランナブルを実装するエントリポイント関数とその呼び出し先

    • これらの関数を含むファイル

    このビューを表示するには、左側のペインのソフトウェア コンポーネントのリストで、関心があるソフトウェア コンポーネントの (動作グラフ) アイコンをクリックします。このグラフからソフトウェア コンポーネントのテキスト説明に戻るには、 (動作ページ) アイコンをクリックします。

    この例では、内部動作 bhv001 を備えたコンポーネントには、エントリポイント関数 foo、init、および step を通じて 3 つのランナブルが実装されていることがわかります。3 つのエントリポイント関数はすべて、ファイル swc001.c で定義されています。

    関数 step は、別のファイル (dep3.c など) で定義された関数を呼び出します。step の アイコンをクリックすると、ランナブル step の実装に関連するファイルのみを表示できます。ソフトウェア コンポーネントの完全なグラフィカル ビューに戻るには、グラフに含まれる空白の任意の場所をクリックします。

  • Code Prover の結果と結果ファイルへのリンクの概要。

    次の行のような行を探します。

    Verification results are in summary: green check=84, orange check=2, red check=1
    この行に続くリンクをクリックして、Polyspace ユーザー インターフェイスで結果ファイルを開きます。以前に .pscp ファイルを開いたことがない場合、リンクをクリックすると単に結果ファイルがダウンロードされる可能性があります。.pscp ファイルが常に (実行可能ファイル polyspaceroot\polyspace\bin を使用して) Polyspace ユーザー インターフェイスで開くようにします (polyspaceroot は Polyspace インストール フォルダーです)。

    結果は、[AUTOSAR ランナブルの実装の無効な結果] などの AUTOSAR 固有の実行時チェックと、[ゼロ除算] などの一般的な C/C++ 実行時チェックから構成されます。

ソフトウェア コンポーネントの AUTOSAR 固有の実行時チェックの解釈

[結果のリスト] ペインで、結果 [AUTOSAR ランナブルの実装の無効な結果] または [AUTOSAR のランタイム環境関数の無効な使用] を選択します。さまざまなペインの情報を使用して結果をさらに詳しく調査します。

戻り値と引数のチェック

[結果の詳細] ペインの情報を使用して、戻り値または引数が ARXML のデータ制約に違反しているかどうか、NULL 値になる可能性があるかどうかを判断します。明確なエラーを示す ! アイコンまたは潜在的なエラーを示す ? アイコンを確認します。

戻り値と各引数について、実行時に実際に取りうる値と ARXML 仕様のデータ型によって許可されている値を確認します。それらを比較して、許可されていない値を見つけます。

結果 [AUTOSAR ランナブルの実装の無効な結果] は、そのランナブルを実装する関数の戻り値または出力引数がデータ制約に違反する可能性があるかどうかを判別します。結果 [AUTOSAR のランタイム環境関数の無効な使用] は、Rte_ 関数の入力引数がデータ制約に違反するかどうかを判別します。

引数の仕様のチェック (オプション)

基本ソフトウェア型が発生させる変数の元となるアプリケーション データ型の確認が必要な場合があります。青い [parameter spec] リンクをクリックして、パラメーターまたは戻り値のデータ型について以下の情報を説明した ARXML の引用を確認します。

  • アプリケーション データ型、実装データ型、基本ソフトウェア型

  • データ制約、単位、計算方法

結果の根本原因の検出

変数がどのようにデータ制約に違反する値を取得するのかを調査します。コードで逆にトレースするには、[ソース] ペインで変数を右クリックし、そのインスタンスすべてを検索するか、変数の定義に移動します。その他のヒントについては、Polyspace デスクトップ ユーザー インターフェイスでの Code Prover の結果の解釈またはPolyspace Access Web インターフェイスでの Code Prover の結果の解釈 (Polyspace Access)を参照してください。

コードまたは ARXML を修正するか、コメントによって結果を正当化するかを決定します。Polyspace ユーザー インターフェイスでのバグ修正または正当化による結果への対処またはPolyspace Access でのバグ修正または正当化による結果への対処 (Polyspace Access)を参照してください。

参考

|

トピック