モデルの解析の実行

この例について

以下のセクションでは、モデル例 sldvdemo_cruise_control について説明します。この例では、Simulink^® Design Verifier™ を使用した、完全なモデルカバレッジを達成するテストケースの生成方法を示します。この例を通じて、Simulink Design Verifier でモデルを解析し、結果を解釈する方法を学習します。

モデルを開く

sldvdemo_cruise_control モデルを開くには、MATLAB^® プロンプトで次のように入力します。

openExample('sldv/CruiseControlTestGenerationExample',...
'supportingFile', 'sldvdemo_cruise_control');

テストケースの生成

解析の実行
解析結果の生成
解析結果をモデル上で強調表示
詳細な解析レポート: (HTML) (PDF)
ハーネスモデルの作成
Simulate Tests and Produce Model Coverage Report
テストケース/反例をスプレッドシートに保存

解析の実行

sldvdemo_cruise_control モデルのテストケースを生成するには、[テストの生成] をクリックします。

Simulink Design Verifier がテストケースを生成するためにモデルの解析を開始すると、[Simulink Design Verifier の結果の概要] ウィンドウが開きます。結果の概要ウィンドウには実行中のログが表示され、解析の進行状況がわかります。

実行中の解析の終了が必要な場合は、[停止] をクリックします。結果を生成するかどうかを尋ねられます。[はい] をクリックすると、その時点で達成された結果に基づいてデータファイルが作成されます。結果の概要ウィンドウにデータファイルのパス名が表示されます。

データファイルは、sldvData という名前の構造体が含まれる MAT ファイルです。この構造体には、解析時に収集および生成されたデータが格納されます。

詳細は、Simulink Design Verifier データファイルの管理を参照してください。

解析結果の生成

Simulink Design Verifier が sldvdemo_cruise_control モデルの解析を完了すると、[結果の概要] ウィンドウにはいくつかのオプションが表示されます。その一部を以下に示します。

解析結果をモデル上で強調表示
詳細な解析レポート: (HTML) (PDF)
ハーネスモデルの作成
テストをシミュレートしてモデルカバレッジレポートを生成
テストケース/反例をスプレッドシートに保存

メモ

他のモデルを解析する場合、解析の結果によっては、オプションのサブセットが表示される場合があります。

次節以降では、これらのオプションについて詳しく説明します。

解析結果をモデル上で強調表示

[Simulink Design Verifier の結果の概要] ウィンドウで、[解析結果をモデル上で強調表示] をクリックすると、解析結果に基づいてモデルのオブジェクトが 3 色で強調表示されます。

グリーン: 達成されたオブジェクティブ
オレンジ: 未判定のオブジェクティブ
レッド: 達成されないオブジェクティブ

モデルの解析結果を強調表示すると、Simulink Design Verifier 結果インスペクターが開きます。解析結果があるモデルのオブジェクトをクリックすると、結果インスペクターにはそのオブジェクトの結果概要が表示されます。

グリーン: 達成されたオブジェクティブ. グリーンのアウトラインは、解析によりそのブロックのすべてのオブジェクティブについてテストケースが生成されたことを示します。ブロックがサブシステムまたは Stateflow^® Atomic サブチャートの場合、グリーンのアウトラインは、子オブジェクトに関連付けられたすべてのオブジェクティブについてのテストケースが解析により生成されたことを示します。

たとえば、sldvdemo_cruise_control モデルでは、グリーンのアウトラインは PI コントローラーサブシステムがすべてのテストオブジェクティブを達成していることを示します。結果インスペクターには、PI コントローラーサブシステムの 2 つの達成されたテストオブジェクティブがリストされます。

オレンジ: 未判定のオブジェクティブ. オレンジのアウトラインは、オブジェクティブが達成されるかどうかを特定できなかったことを示します。この状況は次のような場合に発生します。

解析のタイムアウト
次の事象によりテストケースが生成されることなくテストオブジェクティブが達成された場合
- 自動スタブエラー
- 解析エンジンの制限

レッド: 達成されないオブジェクティブ. レッドのアウトラインは、解析でテストケースを生成できなかったオブジェクティブがいくつかあったことを示します。多くの場合、モデルに到達不可能な設計要素があることが原因です。

次の例では、入力 2 は Switch ブロックの条件を常に満たすため、Switch ブロックは入力 3 の値を通過させることはありません。

詳細な解析レポート: (HTML) (PDF)

[Simulink Design Verifier の結果の概要] ウィンドウで、[詳細な解析レポート: (HTML) (PDF)] の [HTML] をクリックすると、解析の詳細なレポートが保存されて開きます。レポートのパスは次のとおりです。

<current_folder>/sldv_output/...
     sldvdemo_cruise_control/sldvdemo_cruise_control_report.html

HTML レポートには次の章があります。

それぞれのレポートの章の説明は、以下を参照してください。

概要
解析情報
テストオブジェクティブのステータス
モデル項目
テストケース

概要. [目次] で、[概要] をクリックすると概要の章が表示されます。その中の [解析情報] サブセクションの下に次の情報が記載されています。

モデルの名前
リリースおよびチェックサム情報
解析のモード (テスト生成、プロパティ証明、設計エラー検出)
解析のステータス
解析の長さ (秒)

[概要] の下の [オブジェクティブのステータス] サブセクションには、達成されたオブジェクティブの数が表示されます。

解析情報. [目次] で [解析情報] をクリックすると、解析されたモデルと解析オプションに関する情報が表示されます。これらのオプションのいずれかをクリックすると、モデル解析の詳細を確認できます。

テストオブジェクティブのステータス. [目次] で [テストオブジェクティブのステータス] をクリックすると、達成されたオブジェクティブが表で示されます。次の図は、sldvdemo_cruise_control モデルで達成されたオブジェクティブのリストの一部です。

オブジェクティブのステータス

Objectives Satisfied の表には、モデルについて次の情報がリストされます。

# — オブジェクティブの番号
タイプ — オブジェクティブのタイプ
モデル項目 — オブジェクティブのテスト対象のモデル内要素。このリンクをクリックすると、要素が強調表示された状態でモデルが表示されます。
説明 — オブジェクティブの説明
テストケース — オブジェクティブを達成するテストケース。このリンクをクリックすると、そのテストケースに関する詳細な情報が表示されます。

オブジェクティブ 32 の行で、テストケース番号 (5) をクリックすると、レポートの [テストケース] の章のテストケース 5 に関する詳細情報が表示されます。

テストケース 5

この例では、テストケース 5 は 1 つのオブジェクティブを達成します。これは、積分結果が Discrete-Time Integrator ブロックの上限 T 以上となるというものです。この表は、0 秒から 0.06 秒まで間の 6 つの信号の値をリストしています。

モデル項目. [目次] で [モデル項目] をクリックすると、カバレッジオブジェクティブを定義するモデルの各項目についての詳細な情報が表示されます。この表では、解析の終了時におけるオブジェクティブのステータスが示されます。達成されたオブジェクティブの詳細情報については、表内のリンクをクリックしてください。

モデル項目 - Controller/Switch3

モデル項目 - Controller/Switch2

テストケース. [目次] で [テストケース] をクリックすると、生成されたそれぞれのテストケースに関する詳細情報が表示されます。ここには次の情報が記載されています。

テストケースの実行時間の長さ
達成されたオブジェクティブの数
達成されたオブジェクティブに関する詳細情報
入力データ

ハーネスモデルの作成

[Simulink Design Verifier の結果の概要] ウィンドウで、[ハーネスモデルの作成] をクリックすると、sldvdemo_cruise_control_harness という名前のハーネスモデルが作成されて開きます。

Harness model sldvdemo_cruise_control_harness.

このハーネスモデルには次のブロックが含まれています。

Test Case Explanation ブロックは、生成されたテストケースをドキュメント化する DocBlock ブロックです。Test Case Explanation ブロックをダブルクリックすると、テストケースで達成されたオブジェクティブの各テストケースの説明が表示されます。
Test Unit ブロックは、ソフトウェアで解析された元のモデルのコピーを含む Subsystem ブロックです。Test Unit ブロックをダブルクリックすると、その内容が表示され、sldvdemo_cruise_control モデルのコピーであることを確認できます。
メモ
サブシステムの代わりに Model ブロックを使用して、解析中のモデルを参照するハーネスモデルを構成できます。[コンフィギュレーションパラメーター] ダイアログボックスの [Design Verifier]、[結果] ペインで、[解析後に別のハーネスモデルを生成] と [生成されたハーネス内の入力モデルを参照] を選択します。
Inputs ブロックは、生成されたテストケースの信号を含む Signal Editor ブロックです。Inputs ブロックをダブルクリックすると、[信号エディター] ダイアログボックスが開き、8 つのテストケースの信号が表示されます。
Size-Type ブロックは、信号を Inputs ブロックから Test Unit ブロックに送信するサブシステムです。このブロックは、信号のサイズおよびデータ型が Test Unit ブロックと一致することを検証します。

Inputs ブロックの [ブロックパラメーター] ダイアログボックスには 3 つのテストケースがあります。

テストケース 3 を表示するには、[アクティブなシナリオ] のリストから [TestCase_3] を選択し、[信号エディターを開く] ボタンをクリックして信号エディターを開きます。
0.01 秒時点のテストケース 3 は次のとおりです。
- enable 信号と inc 信号は 1 のまま。
- brake 信号と dec 信号は 0 のまま。
- set 信号は 1 から 0 に遷移。
- speed 信号は 100 から 0 に遷移。
Inputs ブロックでは、信号グループは Test Case Explanation ブロックで記述されたテストオブジェクティブを達成します。
Simulink Design Verifier で完全なモデルカバレッジを達成したことを確認するには、すべてのテストケースを使用してハーネスモデルのシミュレーションを実行します。ハーネスモデルのツールストリップで [すべて実行 (カバレッジ)] をクリックします。
Simulink ソフトウェアによりすべてのテストケースがシミュレートされます。Simulink Coverage™ ソフトウェアは、ハーネスモデルのカバレッジデータを収集して、カバレッジレポートを表示します。レポートの概要には、sldvdemo_cruise_control_harness モデルが 100% のカバレッジを達成したことが示されます。
概要

Simulate Tests and Produce Model Coverage Report

[Simulink Design Verifier の結果の概要] ウィンドウで、[テストをシミュレートしてモデルカバレッジレポートを生成] をクリックすると、モデルのシミュレーションが実行され、sldvdemo_cruise_control モデルのカバレッジレポートが生成されます。レポートは、次のパスと名前を使用して保存されます。

current_folder/sldv_output/sldvdemo_cruise_control/...
		sldvdemo_cruise_control_report.html

[すべてを実行しカバレッジを生成] をクリックしてハーネスモデルでテストをシミュレートすると、このカバレッジレポートとモデルそのものに対して生成されたレポートとの間に以下のような差異が見られる場合があります。

ハーネスモデルカバレッジレポートには、追加のタイムステップが含まれる場合があります。ハーネスモデルのカバレッジを収集する場合、モデルの終了時間は最も長いテストケースの終了時間に等しくなります。そのため、より短いテストケースのシミュレーションを実行すると、追加のカバレッジを達成できる場合があります。
ハーネスモデルの Test Unit サブシステムの循環的複雑度のカバレッジは、ハーネスモデルの構造上、モデル自体のカバレッジと異なる場合があります。

テストケース/反例をスプレッドシートに保存

生成されたテストケースまたは反例をスプレッドシートに保存する場合は、[Simulink Design Verifier の結果の概要] ウィンドウで [テストケース/反例をスプレッドシートに保存] をクリックします。

テストケースの組み合わせ

より少数のテストケースにまとめて結果をレビューする場合は、[テストスイートの最適化] パラメーターを [LongTestcases] に設定します。[LongTestcases] 最適化手法を使用する場合、解析で生成されるテストケースは少なくなりますが、より長く、それぞれが複数のテストオブジェクティブを達成するものとなります。

sldvdemo_cruise_control モデルを開き、LongTestcases 最適化手法を指定して解析を再実行します。

[Design Verifier] タブの [準備] セクションのモード設定のドロップダウンメニューから、[設定] をクリックします。
[コンフィギュレーションパラメーター] ダイアログボックスの [Design Verifier] ペインで、[テスト生成] を選択し、[テストスイートの最適化] パラメーターを [LongTestcases] に設定します。[適用] と [OK] をクリックして [コンフィギュレーションパラメーター] ダイアログボックスを閉じます。
sldvdemo_cruise_control モデルで [テストの生成] をクリックします。
結果の概要ウィンドウで [ハーネスモデルの作成] をクリックします。
ハーネスモデルの Inputs ブロックと Test Case Explanation ブロックに、前に作成された 8 つの短いテストケースの代わりに、今回は 1 つの長いテストケースが含まれています。
[すべてを実行しカバレッジを生成] をクリックして、カバレッジを収集します。
こちらの解析でも、34 のオブジェクティブすべてが達成されています。