Main Content

このページの翻訳は最新ではありません。ここをクリックして、英語の最新版を参照してください。

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

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

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

[最大違反ステップ数] オプションで指定されたシミュレーション ステップ数内でプロパティ違反を検索してから、違反の検出に失敗したプロパティの証明を試行します。この手法は、[Prove][FindViolation] の手法を組み合わせたものです。

依存関係

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

コマンド ライン情報

パラメーター: DVProvingStrategy
タイプ: 文字配列
値: 'Prove' | 'FindViolation' | 'ProveWithViolationDetection'
既定の設定: 'Prove'

参考

最大違反ステップ数

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

設定

既定の設定: 20

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

依存関係

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

コマンド ライン情報

パラメーター: DVMaxViolationSteps
タイプ: int32
値: 任意の有効な値
既定の設定: 20

参考