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.

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

[アプリ] タブで [Polyspace コード検証] を選択します。[Polyspace] タブが開きます。
[Polyspace] タブの [モード] セクションで [Code Prover] を選択します。
[解析] セクションを見つけて、ドロップダウンリストから [最上位モデルとして生成されたコード] を選択します。
[解析の実行] をクリックします。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 ユーザーインターフェイスに表示されます。結果には、次のように色分けされたチェックが含まれます。

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

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

[結果のリスト] ペインで、レッドになった [範囲外の配列インデックス] チェックを見つけます。レッドチェック () をクリックします。
[ソース] ペインでカーソルを [ 演算子のレッドチェックに置き、ツールヒントを表示します。配列サイズおよび配列インデックスで可能な値が記述されています。[結果の詳細] ペインでも情報が提供されます。

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

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

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

サブシステムで発生して Arithmetic ブロックに入力されるスケーリングのエラー、不明なキャリブレーションおよびテストされていないデータ範囲。
生成されたコード内での予期せぬデータフローにつながる飽和。
C Function ブロックや Stateflow ブロックなどのカスタムコードブロック内でのプログラミングエラー。

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

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

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

[ソース] ペインで、エラーの上のコメントにあるリンク [<Root>/Command strategy] をクリックします。

  /* CFunction: '<Root>/Command strategy' incorporates:
   *  DataTypeConversion: '<S3>/Cast4'
   *  Inport: '<Root>/Battery info'
   */
  //...
  p = &array[0];
  for (i = 0; i < 100; i++) {
   *p = 0;
    p = &p[1];
  }
  rtb_x = (int16_T)((uint16_T)rtb_y1 - in_battery_info);
  if (rtb_x < 3) {
    rtb_x = (int16_T)(*p + 5);
  //...

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;

範囲外の配列インデックス

[結果のリスト] ペインで、[範囲外の配列インデックス] チェックを選択します。

[ソース] ペインで、エラーの上のコメントにあるリンク [<Root>/Command strategy] をクリックします。

  /* CFunction: '<Root>/Command strategy' incorporates:
   *  DataTypeConversion: '<S3>/Cast4'
   *  Inport: '<Root>/Battery info'
   */
  //...
   for (i = 0; i < 100; i++) {
    *p = 0;
    p = &p[1];
  }
  //...
  if ((rtb_x > 92) && (rtb_x < 110)) {
    if (another_array[(rtb_x - i) + 9] != 0) {
      rtb_x = 92;
    } else {
      rtb_x = 91;
    }
  }

Simulink エディターでは、このエラーの発生元の C Function ブロックが強調表示されます。このブロックでは、i の値は、最初の for ループの後で 100 に設定されています。ステートメント if ((rtb_x > 92) && (rtb_x < 110)) は、rtb_x が取り得る値を 93..109 に制限します。ステートメント another_array[(rtb_x - i) + 9] != 0 では、another_array の可能なインデックスの範囲は 93+9-100 = 2 から 109+9-100 = 18 です。配列 another_array には 2 つの要素しかないため、another_array[(rtb_x - i) + 9] で配列にアクセスすると、レッドの [範囲外の配列インデックス] 実行時チェックになります。

このエラーの解決策の 1 つは、式 [(rtb_x - i) + 9] が 0 または 1 として評価されるように、rtb_x に対する優先条件を変更することです。

if ((rtb_x > 91) && (rtb_x < 93)) {
    if (another_array[(rtb_x - i) + 9] != 0) {
      rtb_x = 92;
    } else {
      rtb_x = 91;
    }
  }

オレンジチェック

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

ゼロ除算 — このオレンジチェックは 2 回報告されます。そのチェックの 1 つが、ステートメント rtb_y1 = (int16_T)((int16_T)(10 * 10) / (int16_T)(10 - rtb_x)) で報告されています。この潜在的なエラーの可能性をトレースするには、コメント <S6>/Divide をクリックします。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) の [オーバーフロー] オレンジチェックを考えます。チェックをモデルにトレースバックするには、オレンジチェックの上のコメントにあるリンク [S1/Gain] をクリックします。Simulink エディターでは、Fault Management サブシステムの Gain ブロックが強調表示されます。

[オーバーフロー] オレンジチェックを避けるための解決策の 1 つは、Sum ブロックにフィードされる信号 in_battery_info の値を制約することです。次に例を示します。
1. Inport ブロック Battery info をダブルクリックして、入力信号 in_battery_info をモデルに提供します。
2. [信号属性] タブで、信号の [最大値] を 500 などの小さい値に変更します。
この手法を使用して、同様の [オーバーフロー] オレンジチェックに対応します。

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

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

[Polyspace] タブで、[設定] 、 [プロジェクトの設定]を選択し、[コーディング規約およびコードメトリクス] ノードで MISRA C:2012 コーディング規約を有効にします。コンフィギュレーションを保存し、ウィンドウを閉じます。
[モード] セクションで [Bug Finder] を選択します。
解析を再実行します。

あるいは、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 によって結果に正当化が追加されます。結果を正当化したら、後続の解析ではそれを再度レビューする必要はありません。

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

[ソース] ペインで、加算演算の上のコメントにあるリンク [S1/Sum1] をクリックします。

/* Gain: '<S1>/Gain' incorporates:
* Inport: '<Root>/Battery Info'
* Inport: '<Root>/Rotation'
* Sum: '<S1>/Sum1'
*/
rtb_k = (int16_T)(((int16_T)((in_rotation + in_battery_info) >> 1) * 24576) >>
                   10);

Sum ブロックでルール違反が発生しています。

このブロックに注釈を付けてルール違反を正当化するには、以下のことを行います。
1. ブロックを選択します。[Polyspace] タブで [注釈の追加] を選択します。
2. [注釈タイプ] に [MISRA-C-2012] を選択し、ルール違反に関する情報を入力します。[ステータス] を [アクションの予定なし]、[重大度] を [Unset] に設定します。
3. [適用] または [OK] をクリックします。[Polyspace の注釈] との文言がブロックの下に表示され、ブロックにコードの注釈が含まれていることが示されます。
コードを再生成し、解析を再実行します。[結果のリスト] ペインの [重大度] 列と [ステータス] 列に、注釈が事前に設定されるようになります。