結果の確認

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 の解析のテストデータとカバレッジデータに関する情報が示されます。

パラメーターとバリアントの制約

[パラメーターとバリアントの制約] 節の [パラメーター制約] 小節には、モデルの解析時に 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 の各派生範囲のリストを示しています。

オブザーバーは設計エラー検出解析で無視されるため、[オブザーバーモデル] 節にはレポートされている派生範囲が表示されません。

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

レポートのこの節には、オブジェクティブのタイプ、タイプに対応するモデルの項目およびオブジェクティブの説明を含む、モデルのすべてのオブジェクティブに関する情報が示されます。

設計エラー検出オブジェクティブのステータス
テストオブジェクティブのステータス
証明オブジェクティブステータス
未判定オブジェクティブのステータス

近似の存在を識別し、各オブジェクティブステータスのレベルで近似をレポートします。詳細については、Simulink Design Verifier が検証結果を使用して近似をレポートする方法を参照してください。次の表は、Simulink Design Verifier の解析モードのオブジェクティブステータスをまとめています。

解析モード	オブジェクティブステータス
設計エラー検出	デッドロジック近似におけるデッドロジックアクティブロジック - シミュレーションが必要有効なオブジェクティブ近似において有効なオブジェクティブ反例によって反証されたオブジェクティブオブジェクティブのエラー - シミュレーションが必要ゼロ除算のため未判定のオブジェクティブ非線形性のため未判定のオブジェクティブスタブのため未判定のオブジェクティブ未判定のオブジェクティブ配列が範囲外にあたるため未判定のオブジェクティブオブジェクティブが未判定 (長い反例が原因の可能性あり)
テスト生成	達成されたオブジェクティブ達成されたオブジェクティブ - シミュレーションが必要達成されないオブジェクティブ近似において非達成のオブジェクティブテストケースで未判定のオブジェクティブ実行時エラーのため未判定のオブジェクティブゼロ除算のため未判定のオブジェクティブ非線形性のため未判定のオブジェクティブスタブのため未判定のオブジェクティブ未判定のオブジェクティブ配列が範囲外にあたるため未判定のオブジェクティブ
プロパティ証明	有効なオブジェクティブ近似において有効なオブジェクティブ反例によって反証されたオブジェクティブ反証されたオブジェクティブ - シミュレーションが必要反例で未判定のオブジェクティブ実行時エラーのため未判定のオブジェクティブゼロ除算のため未判定のオブジェクティブ非線形性のため未判定のオブジェクティブスタブのため未判定のオブジェクティブ未判定のオブジェクティブ配列が範囲外にあたるため未判定のオブジェクティブ

設計エラー検出オブジェクティブのステータス

設計エラー検出解析を実行すると、[設計エラー検出オブジェクティブのステータス] 節にはオブジェクティブステータスについての次の小節が記載されます。

デッドロジック
近似におけるデッドロジック
アクティブロジック - シミュレーションが必要
有効なオブジェクティブ
近似において有効なオブジェクティブ
反例によって反証されたオブジェクティブ
オブジェクティブのエラー - シミュレーションが必要

設計エラー検出解析で Observer Reference ブロックが使用されている場合、この節では、オブザーバーの情報が [オブザーバーモデル] 小節に、設計モデルの情報が [設計モデル] 小節にそれぞれ表示されます。モデル内にアクティブロジックが存在しない場合、この節は空になります。

[設計モデル] 小節の表は、モデル例 sldvdemo_debounce_validprop のアクティブロジックのリストを示しています。

オブザーバーは設計エラー検出解析で無視されるため、[オブザーバーモデル] 節には、レポートされているアクティブロジックが表示されません。

デッドロジック. [デッドロジック] 節には、解析でデッドロジックが見つかった項目がリストされます。

次のイメージは、sldvdemo_fuelsys_logic_simple モデルで生成された解析レポートの [デッドロジック] 節を示しています。

近似におけるデッドロジック. [近似におけるデッドロジック] 節には、解析で近似の影響を受けるデッドロジックが見つかったモデルの項目がリストされます。

R2017b より前のリリースでは、この節には [デッドロジック] としてマークされているオブジェクティブが含まれる場合があります。

次の図は、生成された解析レポートの [近似におけるデッドロジック] 節を示しています。

アクティブロジック - シミュレーションが必要. [アクティブロジック - シミュレーションが必要] 節には、解析でアクティブロジックが見つかったモデルの項目がリストされます。アクティブロジックのステータスを確認するには、テストケースのシミュレーションを追加で実行しなければなりません。

R2017b より前のリリースでは、この節には [アクティブロジック] としてマークされているオブジェクティブが含まれる場合があります。

次のイメージは、sldvdemo_fuelsys_logic_simple モデルで生成された解析レポートの [アクティブロジック - シミュレーションが必要] 節の一部を示しています。

有効なオブジェクティブ. [有効なオブジェクティブ] 節には、解析で有効であることがわかった設計エラー検出オブジェクティブがリストされます。これらのオブジェクティブについては、解析によって、記述された設計エラーは発生することがないと判断されています。

R2017b より前のリリースでは、この節には [有効であると証明済み] とマークされているオブジェクティブが含まれる場合があります。

次のイメージは、sldvdemo_design_error_detection モデルで生成された解析レポートの [有効なオブジェクティブ] 節を示しています。

近似において有効なオブジェクティブ. [近似において有効なオブジェクティブ] 節には、解析で近似の影響の下で有効であることがわかった設計エラー検出オブジェクティブがリストされます。

R2017b より前のリリースでは、この節には [有効であると証明済み] とマークされているオブジェクティブが含まれる場合があります。

次の図は、生成された解析レポートの [近似において有効なオブジェクティブ] 節を示しています。

反例によって反証されたオブジェクティブ. [反例によって反証されたオブジェクティブ] には、報告されたエラーを確認するために反例がシミュレートされ検証された設計エラー検出オブジェクトのセットがリストされます。

次のイメージは、sldvdemo_design_error_detection モデルで生成された解析レポートの [反例によって反証されたオブジェクティブ] 節を示しています。

オブジェクティブのエラー - シミュレーションが必要. [オブジェクティブのエラー - シミュレーションが必要] 節では、設計エラーを示すテストケースが解析で見つかった設計エラー検出オブジェクティブがリストされます。反証ステータスを確認するには、テストケースのシミュレーションを追加で実行しなければなりません。

R2017b より前のリリースでは、この節には [反証] とマークされているオブジェクティブが含まれる場合があります。

次のイメージは、sldvdemo_array_bounds モデルで生成された解析レポートの [オブジェクティブのエラー - シミュレーションが必要] 節を示しています。

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

テストケース生成解析を実行すると、[テストオブジェクティブのステータス] 節にはオブジェクティブステータスについての次の小節が記載されます。

達成されたオブジェクティブ
達成されたオブジェクティブ - シミュレーションが必要
達成されないオブジェクティブ
近似において非達成のオブジェクティブ
テストケースで未判定のオブジェクティブ

[モデルカバレッジオブジェクティブ] を [拡張 MCDC] に設定してモデルを解析すると、ソフトウェアはモデル項目の検出ステータスをレポートします。詳細については、Simulink Design Verifier の拡張 MCDC カバレッジを参照してください。

テストケース生成解析で Observer Reference ブロックが使用されている場合、各テストオブジェクティブステータス節では、オブザーバーの情報が [オブザーバーモデル] 小節に、設計モデルの情報が [設計モデル] 小節にそれぞれ表示されます。モデル内にテストオブジェクティブが見つからない場合、これらの小節は空になります。

この表は、モデル例 sldvdemo_debounce_testobjblks にある設計モデルの [達成されたオブジェクティブ] のテストオブジェクティブの一部を示しています。

この表は、モデル例 sldvdemo_debounce_testobjblks にあるオブザーバーモデルの [達成されたオブジェクティブ] のテストオブジェクティブの一部を示しています。

達成されたオブジェクティブ. [達成されたオブジェクティブ] 節には、解析で達成されたテストオブジェクティブがリストされます。生成されたテストケースはオブジェクティブをカバーします。

次のイメージは、モデル例 sldvdemo_fuelsys_logic_simple で生成された解析レポートの [達成されたオブジェクティブ] 節の一部を示しています。

達成されたオブジェクティブ - シミュレーションが必要. [達成されたオブジェクティブ - シミュレーションが必要] 節には、解析で達成されたテストオブジェクティブがリストされます。達成ステータスを確認するには、テストケースのシミュレーションを追加で実行しなければなりません。

R2017b より前のリリースでは、この節には [達成] としてマークされているオブジェクティブが含まれる場合があります。

次の図は、生成された解析レポートの [達成されたオブジェクティブ - シミュレーションが必要] 節を示しています。

達成されないオブジェクティブ. [非達成のオブジェクティブ] 節には、解析で達成されないと判断されたテストオブジェクティブがリストされます。

R2017b より前のリリースでは、この節には [非達成と証明] とマークされているオブジェクティブが含まれる場合があります。

次のイメージは、モデル例 sldvdemo_fuelsys_logic_simple で生成された解析レポートの [非達成のオブジェクティブ] 節を示しています。

近似において非達成のオブジェクティブ. [近似において非達成のオブジェクティブ] 節には、解析時の近似により、解析で達成されないと判断されたテストオブジェクティブがリストされます。

R2017b より前のリリースでは、この節には [非達成と証明] とマークされているオブジェクティブが含まれる場合があります。

次の図は、生成された解析レポートの [近似において非達成のオブジェクティブ] 節を示しています。

テストケースで未判定のオブジェクティブ. [テストケースで未判定のオブジェクティブ] 節には、解析時の近似の影響により未判定のテストオブジェクティブがリストされます。

R2017b より前のリリースでは、この節には [達成] としてマークされているオブジェクティブが含まれる場合があります。

次のイメージは、モデル例 sldvApproximationsExample で生成された解析レポートの [テストケースで未判定のオブジェクティブ] 節を示しています。

証明オブジェクティブステータス

プロパティ証明解析を実行すると、[証明オブジェクティブのステータス] 節にはオブジェクティブステータスについての次の小節が記載されます。

有効なオブジェクティブ
近似において有効なオブジェクティブ
反例によって反証されたオブジェクティブ
反証されたオブジェクティブ - シミュレーションが必要
反例で未判定のオブジェクティブ

プロパティ証明解析で Observer Reference ブロックが使用されている場合、各証明オブジェクティブステータス節では、オブザーバーの情報が [オブザーバーモデル] 小節に、設計モデルの情報が [設計モデル] 小節にそれぞれ表示されます。モデル内にオブジェクティブが見つからない場合、これらの小節は空になります。

この表は、モデル例 sldvdemo_debounce_validprop にあるオブザーバーモデルの [有効なオブジェクティブ] の証明オブジェクティブを示しています。

有効なオブジェクティブ. [有効なオブジェクティブ] 節には、解析で有効であることがわかった証明オブジェクティブがリストされます。

R2017b より前のリリースでは、この節には [有効であると証明済み] とマークされているオブジェクティブが含まれる場合があります。

次のイメージは、モデル例 sldvdemo_debounce_validprop で生成された解析レポートの [有効なオブジェクティブ] 節を示しています。

近似において有効なオブジェクティブ. [近似において有効なオブジェクティブ] 節には、解析で近似の影響の下で有効であることがわかった証明オブジェクティブがリストされます。

R2017b より前のリリースでは、この節には [有効と証明されたオブジェクティブ] とマークされているオブジェクティブが含まれる場合があります。

次の図は、生成された解析レポートの [近似において有効なオブジェクティブ] 節を示しています。

反例によって反証されたオブジェクティブ. [反例によって反証されたオブジェクティブ] 節には、解析で反証された証明オブジェクティブがリストされます。生成された反例は、証明オブジェクティブの違反を示します。

次のイメージは、モデル例 sldvdemo_debounce_falseprop で生成された解析レポートの [反例によって反証されたオブジェクティブ] 節を示しています。

反証されたオブジェクティブ - シミュレーションが必要. [反証されたオブジェクティブ - シミュレーションが必要] 節には、解析で反証された証明オブジェクティブがリストされます。反証ステータスを確認するには、反例のシミュレーションを追加で実行しなければなりません。

R2017b より前のリリースでは、この節には [反例によって反証されたオブジェクティブ] とマークされているオブジェクティブが含まれる場合があります。

次の図は、生成された解析レポートの [反証されたオブジェクティブ - シミュレーションが必要] 節を示しています。

反例で未判定のオブジェクティブ. [反例で未判定のオブジェクティブ] 節には、解析時の近似の影響により未判定の証明オブジェクティブがリストされます。

R2017b より前のリリースでは、この節には [反証] とマークされているオブジェクティブが含まれる場合があります。

次の図は、生成された解析レポートの [反例で未判定のオブジェクティブ] 節を示しています。

未判定オブジェクティブのステータス

レポートのこの節には、モデルの解析時におけるすべての未判定オブジェクティブに関する情報が示されます。

実行時エラーのため未判定のオブジェクティブ
ゼロ除算のため未判定のオブジェクティブ
非線形性のため未判定のオブジェクティブ
スタブのため未判定のオブジェクティブ
配列が範囲外にあたるため未判定のオブジェクティブ
未判定のオブジェクティブ
オブジェクティブが未判定 (長い反例が原因の可能性あり)

実行時エラーのため未判定のオブジェクティブ. 証明オブジェクティブおよびテストオブジェクティブについて、[実行時エラーのため未判定のオブジェクティブ] 節には、実行時エラーのため解析時に未判定のオブジェクティブがリストされます。実行時エラーは、テストケースまたは反例のシミュレーション中に発生します。

R2017b より前のリリースでは、この節には [反証] または [達成] とマークされているオブジェクティブが含まれる場合があります。

次の図は、生成された解析レポートの [実行時エラーのため未判定のオブジェクティブ] 節を示しています。

この例では、Simulink® Design Verifier™ がステータス [実行時エラーのため未判定] のオブジェクティブを返した場合に生じるエラーを見つける方法を示します。以前は、Simulink® Design Verifier™ ではエラーの原因の詳細が説明されませんでした。

モデルを開く

オブジェクティブステータス [実行時エラーのため未判定] を返すモデルを開きます。

open_system('mUndecidedDueToRunTimeError');

モデルツールストリップから生成されたコードのテストケースの生成

1.[Design Verifier] タブの [モード] セクションで、[テスト生成] オプションを選択します。

2.[テスト生成] オプションをクリックしてテストを生成します。

3.テストの生成後、オブジェクティブの関連付けられているブロックを選択します。"インフォーマー" ウィンドウに、判定オブジェクティブのリストが、その他のオプションとともに表示されます。

エラーメッセージのチェック

4.インフォーマーウィンドウで [エラーの詳細] オプションをクリックして、実行時エラーにアクセスします。このオプションは、ステータスが [実行時エラーのため未判定] のオブジェクティブに対してのみ有効です。

5.Simulink Design Verifier は実行時エラーのあるブロックを強調表示し、ブロックの隣にエラーメッセージを表示します。

6.レポートを生成して、実行時エラーになるテストケースのエラーメッセージを確認します。

ゼロ除算のため未判定のオブジェクティブ. すべてのタイプのオブジェクティブについて、[ゼロ除算のため未判定のオブジェクティブ] 節には、関連するモデル項目のゼロ除算エラーのため解析時に未判定のオブジェクティブがリストされます。モデルの解析を続ける前にゼロ除算エラーを検出するには、整数オーバーフローおよびゼロ除算エラーの検出の手順に従ってください。

非線形性のため未判定のオブジェクティブ. すべてのタイプのオブジェクティブについて、[非線形性のため未判定のオブジェクティブ] 節には、非線形演算の計算が必要なために解析時に未判定のオブジェクティブがリストされます。Simulink Design Verifier では、非線形演算および非線形ロジックがサポートされていません。

スタブのため未判定のオブジェクティブ. すべてのタイプのオブジェクティブについて、[スタブのため未判定のオブジェクティブ] 節には、スタブのために解析時に未判定のオブジェクティブを含むモデル項目がリストされます。R2013b より前のリリースでは、これらのオブジェクティブには、[達成されたオブジェクティブ – テストケースなし] または [反証されたオブジェクティブ – 反例なし] とマークされているオブジェクティブが含まれる場合があります。

配列が範囲外にあたるため未判定のオブジェクティブ. すべてのタイプのオブジェクティブについて、[配列が範囲外にあたるため未判定のオブジェクティブ] 節には、関連するモデル項目に範囲外の配列エラーがあるため解析時に未判定になったオブジェクティブがリストされます。モデルから範囲外の配列エラーを検出するには、配列の範囲外へのアクセスエラーの検出を参照してください。

未判定のオブジェクティブ. オブジェクティブのすべてのタイプについて、[未判定のオブジェクティブ] の節では、割り当てられた時間内に解析が結果を判定できなかったオブジェクティブがリストされます。

次のプロパティ証明の例では、このソフトウェアが解析時間の制限 ([最大解析時間] パラメーターで指定) を超えているか、これらのオブジェクティブの処理の完了前にユーザーが解析を中断しています。

オブジェクティブが未判定 (長い反例が原因の可能性あり). オーバーフローなど一部の設計エラーは、非常に長いテストケースを使用しないと明らかにならないことがあります。このようなテストケースは、構築やシミュレーションが実行不可能な場合があります。設計エラーチェックの反例が実行不可能なほど長いことを Simulink Design Verifier が検出した場合、ステータス [オブジェクティブが未判定 (長い反例が原因の可能性あり)] を返し、その反例自体を返さずに反例の最小の長さを返すことがあります。

この例のモデルは、uint32 型の変数で boolean 入力が true となった回数をカウントします。整数のオーバーフローが起こる可能性がありますが、ステップ数が uint32 の最大値を超えてからになります。

モデルを開く

モデル "counterexample" を開きます。

open_system('counter');

設計エラー検出解析の実行

1.モデルは、[整数のオーバーフロー] オプションを有効にして事前に構成されています。[Design Verifier] タブで [設計エラーの検出] をクリックします。

2.ソフトウェアは整数オーバーフローエラーについてモデルを解析します。解析が完了すると、Add ブロックの [結果の概要] ウィンドウに、ブロックのステータスが [オブジェクティブが未判定 (長い反例が原因の可能性あり)] として表示されます。

このステータスとともに、反例の最小の長さが、4294967295 シミュレーションステップとしてレポートされます。

解析結果のレビュー

レポートに、新たな節 [オブジェクティブが未判定 (長い反例が原因の可能性あり)] が表示されます。この節には、実行不可能なほど長い反例をもつすべてのオブジェクティブが表示され、シミュレーションステップ数として反例の最小の長さが表示されます。

モデル項目の章

レポートのモデル項目の章には、カバレッジオブジェクティブを定義するモデルの各オブジェクトの表が含まれます。それぞれのオブジェクトの表には、すべての関連付けられたオブジェクティブが、オブジェクティブのタイプ、説明および解析終了時のステータスと共にリストされます。

モデルの個々のオブジェクトの表は、ここにあるような、モデル例 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 であり、これによってオーバーフローエラーが発生しました。

テストケースの章

テスト生成解析を実行すると、レポートには [テストケース] の章が含まれます。この章では、解析で生成されたテストケースを節にまとめて記述しています。

目次
概要
オブジェクティブ
生成された入力データ
期待される出力
Long Test Cases

概要

概要節では以下がリストされます。

テストケースを構成する信号の長さ
テストケースが達成するテストオブジェクティブの合計数

オブジェクティブ

オブジェクティブの節には以下がリストされます。

テストケースがそのオブジェクティブを達成するタイムステップ。
テストケースがそのオブジェクティブを達成する時間。
そのオブジェクティブに関連付けられたモデルの項目へのリンク。リンクをクリックすると、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 節には、反例がプロパティを反証したタイムステップと対応する時間がリストされます。この節には、そのタイムステップでの信号値もリストされます。