Main Content

モデルにおける結果の強調表示

モデルの強調表示による結果のレビュー

Simulink® Design Verifier™ を使用してモデルを解析すると、解析されたモデル オブジェクトは次のいずれかの色で自動的に強調表示されます。

  • グリーン

  • レッド

  • オレンジ

  • グレー

Simulink エディターで強調表示されているオブジェクトを見ることで一目で解析結果をレビューできます。

Simulink Design Verifier 結果インスペクター

モデルが強調表示されている場合、解析で結果が記録されたオブジェクトをクリックすることができます。そうすると、Simulink Design Verifier 結果インスペクターには、そのオブジェクトの詳細な解析結果が表示されます。

モデル上の結果の自動強調表示

解析時に、オブジェクティブ ステータスが更新されると、Simulink Design Verifier はモデル オブジェクトを自動的に強調表示します。既定では、自動強調表示は有効になっています。強調表示を無効にするには、[結果の概要] ウィンドウで [強調表示の無効化] をクリックします。

Simulink エディターでモデル上の結果が強調表示されます。強調表示が有効なときは、結果インスペクターが開いて、解析オブジェクティブのステータスの概要が表示されます。

メモ

Simulink Design Verifier では、Stateflow® の状態遷移表は強調表示されません。Simulink Design Verifier のレポート、データ ファイルおよびログ ファイルには、状態遷移表の解析データが含まれます。レポートを使用すると、状態遷移表に移動できます。

モデル上のグリーンの強調表示

グリーンに強調表示されているオブジェクトは、それぞれの解析タイプで次を意味します。

解析モードグリーンの強調表示

設計エラー検出

  • オーバーフローまたはゼロ除算エラーが見つからなかった。

  • デッド ロジックが見つからなかった。

  • ユーザー指定の最小および最大制約の範囲外の中間信号または出力信号が見つからなかった。

  • 配列の範囲外へのアクセス エラーが見つからなかった。

テスト生成

テスト オブジェクティブを達成させるテスト ケースが見つからなかった。

プロパティ証明

証明オブジェクティブがすべて有効と判定された。

モデル上のレッドの強調表示

レッドに強調表示されているオブジェクトは、それぞれの解析タイプで次を意味します。

解析モードレッドの強調表示

設計エラー検出

  • オーバーフローまたはゼロ除算エラーが発生するテスト ケースが 1 つ以上見つかった。

  • デッド ロジックが見つかった。

  • ユーザー指定の最小および最大制約の範囲外の中間信号または出力信号が見つかった。

  • 配列の範囲外へのアクセス エラーが発生するテスト ケースが 1 つ以上見つかった。

テスト生成

達成されないテスト オブジェクティブがあった。

プロパティ証明

証明オブジェクティブが反証され、そのオブジェクティブが反証された反例が生成された。

レッドで強調表示されたオブジェクトがモデルに 1 つ以上含まれている場合、モデルには Simulink Design Verifier がレッドで強調表示していない他の設計エラーが含まれている可能性があります。設計内のオブジェクトが原因でランタイム エラーとなっている場合、Simulink Design Verifier は、その下流のオブジェクトにさらにエラーがあるか、またはそれらのエラーがランタイム エラーの原因となるオブジェクトの結果に依存しているかを特定できない場合があります。最初にレッドで強調表示される原因となったエラーを解決し、解析を再実行して、Simulink Design Verifier によってモデル内の他のオブジェクトがレッドで強調表示されていないか確認してください。

モデル上のオレンジの強調表示

オレンジに強調表示されているオブジェクトは、それぞれの解析タイプについて次を意味します。

解析モードオレンジの強調表示

設計エラー検出

強調表示されたモデル オブジェクトについて、

  • 少なくとも 1 つの設計エラー検出オブジェクティブが判定されなかった。この状況は次の場合に発生します。

    • 解析がまだ進行中である。

    • 解析がタイムアウトした。

    • ゼロ除算または非線形演算が原因で、解析で設計エラー検出オブジェクティブを判定できない。

    • スタブが原因で、ソフトウェアが設計エラー検出オブジェクティブを判定できない。詳細は、自動スタブによる非互換性処理を参照してください。

    • 解析エンジンの制限により、ソフトウェアが設計エラー検出オブジェクティブを判定できない。たとえば、上下限のない while ループがあった場合、解析では近似が行われます。詳細については、Role of Approximations During Model Analysisを参照してください。

テスト生成

強調表示されたモデル オブジェクトについて、

  • 少なくとも 1 つのテスト オブジェクティブが判定されなかった。この状況は次の場合に発生します。

    • 解析がまだ進行中である。

    • 解析がタイムアウトした。

    • ゼロ除算または非線形演算が原因で、解析でテスト オブジェクティブを判定できない。

    • スタブが原因で、ソフトウェアがテスト オブジェクティブを判定できない。詳細は、自動スタブによる非互換性処理を参照してください。

    • 解析エンジンの制限により、ソフトウェアがテスト オブジェクティブを判定できない。たとえば、上下限のない while ループがあった場合、解析では近似が行われます。詳細については、Role of Approximations During Model Analysisを参照してください。

プロパティ証明

強調表示されたモデル オブジェクトについて、

  • 少なくとも 1 つの証明オブジェクティブが判定されなかった。この状況は次の場合に発生します。

    • 解析がまだ進行中である。

    • 解析がタイムアウトした。

    • 証明オブジェクティブが、このソフトウェアが制御できない値をもつ信号に存在する。たとえば、Constant ブロックなど。

    • ゼロ除算または非線形演算が原因で、解析で証明オブジェクティブを判定できない。

    • スタブが原因で、ソフトウェアが証明オブジェクティブを判定できない。詳細は、自動スタブによる非互換性処理を参照してください。

    • 解析エンジンの制限により、ソフトウェアが証明オブジェクティブを判定できない。たとえば、上下限のない while ループがあった場合、解析では近似が行われます。詳細については、Role of Approximations During Model Analysisを参照してください。

モデル上のグレーの強調表示

グレーに強調表示されているオブジェクトは次を意味します。

解析モードグレーの強調表示
  • 設計エラー検出

  • テスト生成

  • プロパティ証明

モデル オブジェクトが解析に含まれていなかった。