Polyspace Code Prover を使用した AUTOSAR ソフトウェア コンポーネントの検証

R2018a 以降、Polyspace Code Prover™ は、ソフトウェア開発の AUTOSAR (Automotive Open System Architecture) 方法論を直接サポートしています。AUTOSAR ソフトウェア開発ワークフローにおける役割に関わらず、ユーザーは Release 2018a 以降の Polyspace Code Prover を AUTOSAR 対応の静的解析ツールとして使用できます。

Polyspace Code Prover は、AUTOSAR ソフトウェア コンポーネントのコード実装に対して静的プログラム解析を実行します。この解析により、起こりうるランタイムエラーや、コードと AUTOSAR XML (ARXML) 内の設計仕様との不一致をチェックします。

AUTOSAR 方法論

AUTOSAR 方法論は、輸送システムの電子コントロールユニット (ECU) に対応したソフトウェア開発標準です。この方法論は、ECU ハードウェアと通信を行うためのインフラストラクチャと、ECU の機能を実装するアプリケーション層を分離するものです。

本質的に、この方法論には、基盤となるハードウェアから独立してアプリケーション層ソフトウェアを開発できるようにするための一連のルールが用意されています。通信用インターフェイスに関する AUTOSAR ルールに従っている限り、AUTOSAR ランタイム環境 (RTE) では、適切なサービスを使用して ECU ハードウェア上にアプリケーション ソフトウェアを展開できます。

AUTOSAR アプリケーション層のソフトウェア開発ワークフロー

AUTOSAR 方法論におけるアプリケーション層のソフトウェア開発は、2 つのパートに分かれています。(1) アーキテクチャと通信の定義と (2) コード実装の記述です。

1. アーキテクチャの定義: AUTOSAR ソフトウェア開発のいわゆるコントラクト フェーズにおいて、ソフトウェア設計者は、アプリケーション層を構成するソフトウェア コンポーネント (SWC) を設計します。仕様書 (XML 形式) は、SWC をポート、インターフェイス、およびランナブルで定義しています。AUTOSAR XML (ARXML) 仕様を使用すると、ソフトウェア コンポーネントのランナブルを実装する C 関数のヘッダーファイルと空の本体を含むコードスタブを生成することができます。
2. コード実装の記述: ソフトウェア開発者は、ソフトウェア コンポーネントのランナブルを実装する C 関数の本体を記述します。また、Simulink などの高位設計ツールを使用して関数を生成することもできます。(Simulink を使用して仕様を生成することもできます。)

通常、上記 2 つのアクティビティは、異なる組織 (OEM と Tier 1 サプライヤーなど) で発生するか、組織の別々の部門で発生し、多くの場合、さまざまな特定分野の専門家が関与します。

AUTOSAR 方法論では、ソフトウェア開発が一方通行のプロセスであるかのように見えるかもしれません。ソフトウェア設計者は、ARXML 仕様による設計を提供し、開発者はそれらの仕様の範囲内でコードを記述します。しかし実際には、設計を実装することにより、設計の変更を伴う可能性のある考慮事項が明らかになる、という双方向のプロセスになっています。次の 2 つの状況について見てみましょう。

• 新しいエラー ステータス コードが必要な場合: ARXML 仕様で、ランナブルが返すことができるエラー ステータス コードを定義します。ランナブルの開発時に、開発者は事前定義されたもの以外のエラー ステータス コードも必要であることに気付きます。ただし、開発者がこの新しいエラー ステータス コードを使用すると、仕様に違反するリスクがあります。
• 実行時に変数が制約範囲外の値を取得する場合: ARXML 仕様で、特定のデータ型に対する制約範囲を定義します。制約範囲は、車両速度などの物理量から算出されます。ランナブルがデータ型に制約のある変数を他のランナブルに渡す場合はいつでも、その変数が指定された範囲内の値を持っていると考えます。しかし、実行時には、開発者が気づかないうちに、ある予期せぬ実行パス (コード中の if ステートメントの分岐など) により、その範囲外の値を変数が取得する可能性があります。

上記の状況は、仕様がコードの状態を正確に反映しなくなったことを示しています。少なくとも、コードの修正が必要です。

開発プロセスを自動化するツール

このような状況を自動的に検出し、仕様やコードを修正するように設計されたツールがあれば便利だと思いませんか?ソフトウェア設計者と開発者のやりとりは間違いなく容易になるでしょう。

さらに、既に利用可能な ARXML 仕様書以外に、ツールに追加の設定をする必要がないとしたら、もっと都合が良いと思いませんか?そのツールが、オーバーフローやゼロ除算など、他のランタイムエラーもチェックしてくれるとしたら一層便利です。

いいニュースがあります。Polyspace Code Prover の新しい AUTOSAR 機能は、この機能をすべて備え、開発プロセスの自動化に役立ちます。

Polyspace Code Prover は AUTOSAR ワークフローにどのように適合しますか?

Polyspace Code Prover は、AUTOSAR ソフトウェア コンポーネントのコード実装に対して、静的プログラム解析を実行します。

用意する必要があるのは、ARXML 仕様とコードの実装 (C ファイル) を含む 2 つの物理フォルダーのみです。Polyspace Code Prover は、ソフトウェア コンポーネントの仕様に基づき、コードをモジュールに分割します。各モジュールには、1 つのソフトウェア コンポーネントの内部動作で定義されたランナブルを実装する C ファイルが含まれます。また、各モジュールには、それらのランナブルから呼び出される関数を持つ他の C ファイルが含まれます。

次に、解析により、各モジュールに対して次の項目のチェックが行われます。

• ARXML 仕様との不一致。これらのチェックでは、以下の状態を判定します。
  • すべてのランナブルが実装されている。
  • ランナブルを実装する関数が、ARXML のデータ型仕様に従っている。(このチェックは、上述した、新しいエラー ステータス コードが必要な状況をカバーします。)
  • 他のランナブルとの通信に使用される関数 Rte_ が、ARXML のデータ型仕様に従っている。(このチェックは、上述した、制約範囲外の値を変数が取得する状況をカバーします)。

• ランタイムエラー。これらのチェックは、ランナブルの本体に特定の種類のランタイムエラー (オーバーフローなど) がないことを証明することを目的としています。

チェック結果は、Polyspace の通常の色 (有効であることが証明された場合は緑、無効である場合は赤、手作業での確認が必要な場合はオレンジ) で表示されます。また、Polyspace のチェック結果から仕様に移動することもできます。

証明では、ARXML 仕様からのデータ型定義がチェック以外の目的でも使用されることに注意してください。ランナブル入力、関数 Rte_ の戻り値、および出力引数の正確な範囲を指定するためにも使用されます。データ型が特定の範囲に制約されている場合、証明ではそのデータ型を使用するすべての変数にこの制約範囲を使用します。

言い換えれば、証明はすべて AUTOSAR 対応であると言えます。

Polyspace Code Prover は、AUTOSAR 開発ワークフローのさまざまな時点で使用することができます。ソフトウェア開発者は、懸念のあるソフトウェア コンポーネントのコード実装をチェックすることができます。ソフトウェア設計者は、サプライヤーからのコード実装が仕様に従っているかどうかをチェックすることができます。仕様を変更する必要がある場合は、ツールをすぐに実行して、変更した場合に生じる既存のコードへの影響を確認することもできます。

ワークフローに関する提案やその他の詳細については、Polyspace Code Prover ドキュメンテーションを参照してください。

参照

• AUTOSAR 公式規格
• AUTOSAR Compendium (Part 1:Application & RTE), Oliver Scheid (based on AUTOSAR 4.0.3)
• AUTOSAR 入門: Massimo Violante 教授による講義