このページの内容は最新ではありません。最新版の英語を参照するには、ここをクリックします。
Design Verifier ペイン
Design Verifier ペインの概要
解析オプションの指定および Simulink® Design Verifier™ 出力の構成を行います。
モード
Simulink Design Verifier の解析モードを指定します。
設定
既定の設定: テスト生成
設計エラー検出
モデルの整数および固定小数点のオーバーフロー エラー、およびゼロ除算エラーを検出します。
テスト生成
モデルのテスト ケースを生成します。
プロパティ証明
モデルのプロパティを証明します。
ヒント
Simulink Design Verifier は、[Design Verifier] タブの [モード] セクションで以下のいずれかの解析オプションを選択したとき、そのオプションの値を指定します。
[設計エラー検出] を選択し、[設計エラーの検出] をクリックします。
[テスト生成] を選択し、[テストの生成] をクリックします。
[プロパティ証明] を選択し、[プロパティの証明] をクリックします。
依存関係
[モード] パラメーターの設定により、[モデルの互換性のチェック] の下のボタンは次のように変化します。
モード:
テスト生成
の場合、ボタン: テストの生成モード:
設計エラー検出
の場合、ボタン: エラーの検出モード:
プロパティ証明
の場合、ボタン: プロパティの証明
コマンド ライン情報
パラメーター: DVMode |
タイプ: 文字配列 |
値: 'TestGeneration' | 'DesignErrorDetection' | 'PropertyProving' |
既定の設定: 'TestGeneration' |
参考
最大解析時間
Simulink Design Verifier がモデルの解析に費やす最大時間を秒単位で指定します。最大解析時間の値は、解析に指定しても構わない値に設定できます。また、解析はいつでも停止できます。
設定
既定の設定: 300
入力された値は、Simulink Design Verifier がモデルの解析に費やす最大秒数を表します。
コマンド ライン情報
パラメーター: DVMaxProcessTime |
タイプ: double |
値: 任意の有効な値 |
既定の設定: 300 |
出力フォルダー
Simulink Design Verifier による出力の書き込み先のパス名を指定します。
設定
既定の設定: sldv_output/$ModelName$
現在のフォルダーの絶対パスまたは相対パスを入力します。
$ModelName$
は、モデル名を表すトークンです。
ヒント
次のパラメーターを使用して、Simulink Design Verifier の出力の名前および場所をカスタマイズできます。
[結果] ペイン:
データ ファイル名
ハーネス モデルのファイル名
[Simulink テスト オプション]、[テスト ファイル名]
[レポート] ペイン:
レポート ファイル名
出力モデルのファイル パス
[ブロック置換] ペイン:
出力モデルのファイル パス
コマンド ライン情報
パラメーター: DVOutputDir |
タイプ: 文字配列 |
値: 任意の有効なパス |
既定の設定: 'sldv_output/$ModelName$' |
参考
接尾辞を追加して出力ファイル名を固有にする
Simulink Design Verifier が数値の接尾辞を追加して出力ファイル名を一意にするかどうかを指定します。
設定
既定の設定: オン
- オン
数字をインクリメントする接尾辞を Simulink Design Verifier 出力ファイル名に追加します。このオプションを選択することで、同名の既存のファイルが上書きされないようにします。
- オフ
接尾辞を Simulink Design Verifier 出力ファイル名に追加しません。この場合、このソフトウェアは同名の既存のファイルを上書きする可能性があります。
コマンド ライン情報
パラメーター: DVMakeOutputFilesUnique |
タイプ: 文字配列 |
値: 'on' | 'off' |
既定の設定: 'on' |
参考
モデルの互換性チェック
チェックを実行してモデルと Simulink Design Verifier の互換性を評価します。詳細は、Simulink Design Verifier のチェックを参照してください。
テストの生成/エラーの検出/プロパティの証明
[モード] パラメーターを設定すると、このボタンは次のように変化します。
モード:
テスト生成
の場合、ボタン: テストの生成詳細については、テスト ケースの生成とはを参照してください。
モード:
設計エラー検出
の場合、ボタン: エラーの検出詳細については、設計エラー検出とはを参照してください。
モード:
プロパティ証明
の場合、ボタン: プロパティの証明詳細については、プロパティ証明とはを参照してください。
モデル表現の再作成
モデル表現を Simulink Design Verifier 解析用に再作成するかどうかを指定します。
設定
既定の設定: 変更が検出された場合
常時
モデル表現を常に再作成します。
変更が検出された場合
モデルの変更が検出されたときにのみ、モデル表現を再作成します。
コマンド ライン情報
パラメーター: DVRebuildModelRepresentation |
タイプ: character array |
値: 'Always' | 'IfChangeIsDetected' |
既定の設定: 'If change is detected' |
参考
未サポートのブロックおよび関数の自動スタブ化
サポートされていないブロックと関数を解析時に無視するかどうかを指定します。
設定
既定の設定: オン
- オン
サポートされないブロックおよび関数を無視して、解析を続行します。
- オフ
Simulink Design Verifier がサポートされないブロックまたは関数を検出した場合、警告を表示し、解析を続行するかどうかを尋ねます。
コマンド ライン情報
パラメーター: DVAutomaticStubbing |
タイプ: 文字配列 |
値: 'on' | 'off' |
既定の設定: 'on' |
参考
解析で S-Function をサポート
Simulink Design Verifier との互換性をもつようにコンパイルされた S-Function のサポートを有効にするかどうかを指定します。
設定
既定の設定: オン
- オン
Simulink Design Verifier との互換性をもつようにコンパイルされた S-Function のサポートを有効にします。
- オフ
Simulink Design Verifier は解析時に自動的に S-Function をスタブします。
コマンド ライン情報
パラメーター: DVSFcnSupport |
タイプ: 文字配列 |
値: 'on' | 'off' |
既定の設定: 'on' |
参考
指定された最小/最大入力値の使用
指定された最小値および最大値を、モデル内のすべての入力信号に対する制約として考慮するテスト ケースを生成するかどうかを指定します。
設定
既定の設定: オン
- オン
指定された最小値および最大値をすべての入力信号への制約として考慮します。
- オフ
指定された最小値および最大値を無視します。
コマンド ライン情報
パラメーター: DVDesignMinMaxConstraints |
タイプ: 文字配列 |
値: 'on' | 'off' |
既定の設定: 'on' |
参考
有理近似のインスタンスを減らすために追加の解析を実行
Simulink Design Verifier が解析時に有理近似の使用を減らそうとするかどうかを指定します。
設定
既定の設定: オン
- オン
Simulink Design Verifier を使用してモデルを解析する際に、Simulink Design Verifier はモデル内での有理近似の使用を減らそうとします。この設定を有効にすると、解析時間が長くなる場合があります。
- オフ
Simulink Design Verifier は解析時に有理近似の使用を減らしません。
コマンド ライン情報
パラメーター: DVReduceRationalApprox |
タイプ: 文字配列 |
値: 'on' | 'off' |
既定の設定: 'on' |
並列計算でテスト ケースまたは反例を検証
並列計算でテスト ケースまたは反例を検証するかどうかを指定します。このオプションには Parallel Computing Toolbox™ のライセンスが必要です。
検証で並列計算を使用する場合
一般に、次の場合に、並列実行で検証時間を削減できます。
シミュレーションに時間がかかる複雑な Simulink モデルがある。
Simulink Design Verifier の解析が最大解析時間を超え、シミュレーションが必要なステータスのオブジェクティブ数になる。詳細については、達成されたオブジェクティブ - シミュレーションが必要および反証されたオブジェクティブ - シミュレーションが必要を参照してください。
テスト生成解析により長いテスト ケースが生成される。これは、[テスト スイートの最適化] を
[LongTestcases]
または既定値を超える [最大テスト ケース ステップ数] 値に設定したことが原因と考えられます。詳細については、テスト生成ペインの概要を参照してください。
検証に並列計算を使用する場合は、次の点を考慮しなければなりません。
並列プールを起動するには時間がかかり、解析時間全体に影響します。解析時間を削減するには、次のようにします。
テスト生成解析を実行する前に、並列プールが既に実行されていることを確認します。既定の設定では、指定した分単位の値にわたりアイドル状態になると、並列プールはシャットダウンします。この設定を変更する場合は、Parallel Computing Toolbox のトピック「並列基本設定の指定」を参照してください。
すべての並列プール ワーカーで Simulink を読み込みます。
次の場合、シミュレーションは順次行われます。
クラスターは
local
ではない。local
クラスターのみを使用するように、並列基本設定を構成します。この設定を変更する場合は、Parallel Computing Toolbox のトピック「並列基本設定の指定」を参照してください。SLDV 解析を起動する前のモデルは
dirty state
である。モデルに
ToFile
ブロックがある。このモデルは内部ハーネスです。
Simulink Test™ マネージャーからの機能テストとカバレッジ解析などの製品間の機能では、検証の並列計算をサポートしていません。詳細については、機能テストの実行とテスト カバレッジの解析 (Simulink Test)を参照してください。
設定
既定の設定: オフ
- オン
Parallel Computing Toolbox ライセンスがある場合、Simulink Design Verifier は同じマシンの複数のワーカーにわたって、テスト ケースまたは反例を並列で検証します。
- オフ
Simulink Design Verifier はテスト ケースまたは反例を逐次検証します。
コマンド ライン情報
パラメーター: DVUseParallel |
タイプ: 文字配列 |
値: 'on' | 'off' |
既定の設定: 'off' |
参考
コード解析の追加オプション
Simulink Design Verifier との互換性をもつようにコンパイルされた S-Function を解析するための追加オプションを指定します。詳細については、S-Function および C/C++ コードのサポートの制限事項と考慮事項を参照してください。
設定
既定の設定: ''
Simulink Design Verifier との互換性をもつようにコンパイルされた S-Function を解析するための追加オプションを入力します。たとえば、配列の最大サイズを指定するには、「defaultArraySize = 512
」と入力します。
コマンド ライン情報
パラメーター: DVCodeAnalysisExtraOptions |
タイプ: 文字配列 |
値: S-Function の解析に有効な任意のオプション |
既定の設定: '' |
フィルターを基にオブジェクティブを無視する
[フィルター ファイル] のオブジェクティブを無視して、モデルを解析することを指定します。[フィルター ファイル] には、解析から除外するテスト生成用のモデル カバレッジ オブジェクティブ、デッド ロジック検出オブジェクティブ、および設計エラー検出オブジェクティブが含まれます。
設定
既定の設定: オフ
- オン
テスト生成および設計エラー検出解析中に、[フィルター ファイル] に含まれるオブジェクティブを無視します。
- オフ
[フィルター ファイル] に含まれるものも含め、テスト生成および設計エラー検出解析時にすべてのオブジェクティブについて結果を生成します。
依存関係
このパラメーターは [フィルター ファイル] を有効にします。
コマンド ライン情報
パラメーター: DVCovFilter |
タイプ: 文字配列 |
値: 'on' | 'off' |
既定の設定: 'off' |
参考
カバレッジのフィルター (Simulink Coverage)
フィルター ファイル
解析から除外するモデル カバレッジ オブジェクティブおよび設計エラー検出オブジェクティブを含むファイルのフォルダー名とファイル名を指定します。
設定
既定の設定: ''
テスト生成および設計エラー検出解析で無視するオブジェクティブを含むフォルダー名とファイル名を指定します。
[フィルター エクスプローラー] ボタンをクリックして、既存の [フィルター ファイル] を読み込むか新しいファイルを作成します。
コマンド ライン情報
パラメーター: DVCovFilterFileName |
タイプ: 文字配列 |
値: コンマまたはセミコロンで区切った有効なファイル パス |
既定の設定: '' |
参考
カバレッジ フィルターの規則とファイル (Simulink Coverage)
フィルター エクスプローラー
[フィルター エクスプローラー] をクリックして、設計エラー検出およびテスト生成解析で無視するオブジェクティブを含むファイルを読み込みます。
依存関係
このボタンは、[フィルターを基にオブジェクティブを無視する] によって有効になります。