Simulink モデルから生成されたコードに対する Polyspace 解析の実行

このチュートリアルでは、Simulink^® モデルから生成された C/C++ コードに対して Polyspace^® 解析を実行する方法を説明します。サブシステムから生成された C/C++ コードを解析することもできます。完全なワークフローについては、Embedded Coder によって生成されたコードに対する Polyspace 解析の実行を参照してください。

前提条件

Simulink から Polyspace を実行する前に、Polyspace インストールと MATLAB^® インストールをリンクしなければなりません。MATLAB や Simulink との Polyspace の統合を参照してください。

この例で使用されるモデルを開くには、MATLAB コマンド ウィンドウで以下を実行します。

openExample('polyspace_code_prover/OpenSimulinkModelForPolyspaceAnalysisExample')

Polyspace 解析のための Simulink モデルを開く

Open the model polyspace_controller_demo.

生成されたコードでのランタイム エラーのチェック

1. [アプリ] タブで [Polyspace コード検証] を選択します。[Polyspace] タブが開きます。

2. [Polyspace] タブの [モード] セクションで [Code Prover] を選択します。

3. [解析] セクションを見つけて、ドロップダウン リストから [最上位モデルとして生成されたコード] を選択します。

4. [解析の実行] をクリックします。Polyspace は、モデルが最終コード生成の後に変更されているかどうかチェックします。生成されたコードが最新の場合、Polyspace は解析を開始します。生成されたコードが最新でないか、生成されたコードが存在しない場合、Polyspace は最初にコードを生成してから、解析を開始します。

   

あるいは、MATLAB コマンド ウィンドウから解析を開始するには、以下を入力します。

% Load model
load_system('polyspace_controller_demo');
% Generate code
slbuild('polyspace_controller_demo');
% Create Polyspace options object
mlopts = pslinkoptions('polyspace_controller_demo'); 
% Specify result folder
mlopts.ResultDir ='\cp_result';
% Set analysis to Code Prover mode
mlopts.VerificationMode = 'CodeProver'; 
% Run analysis
pslinkrun('polyspace_controller_demo', mlopts);

MATLAB コマンド ウィンドウでの Polyspace 解析の実行の詳細については、pslinkoptionsとpslinkrunを参照してください。

解析結果のレビュー

解析が完了したら、解析結果が Polyspace Platform ユーザー インターフェイスに表示されます。ツールストリップの [レビュー] をクリックして結果リスト ビューを開きます。結果には、次のように色分けされたチェックが含まれます。

• グリーン:このチェックは、指定されたデータ制約について失敗していないことが証明されたコードに表示されます。たとえば、除算演算で [ゼロ除算] エラーが発生していません。

• レッド:このチェックは、指定されたデータ制約セットについて常に失敗することが検証されたエラーに表示されます。たとえば、除算演算で常に [ゼロ除算] エラーが発生します。

• オレンジ:このチェックは、指定されたデータ制約の特定の値について失敗する可能性がある、未証明のコードに潜在的なエラーがあることを示します。たとえば、除算演算で [ゼロ除算] エラーが発生することがあります。

• グレー:チェックでは、指定されたデータ制約セットについて、到達できないコードの動作が示されます。

各結果を詳細にレビューします。Code Prover の結果で次のようにします。

1. [結果のリスト] ペインで、レッドの [不適切にデリファレンスされたポインター] チェックを見つけます。レッド チェック () をクリックします。

2. [ソース] ペインで、カーソルをフラグの付いたトークンに置きます。Polyspace から、結果に関する追加情報が示されたツールヒントが表示されます。[結果の詳細] ペインでも情報が提供されます。

レッド チェックは C Function ブロック Command_Strategy 内の手書きの C コードで発生しています。

モデルの問題のトレースと修正

Polyspace によって報告される生成されたコードの問題は、モデル内の問題に原因がある可能性があります。根本原因を調査するには、問題をモデルにトレースバックします。コード内の問題は、次のような設計の問題に原因がある可能性があります。

• サブシステムで発生して Arithmetic ブロックに入力されるスケーリングのエラー、不明なキャリブレーションおよびテストされていないデータ範囲。

• 生成されたコード内での予期せぬデータ フローにつながる飽和。

• C Function ブロックや Stateflow ブロックなどのカスタム コード ブロック内でのプログラミング エラー。

モデル例の設計の問題を修正するには、Polyspace によって報告されるランタイム エラーの根本原因を特定します。

不適切にデリファレンスされたポインター

1. [結果のリスト] ペインで、[不適切にデリファレンスされたポインター] チェックを選択します。

2. [結果の詳細] ペインで [モデルに移動] () をクリックします。

Simulink エディターでは、このエラーの発生元の C Function ブロックが強調表示されます。このブロックでは、ポインター p が 100 回インクリメントされ、array の境界の外側の *p をポイントします。rtb_x = (int16_T)(*p + 5); のデリファレンス演算によって、レッドの [不適切にデリファレンスされたポインター] チェックが表示されます。

このエラーの解決策の 1 つは、C Function ブロックの for ループの後ろの、メモリの有効な場所に *p をポイントすることです。

// After the for loop, point p to a valid memory location
p = &(array[50]);
// ...
tmp = *p + 5;

オレンジ チェック

オレンジ チェックは、特定のコードの実行パスで発生する可能性のあるランタイム エラーを表しています。オレンジ チェックをレビューして、それらの潜在的な問題の原因を順位付けします。次に例を示します。

• ゼロ除算 — このオレンジ チェックは 2 回報告されます。そのチェックの 1 つが、ステートメント rtb_y1 = (int16_T)((int16_T)(10 * 10) / (int16_T)(10 - rtb_x)) で報告されています。この問題の原因をトレースするには [モデルに移動] () をクリックします。Simulink エディターで、Divide ブロックが強調表示されます。÷ 入力がゼロに等しい実行パスでは、除算演算の結果、[ゼロ除算] エラーが発生します。

  

  このエラーを解決するには、÷ 入力がゼロでないことを確認してください。たとえば、If (Simulink) ブロックを使用して、Divide ブロックを If Action Subsystem (Simulink) に配置します。

  

  その他の [ゼロ除算] チェックも、ゼロ分母のチェックと同様の手法を使用して解決できます。

• 範囲外の配列インデックス:このオレンジ チェックは、ステートメント polyspace_controller_demo_Y.FaultTable[*i] = 10; で報告されます。この結果では、[結果の詳細] で [モデルに移動] () ボタンを使用できません。このような場合は、ソース コードで最も近くにあるモデルへのリンクをクリックします。たとえば、この潜在的なエラーの根本原因をトレースするには、オレンジ エラーの前にあるコメントのリンク [S4:76] をクリックします。Simulink エディターでは、Stateflow チャート synch_and_asynch_monitoring が強調表示されます。Stateflow^® チャートの入力変数 index までエラーをトレースします。

  

  このチェックを避けるための解決策の 1 つは、入力変数 index を制約することです。Stateflow チャートの前で Saturation ブロックを使用して、index の値を 0 から 100 に制限します。

• オーバーフロー: Polyspace は、いくつかの [オーバーフロー] オレンジ チェックを報告します。それらのチェックは、入力を制約することで解決します。たとえば、ステートメント rtb_k = (int16_T)(((int16_T)((in_rotation + in_battery_info) >> 1) * 24576) >> 10) の [オーバーフロー] オレンジ チェックを考えます。[モデルに移動] () をクリックすると、Simulink エディターで、Fault Management サブシステムの Gain ブロックが強調表示されます。

  

  [オーバーフロー] オレンジ チェックを避けるための解決策の 1 つは、Sum ブロックにフィードされる信号 in_battery_info の値を制約することです。次に例を示します。

  1. Inport ブロック Battery info をダブルクリックして、入力信号 in_battery_info をモデルに提供します。

  2. [信号属性] タブで、信号の [最大値] を 500 などの小さい値に変更します。

  この手法を使用して、同様の [オーバーフロー] オレンジ チェックに対応します。

コーディング ルール違反のチェック

コーディング ルール違反をチェックするには、Polyspace Bug Finder™ 解析を開始します。

1. [Polyspace] タブで、[設定] 、 [プロジェクトの設定]を選択し、[コーディング規約およびコード メトリクス] ノードで MISRA C:2012 コーディング規約を有効にします。構成を保存し、ウィンドウを閉じます。

2. [モード] セクションで [Bug Finder] を選択します。

3. 解析を再実行します。

あるいは、MATLAB コマンド ウィンドウで以下を入力します。

% Enable checking for MISRA C:2012 violations
mlopts.VerificationSettings = 'PrjConfigAndMisraC2012';
% Specify separate folder for Bug Finder analysis
mlopts.ResultDir ='\bf_result';
% Set analysis to Bug Finder mode
mlopts.VerificationMode = 'BugFinder'; 
% Run analysis
pslinkrun('polyspace_controller_demo', mlopts);

解析完了後、MISRA C:2012 ルール違反のリストが表示された Polyspace UI が開きます。

ブロックに注釈を付けて結果を正当化

Polyspace の結果を正当化するには、ブロックに注釈を追加します。コード解析時に、Polyspace によって結果に正当化が追加されます。結果を正当化したら、後続の解析ではそれを再度レビューする必要はありません。

1. [結果のリスト] ペインで、左上隅にあるリストから [ファイル] を選択します。

2. ファイル polyspace_controller_demo.c の関数 polyspace_controller_demo_step() で、MISRA C:2012 ルール 10.4 の違反を選択します。[ソース] ペインには、加算演算がルールに違反していることが示されます。

3. [結果の詳細] ペインで、[重大度]、[ステータス] および [コメント] フィールドにこの違反の正当化を追加します。[ステータス] を [アクションの予定なし]、[重大度] を [未設定] に設定します。

4. [ブロックへの注釈] () をクリックして、違反が発生した Simulink ブロックに注釈をコピーします。

   

   [Polyspace の注釈] との文言がブロックの下に表示され、ブロックにコードの注釈が含まれていることが示されます。

5. コードを再生成し、解析を再実行します。[結果のリスト] ペインの [重大度] 列と [ステータス] 列に、注釈が事前に設定されるようになります。

参考

トピック

• Embedded Coder によって生成されたコードに対する Polyspace 解析の実行
• 以前のリリースの Simulink を使用して生成されたコードに対する Polyspace の実行