Main Content

このページの翻訳は最新ではありません。ここをクリックして、英語の最新版を参照してください。

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

Simulink® モデルやサブシステムから生成されたコードに対して Polyspace® を実行できます。

  • Polyspace Bug Finder™ では、コードのバグまたはコーディング ルール違反 (MISRA C®:2012 ルールなど) がチェックされます。

  • Polyspace Code Prover™ では、コードのランタイム エラーが網羅的にチェックされます。

コード生成に Embedded Coder® を使用する場合、このチュートリアルでは、単純な Simulink モデルから生成されたコードに対して Polyspace を実行する方法を説明します。完全なワークフローについてはEmbedded Coder によって生成されたコードに対する Polyspace 解析の実行を参照してください。

前提条件

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

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

openExample('polyspace_code_prover/OpenModelForCodeGenerationAndPolyspaceAnalysisExample')

コード生成および Polyspace 解析向けにモデルを開く

コード生成および Polyspace 解析の設定を行うためにモデル polyspace_controller_demo を開きます。

コードの生成と解析

モデルから生成されたコードの Polyspace 解析を開始するには、以下を行います。

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

  2. [Polyspace] タブで [解析] フィールドを見つけて、ドロップダウン メニューから [最上位モデルとして生成されたコード] を選択します。

  3. キャンバスの任意の場所をクリックします。[次のコードの解析] フィールドにモデル名が表示されます。[解析の実行] を選択します。

[解析の実行] をクリックすると、生成コードを Polyspace がチェックします。生成コードが存在しない場合、Polyspace は Embedded Coder を使用してコードを生成してから、解析を開始します。

等価な MATLAB コード:

load_system('polyspace_controller_demo');
slbuild('polyspace_controller_demo');
mlopts = pslinkoptions('polyspace_controller_demo'); 
mlopts.ResultDir ='\result'
mlopts.VerificationMode = 'CodeProver'; 
pslinkrun('polyspace_controller_demo', mlopts);
Bug Finder を使用して解析するには、CodeProverBugFinder に置き換えます。コードの詳細については、pslinkoptionsおよびpslinkrunを参照してください。

解析結果のレビュー

解析後、検証結果が Polyspace ユーザー インターフェイスに表示されます。

Bug Finder を実行する場合、検証結果には、生成されたコード内で検出されたバグが含まれます。Code Prover を実行する場合、検証結果には、次のように色分けされたチェックが含まれます。

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

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

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

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

解析結果を詳細にレビューします。以下に Code Prover の検証結果での例を示します。

  1. [検証結果のリスト] ペインで、レッドになった [範囲外の配列インデックス] チェックを選択します。

  2. [ソース] ペインでカーソルをレッド チェックに置き、追加情報を表示します。たとえば、赤い [ 演算子のツールヒントでは、配列サイズおよび配列インデックスで可能な値が記述されています。[検証結果の詳細] ペインでも情報が提供されます。

エラーは手書きの C ファイル Command_strategy_file.c に発生しています。C ファイルは、(モデル参照 relative threshold において) Reduced Precision サブシステムの S-Function ブロック Command_Strategy 内にあります。

エラーをモデルにトレースバックして修正

モデルから生成されたコードについては、エラーをモデルにトレースバックできます。以下の節では、特定の Code Prover の検証結果をモデルに再度トレースする方法を説明します。

エラー 1: 範囲外の配列インデックス

  1. [検証結果のリスト] ペインで、ファイル polyspace_controller_demo.c で発生している [範囲外の配列インデックス] オレンジ エラーを選択します。

  2. [ソース] ペインで、オレンジ エラーの上のコメントにあるリンク [S4:76] をクリックします。

    /* Transition: '<S4>:75' */
    /* Transition: '<S4>:76' */
    (*i)++;
    
    /* Outport: '<Root>/FaultTable' */
    polyspace_controller_demo_Y.FaultTable[*i] = 10;

Stateflow チャート synch_and_asynch_monitoring での遷移が原因でエラーが発生していることがわかります。エラーは Stateflow チャートの入力変数 index にトレースできます。

範囲外の配列インデックスを回避する方法はいくつかあります。1 つの方法は、Stateflow チャートの前に Saturation ブロックを使用して入力変数 index を制約することです。

エラー 2: オーバーフロー

  1. [検証結果のリスト] ペインで、以下で示されている [オーバーフロー] オレンジ エラーを選択します。エラーがファイル polyspace_controller_demo.c に表示されます。

  2. [ソース] ペインで、エラーをレビューします。エラーをモデルにトレースバックするには、オレンジ エラーの上のコメントにあるリンク [S1/Gain] をクリックします。

    /* Gain: '<S1>/Gain' incorporates:
    * Inport: '<Root>/Battery Info'
    * Inport: '<Root>/Rotation'
    * Sum: '<S1>/Sum1'
    */
    
    Gain = (int16_T)(((int16_T)((in_rotation + in_battery_info) >> 1) * 24576) >>
                       10);
    
    Gain ブロックに続く Sum ブロック内の Fault Management サブシステムでエラーが発生していることがわかります。

オーバーフローを回避する方法はいくつかあります。1 つの方法は、Sum ブロックにフィードされる信号 in_battery_info の値を制約することです。信号を制約するには、次のようにします。

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

  2. [信号属性] タブで、信号の [最大値] を変更します。

このモデルのエラーは、次のうちのいずれかが原因で発生しています。

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

  • Stateflow のイベントベース モデリングや手書きのルックアップ テーブル関数での配列操作。

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

  • Stateflow のプログラミング エラー。

エラーの根本原因を特定したら、モデルを適切に変更して問題を修正することができます。

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

コーディング ルール違反をチェックするには、コード解析を開始する前に、以下のことを行います。

  1. [Polyspace] タブで [設定] を選択します。

  2. [コンフィギュレーション パラメーター] ダイアログ ボックスで、[検証設定] リストにある該当オプションを選択します。たとえば、[プロジェクト コンフィギュレーションおよび MISRA C 2012 AGC のチェック] を選択します。

    MISRA C:2012 ルールのチェックには Bug Finder を実行することをお勧めします。[Polyspace] タブで [Bug Finder] を選択します。

  3. [適用] または [OK] をクリックして、解析を再実行します。

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

検証結果は、ブロックに注釈を追加することによって正当化できます。コード解析において、Polyspace Code Prover は注釈を読み取り、検証結果に正当化を追加します。検証結果を正当化したら、それを再度レビューする必要はありません。

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

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

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

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

    Sum ブロックでルール違反が発生することがわかります。

    このブロックに注釈を付けてルール違反を正当化するには、以下のことを行います。

    1. ブロックを選択します。[Polyspace] タブで [注釈の追加] を選択します。

    2. [注釈タイプ]MISRA-C-2012 を選択し、ルール違反に関する情報を入力します。[ステータス][アクションの予定なし][重大度][未設定] に設定します。

    3. [適用] または [OK] をクリックします。[Polyspace の注釈] との文言がブロックの下に表示され、ブロックにコードの注釈が含まれていることが示されます。

    4. コードを再生成し、解析を再実行します。[検証結果のリスト] ペインの [重大度] 列と [ステータス] 列に、注釈が入力されます。

関連するトピック