解析レポートの結果の確認
Simulink Design Verifier レポートの生成
解析の後、Simulink® Design Verifier™ は解析結果に関する詳細な情報を含む HTML レポートを生成することができます。
解析レポートには次のハイパーリンクが含まれます。
レポートの詳細項目への移動
解析で結果を記録した Simulink モデルのオブジェクトへの移動
Simulink Design Verifier の PDF バージョンのレポートを追加生成することもできます。
解析レポートの作成
詳細な解析レポートを作成するには、解析の前または後に次のいずれかを行います。
解析の前に、[コンフィギュレーション パラメーター] ダイアログ ボックスの [Design Verifier] 、 [レポート] ペインで、[結果のレポートを生成] を選択します。Simulink Design Verifier の PDF バージョンの追加レポートを保存する場合、[追加レポートを PDF 形式で生成] を選択します。
解析の後に、Simulink Design Verifier のログ ウィンドウで HTML 形式または PDF 形式を選択して、[詳細な解析レポートを生成] をクリックします。
前付
レポートは次の 2 つの節から始まります。
タイトル
タイトル節には次の情報がリストされます。
Simulink Design Verifier が解析したモデルまたはサブシステムの名前
現在の MATLAB® セッションに関連付けられたユーザー名
Simulink Design Verifier によるレポート生成日時
目次
目次がタイトルに続きます。目次の項目をクリックすると、レポートのそれぞれの章にすばやく移動できます。
概要の章
レポートの概要の章には、次の情報が記載されます。
モデルの名前
解析が実行された MATLAB リリース
解析されたモデルの状態を表すチェックサム値
解析モード
モデル表現
テスト生成ターゲット (テスト ケース生成解析に該当)
解析のステータス
前処理時間
解析時間
解析されたオブジェクティブのステータス。これには、各ステータスのパーセンテージ数値が含まれる
解析情報の章
レポートの解析情報の章には、次の節が含まれます。
モデル情報
モデル情報の節では、モデルの現在のバージョンに関する次の情報が提供されます。
Simulink Design Verifier が解析したモデルのパスおよびファイル名
モデル バージョン
モデルの最終保存日時
モデルの最終保存者の名前
解析オプション
解析オプションの節では Simulink Design Verifier 解析の設定に関する情報が提供されます。
解析オプションの節には、Simulink Design Verifier 解析に影響を及ぼしたパラメーターがリストされます。カバレッジ フィルター処理を有効にした場合、そのフィルター ファイル名がこの節に記載されます。
メモ
これらのパラメーターの詳細は、モデルの解析オプションの構成を参照してください。
サポートされていないブロック
モデルにサポートされないブロックが含まれる場合、既定で有効化されている自動スタブにより、解析は続行されます。自動スタブが有効な場合、サポートされないブロックのインターフェイスのみが考慮され、実際の動作は考慮されません。この手法により解析の完了が可能になります。ただし、サポートされないモデル ブロックのいずれかがシミュレーションの結果に影響するものである場合、部分的な解析結果しか得られない可能性があります。
サポートされていないブロックの節は、解析でサポートされていないブロックがスタブされた場合にのみ表示されます。ここでは、サポートされていないブロックが、モデル内の各ブロックへのハイパーリンクとともに、表にリストされます。
自動スタブの詳細は、自動スタブによる非互換性処理を参照してください。
ユーザー アーティファクト
ユーザー アーティファクトの節には、Simulink Design Verifier の解析のテスト データとカバレッジ データに関する情報が示されます。
パラメーターとバリアントの制約
[パラメーターとバリアントの制約] 節の [パラメーター制約] 小節には、モデルの解析時に Simulink Design Verifier によって適用されたテスト条件に関する情報が示されます。
制約の表のハイパーリンクをクリックして、モデル内の制約に移動できます。モデル ウィンドウ内の対応する Test Condition ブロックが強調表示され、新しいウィンドウが開いてブロックの詳細が表示されます。
制約の表の Source と SourceType の列から制約に関するワークスペース情報を確認できます。これらの列には、モデル ワークスペース、ベース ワークスペース、またはデータ ディクショナリのいずれのパラメーターであるかに関する情報が格納されます。
ブロック置換の概要
ブロック置換の概要には、Simulink Design Verifier が実行したブロック置換の概要が示されます。これは、Simulink Design Verifier がモデル内でブロックを置き換えた場合にのみ表示されます。
表の各行は、Simulink Design Verifier がモデルに適用した個々のブロック置換ルールに対応します。表には以下がリストされます。
ブロック置換ルールとそのルールが指定する
BlockTypeパラメーターの値を含むファイルの名前ブロック置換の
MaskDescriptionパラメーターが指定するルールの説明Simulink Design Verifier がモデルで置き換えたブロックの名前
モデルの特定のブロック置換を見つけるには、表の Replaced Blocks 列にあるその置換名をクリックします。適用されたブロックがモデル ウィンドウで強調表示され、新しいウィンドウが開いてブロックの詳細が表示されます。
近似
近似の表の各行には、Simulink Design Verifier がモデルの解析中に使用した近似のタイプがそれぞれ示されています。
メモ
近似が行われている場合、解析結果のレビューは慎重に行ってください。まれに、近似の結果が、テスト オブジェクティブ達成に失敗したテスト ケースになったり、証明オブジェクティブを反証できない反例になったりすることがあります。たとえば、浮動小数点の丸め誤差により、指定されたしきい値を信号が超えられない場合があります。
解析のハーネス情報
[解析のハーネス情報] 節には、モデルの解析に使用される Simulink Design Verifier によって生成された解析ハーネスの概要が示されます。[解析のハーネス情報] 節には、モデルがエクスポート関数モデルか、対応する Simulink 関数をもたない Function Caller ブロックを含むモデルかに基づいて、次の小節が表示されます。
エクスポート関数解析のスケジュール. Simulink Design Verifier は、解析時に Export Functions を呼び出すための解析ハーネスを想定します。たとえば、次の表は、モデル sldvExportFunction_autosar_multirunnables の解析ハーネスを示しています。
解析用にスタブされた Simulink 関数. [解析用にスタブされた Simulink 関数] の次の表は、解析ハーネスでスタブされた Simulink 関数に対応する関数プロトタイプを示しています。
メモ
Simulink Design Verifier は、スタブされた Simulink 関数が単一のタイム ステップ中に複数回呼び出される場合、その関数の出力は変わらないと仮定します。
派生範囲の章
設計エラー検出解析では、モデルの各ブロックに対して Outports の信号値の派生範囲が計算されます。この情報は、データ オーバーフローやゼロ除算エラーの原因の特定に役立ちます。
解析レポートの [派生範囲] の章の表には、これらの範囲がリストされます。
設計エラー検出解析で Observer Reference ブロックが使用されている場合、この節では、オブザーバーの情報が [オブザーバー モデル] 小節に、設計モデルの情報が [設計モデル] 小節にそれぞれ表示されます。
[設計モデル] 小節の表は、モデル例 sldvdemo_debounce_validprop の各派生範囲のリストを示しています。
オブザーバーは設計エラー検出解析で無視されるため、[オブザーバー モデル] 節にはレポートされている派生範囲が表示されません。
オブジェクティブのステータスの章
レポートのこの節には、オブジェクティブのタイプ、タイプに対応するモデルの項目、オブジェクティブの説明、解析時間を含む、モデルのすべてのオブジェクティブに関する情報が示されます。オブジェクティブのステータスの章における解析時間は、オブジェクティブが判定された時間です。
テスト オブジェクティブのステータス: テスト ケースがテスト オブジェクティブを満たすか、満たせないか、または判定できないかを報告します。
設計エラー検出オブジェクティブのステータス: 解析によって、設計エラー、デッド ロジック、エラーなし、または不確定のいずれが検出されたかを報告します。
証明オブジェクティブ ステータス: 解析によって、プロパティが証明されたか、違反が検出されたか、または判定できないかを報告します。
一般的なオブジェクティブ ステータス: 結果が不確定であることを報告します。
解析モードに基づいたさまざまなオブジェクティブのステータスの詳細については、Understanding Objective Statusesを参照してください。
近似の存在を識別し、各オブジェクティブ ステータスのレベルで近似をレポートします。詳細については、結果の近似についてを参照してください。次の表は、Simulink Design Verifier の解析モードのオブジェクティブ ステータスをまとめています。
モデル項目の章
レポートのモデル項目の章には、カバレッジ オブジェクティブを定義するモデルの各オブジェクトの表が含まれます。それぞれのオブジェクトの表には、すべての関連付けられたオブジェクティブが、オブジェクティブのタイプ、説明および解析終了時のステータスと共にリストされます。
モデルの個々のオブジェクトの表は、ここにあるような、モデル例 sldvdemo_cruise_control の PI Controller サブシステムについての Discrete-Time Integrator の表と似ています。
モデルの特定のオブジェクトを強調表示するには、表の左上隅にある「表示」をクリックすると新しいウィンドウが開き、オブジェクトの詳細が表示されます。個々のオブジェクティブに適用されたテスト ケースの詳細を表示するには、表の最後の列にあるテスト ケース番号をクリックします。
プロパティ証明解析で Observer Reference ブロックが使用されている場合、各モデル項目節では、オブザーバーの情報が [オブザーバー モデル] 小節に、設計モデルの情報が [設計モデル] 小節にそれぞれ表示されます。モデル内にテスト オブジェクティブが見つからない場合、これらの小節は空になります。
この表は、モデル例 sldvdemo_debounce_testobjblks にある設計モデルのテスト オブジェクティブの 1 つを示しています。
この表は、モデル例 sldvdemo_debounce_testobjblks にあるオブザーバー モデルのテスト オブジェクティブの 1 つを示しています。
設計エラーの章
設計エラー検出解析を実行し、その解析でモデル内に設計エラーが検出された場合、レポートに [設計エラー] の章が含まれます。この章では、解析によって反証された設計エラーについてまとめます。
目次
設計エラーの章には目次があります。目次の各項目は、個々の設計エラーに関する結果へのハイパーリンクになっています。
概要
概要節では以下がリストされます。
モデルの項目
検出された設計エラーのタイプ (オーバーフローまたはゼロ除算)
解析のステータス (反証または証明された有効性)
次の例では、sldvdemo_debounce_falseprop モデルが解析され、設計エラーが検出されています。Verify True Output という名前の Verification Subsystem の Sum ブロックでオーバーフロー エラーが検出されています。
テスト ケース
テスト ケース節には、テスト ケースが設計エラーのオブジェクティブを反証したタイム ステップと対応する時間がリストされます。Inport ブロック raw の値は 255 であり、これによってオーバーフロー エラーが発生しました。
テスト ケースの章
テスト生成解析を実行すると、レポートには [テスト ケース] の章が含まれます。この章では、解析で生成されたテスト ケースを節にまとめて記述しています。
目次
テスト ケースの章には目次があります。目次の各項目は、個々のテスト ケースに関する情報へのハイパーリンクになっています。
概要
概要節では以下がリストされます。
テスト ケースを構成する信号の長さ
テスト ケースが達成するテスト オブジェクティブの合計数
オブジェクティブ
オブジェクティブの節には以下がリストされます。
テスト ケースがそのオブジェクティブを達成するタイム ステップ。
テスト ケースがそのオブジェクティブを達成する時間。
そのオブジェクティブに関連付けられたモデルの項目へのリンク。リンクをクリックすると、Simulink エディターでそのモデルの項目が強調表示されます。
テスト オブジェクティブのステータスの章とテスト ケースの章の間を移動するリンクを使用して達成されたオブジェクティブ。
生成された入力データ
生成された入力データの節では、モデルの項目に関連付けられた各入力信号について、テスト ケースが個々のテストオブジェクティブを達成するタイム ステップおよび対応する時間がリストされます。信号値がそれらのタイム ステップの間変化しない場合、表にはタイム ステップと時間が範囲としてリストされます。
メモ
生成された入力データの表では、信号値がテスト オブジェクティブに影響しないタイム ステップについては、信号値としての数値ではなく、ダッシュ (–) が表示されます。信号のどの値も影響していない場合は、その信号全体が表から除外されます。ハーネス モデルでは、[結果に影響しないデータをランダム化] パラメーターを有効にしない限り、Inputs ブロックにはこれらの値が 0 で示されます (結果に影響しないデータをランダム化を参照)。
期待される出力
[コンフィギュレーション パラメーター] ダイアログ ボックスの [Design Verifier] 、 [結果] ペインで [期待される出力値を含める] を選択すると、レポートにはテスト ケースごとの [期待される出力] 節が記載されます。この表には、モデルの項目に関連付けられたそれぞれの出力信号について、各タイム ステップで想定される出力値がリストされます。
Long Test Cases
[テスト スイートの最適化] オプションを [LongTestcases] に設定すると、レポートの Test Cases の章にはより長いテスト ケースに関する、より少数の節が記載されます。
プロパティの章
プロパティ証明解析を実行すると、レポートには Properties の章が含まれます。この章では、このソフトウェアが生成した証明オブジェクティブおよび反例を節にまとめて記述しています。
目次
プロパティの章には目次があります。目次の各項目は、反証された個々のプロパティに関する情報へのハイパーリンクになっています。
プロパティ証明解析で Observer Reference ブロックが使用されている場合、各プロパティの章では、オブザーバーの情報が [オブザーバー モデル] 小節に、設計モデルの情報が [設計モデル] 小節にそれぞれ表示されます。モデル内にプロパティがない場合は空になります。
この表は、モデル例 sldvdemo_debounce_validprop にあるオブザーバー モデルのプロパティの 1 つを示しています。
概要
概要節では以下がリストされます。
このソフトウェアが解析したモデルの項目
評価されたプロパティのタイプ
解析のステータス
次の例では、sldvdemo_cruise_control_verification モデルが解析され、プロパティが証明されています。BrakeAssertion という名前の Assertion ブロックへの入力が非ゼロであることが、解析により証明されています。
反例
Counterexample 節には、反例がプロパティを反証したタイム ステップと対応する時間がリストされます。この節には、そのタイム ステップでの信号値もリストされます。
