Design Verifier ペイン: プロパティ証明

プロパティ証明ペインの概要
Assertion ブロック
証明の前提
手法
最大違反ステップ数

プロパティ証明ペインの概要

Simulink^® Design Verifier™ による解析モデルのプロパティ証明方法を制御するオプションを指定します。

参考

Assertion ブロック

モデル内の Assertion ブロックを有効にするか無効にするかを指定します。

設定

既定の設定: ローカル設定を使用

ローカル設定を使用: 各ブロックの [有効] パラメーターの値に基づいて、Assertion ブロックを有効または無効にします。ブロックの [有効] パラメーターが選択されている場合、そのブロックは有効になります。そうでない場合、ブロックは無効になります。
すべて有効: モデル内のすべての Assertion ブロックを [有効] パラメーターの設定にかかわらず有効にします。
すべて無効: モデル内のすべての Assertion ブロックを [有効] パラメーターの設定にかかわらず無効にします。

コマンドライン情報

パラメーター: DVAssertions

タイプ: 文字配列

値: 'UseLocalSettings' | 'EnableAll' | 'DisableAll'

既定の設定: 'UseLocalSettings'

参考

証明の前提

モデル内の Proof Assumption ブロックを有効にするか無効にするかを指定します。

設定

既定の設定: ローカル設定を使用

ローカル設定を使用: 各ブロックの [有効] パラメーターの値に基づいて、Proof Assumption ブロックを有効または無効にします。ブロックの [有効] パラメーターが選択されている場合、そのブロックは有効になります。そうでない場合、ブロックは無効になります。
すべて有効: モデル内のすべての Proof Assumption ブロックを [有効] パラメーターの設定にかかわらず有効にします。
すべて無効: モデル内のすべての Proof Assumption ブロックを [有効] パラメーターの設定にかかわらず無効にします。

コマンドライン情報

パラメーター: DVProofAssumptions

タイプ: 文字配列

値: 'UseLocalSettings' | 'EnableAll' | 'DisableAll'

既定の設定: 'UseLocalSettings'

参考

手法

プロパティの証明時に Simulink Design Verifier が使用する手法を指定します。

設定

既定の設定: Prove

Prove: プロパティ証明を実行します。
FindViolation: [最大違反ステップ数] オプションで指定されたシミュレーションステップ数内でプロパティ違反のみを検索します。
ProveWithViolationDetection: プロパティ違反の検索と、違反の検出に失敗したプロパティ証明の試行の両方を行います。この手法は、[ProveWithViolationDetection] 手法と [FindViolation] 手法間の相対的な最適バランスです。

依存関係

[FindViolation] または [ProveWithViolationDetection] を選択すると [最大違反ステップ数] パラメーターが有効になります。

コマンドライン情報

パラメーター: DVProvingStrategy

タイプ: 文字配列

値: 'Prove' | 'FindViolation' | 'ProveWithViolationDetection'

既定の設定: 'Prove'

参考

最大違反ステップ数

Simulink Design Verifier がプロパティ違反を検索する際のシミュレーションステップの最大数を指定します。

設定

既定の設定: 20

Simulink Design Verifier ソフトウェアは指定されたシミュレーションステップの最大数を超えて検索しません。そのため、シミュレーションの後半で発生する可能性のある違反は特定できません。

依存関係

このパラメーターは、[手法] を [FindViolation] または [ProveWithViolationDetection] に設定したときに有効になります。

コマンドライン情報

パラメーター: DVMaxViolationSteps

タイプ: int32

値: 任意の有効な値

既定の設定: 20