Main Content

結果の確認

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 ブロックが強調表示され、新しいウィンドウが開いてブロックの詳細が表示されます。

ブロック置換の概要

ブロック置換の概要には、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 モデルで生成された解析レポートの [オブジェクティブのエラー - シミュレーションが必要] 節を示しています。

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

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

[モデル カバレッジ オブジェクティブ] を [Enhanced 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 では、非線形演算および非線形ロジックがサポートされていません。

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

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

配列が範囲外にあたるため未判定のオブジェクティブ

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

未判定のオブジェクティブ

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

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

モデル項目の章

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

モデルの個々のオブジェクトの表は、ここにあるような、モデル例 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] 、 [結果] ペインで [期待される出力値を含める] を選択すると、レポートにそれぞれのテスト ケースの Expected Output 節が記載されます。この表には、モデルの項目に関連付けられたそれぞれの出力信号について、各タイム ステップで想定される出力値がリストされます。

Long Test Cases

[テスト スイートの最適化] オプションを [LongTestcases] に設定すると、レポートの Test Cases の章にはより長いテスト ケースに関する、より少数の節が記載されます。

プロパティの章

プロパティ証明解析を実行すると、レポートには Properties の章が含まれます。この章では、このソフトウェアが生成した証明オブジェクティブおよび反例を節にまとめて記述しています。

目次

プロパティの章には目次があります。目次の各項目は、反証された個々のプロパティに関する情報へのハイパーリンクになっています。

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

この表は、モデル例 sldvdemo_debounce_validprop にあるオブザーバー モデルのプロパティの 1 つを示しています。

概要

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

  • このソフトウェアが解析したモデルの項目

  • 評価されたプロパティのタイプ

  • 解析のステータス

次の例では、sldvdemo_cruise_control_verification モデルが解析され、プロパティが証明されています。BrakeAssertion という名前の Assertion ブロックへの入力が非ゼロであることが、解析により証明されています。

反例

Counterexample 節には、反例がプロパティを反証したタイム ステップと対応する時間がリストされます。この節には、そのタイム ステップでの信号値もリストされます。