モデル プロパティ証明のワークフロー
設計モデルのプロパティを証明するには、以下のワークフローを使用します。
要件の仕様などに基づき、設計モデルの検証オブジェクティブを決定します。
設計モデルをインストルメント化して、証明オブジェクティブおよび証明前提を指定します。
単純なプロパティの場合、証明オブジェクティブを指定するブロックまたは MATLAB® 関数を含むモデルをインストルメント化します。
システムレベル プロパティの場合、設計モデルを参照する Model ブロックを含む検証モデルを構築し、同じ入力および出力を使用して設計モデル インターフェイスのプロパティを定義します。
Proof Assumption ブロックまたは
sldv.assume
を使用して解析の制約を定義します。これらの制約は、すべての有効な証明オブジェクティブに適用されます。メモ
証明前提は、すべての有効な証明オブジェクティブに適用されます。矛盾する前提が指定されていると解析全体が無効になる場合があるので、指定されていないことを確認してください。
Simulink® Design Verifier™ によるモデルのプロパティ証明の制御オプションを指定します。
Simulink Design Verifier 解析を実行して結果をレビューします。
このワークフローの実証演習は、モデルのプロパティの証明を参照してください。