Main Content

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

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

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

  • Polyspace Bug Finder™ では、コードのバグまたはコーディング ルール違反がチェックされます。

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

このチュートリアルでは、Simulink モデルから生成されたコードに対して Polyspace 解析を実行する方法を説明します。完全なワークフローについては、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 コード検証] を選択します。

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

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

    Polyspace により Code Prover 解析が開始されます。

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

あるいは、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);
pslinkoptionsおよびpslinkrunを参照してください。

解析結果のレビュー

解析完了後、Polyspace ユーザー インターフェイスで検証結果が開きます。検証結果には、次のように色分けされたチェックが含まれます。

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

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

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

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

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

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

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

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

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

モデルから生成されたコードのエラーは、モデル内の問題に原因があります。根本原因を調査するには、エラーをモデルにトレースバックします。

エラー 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;

Simulink エディターでは、このエラーの発生元が強調表示されます。この場合、Stateflow チャート synch_and_asynch_monitoring での遷移が原因でエラーが発生しています。Stateflow チャートの入力変数 index までエラーをトレースします。

オレンジの [範囲外の配列インデックス] 違反を避けるために考えられる解決策の 1 つは、入力変数 index を制約することです。Stateflow チャートの前で Saturation ブロックを使用して index を 0 と 100 の間に制限します。変更したモデルで解析を実行すると、オレンジ チェックが解決されます。

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

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

    /* 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);
    

  2. [ソース] ペインで、エラーをレビューします。エラーをモデルにトレースバックするには、オレンジ エラーの上のコメントにあるリンク [S1/Gain] をクリックします。Simulink エディターでは、このエラーの発生元が強調表示されます。この場合、Gain ブロックに続く Sum ブロック内の Fault Management サブシステムでエラーが発生しています。

[オーバーフロー] オレンジ エラーを避けるための考えられる解決策の 1 つは、Sum ブロックにフィードされる信号 in_battery_info の値を制約することです。

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

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

変更したモデルで解析を実行すると、オレンジ チェックが解決されます。

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

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

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

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

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

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

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

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

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

  2. [Polyspace] タブで [Bug Finder] を選択します。

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

あるいは、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 では検証結果に正当化を追加します。検証結果を正当化したら、それを再度レビューする必要はありません。

  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'
    */
    rtb_k = (int16_T)(((int16_T)((in_rotation + in_battery_info) >> 1) * 24576) >>
                       10);

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

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

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

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

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

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

関連するトピック