Simulink Design Verifier フィルター エクスプローラーを使用したオブジェクティブのフィルター処理

設計エラー検出またはテスト生成解析からのモデル オブジェクトおよびコード式のフィルター処理により、Simulink^® Design Verifier™ 解析のオブジェクトのサブセットに集中できます。解析に長時間かかるモデル オブジェクトがある場合や、解析で固有のオブジェクティブに集中する場合にフィルターを使用します。

[コンフィギュレーション パラメーター] ウィンドウを開き、[Design Verifier] をクリックし、[詳細設定パラメーター] でフィルターを基にオブジェクティブを無視するを選択することで、1 つ以上のフィルター ファイルを追加できます。[フィルター ファイル] パラメーターでフィルター ファイルを入力します。カバレッジ フィルター ファイルの詳細については、カバレッジ フィルターの作成と使用 (Simulink Coverage)を参照してください。コードベースの解析で [Design Verifier] オブジェクティブをフィルターして、コードベースの結果をモベルベースの結果に合わせることもできます。

設計エラー検出またはテスト生成解析を実行してから、Simulink Design Verifier フィルター エクスプローラーを使用して、unsatisfiable、dead logic、undecided、および falsified オブジェクティブを正当化できます。Simulink Design Verifier フィルター エクスプローラーを使用してフィルターを編集する場合、Simulink Design Verifier レポートを更新し、モデルを再度解析せずに解析結果をモデルで強調表示できます。オブジェクティブをフィルター処理する方法の詳細な例については、設計エラー検出のためのオブジェクティブの除外と正当化を参照してください。

Simulink Design Verifier フィルター エクスプローラーを使用したフィルター ファイルの編集

モデルの解析後、Simulink Design Verifier ファイル エクスプローラーを使用して、falsified、unsatisfiable、undecided、および dead logic オブジェクティブを正当化し、フィルター ファイルを更新できます。

[結果の概要] ウィンドウまたは結果インスペクター ウィンドウからフィルター エクスプローラーを開くことができます。

• [結果の概要] ウィンドウで、[フィルター エクスプローラーを開く] をクリックします。

  

• 結果インスペクター ウィンドウで、次のようにします。

  • 正当化済みオブジェクティブのフィルター規則を確認するには、[表示] をクリックします。

  • オブジェクティブを正当化するには、[正当化] をクリックします。

    

Simulink Design Verifier フィルター エクスプローラーでは、以下を行うことができます。

• フィルター ファイルの作成、読み込み、編集、または保存を行う。

• アクティブな sldvData からすべての Unsatisfiable、Falsified、および Dead Logic オブジェクティブを正当化するフィルター ファイルを作成する。

• モデルにアクセスしてフィルター規則に関連付けられているモデル オブジェクトを検査する。

• オブジェクティブまたはモデル オブジェクトあるいはコード式が除外または正当化される理由に関する根拠の説明を追加する。

タスク	アクション
規則に関連付けられているモデル オブジェクトにアクセスする。 メモ この手順はモデル オブジェクティブ解析でのみ有効です。	規則を選択します。 [モデル内に表示] をクリックします。モデル オブジェクトは青で強調表示されます。
規則を削除する。	規則を選択します。 [規則の削除] をクリックします。
現在の規則をファイルに保存する。	[適用] をクリックします。 フィルター ファイルのファイル名とフォルダーを指定して、[保存] をクリックします。
フィルター ファイルの名前を変更する	[名前を付けて保存] をクリックします。 フィルター ファイルのファイル名とフォルダーを指定して、[保存] をクリックします。
既存のフィルター ファイルを読み込む。	[フィルターの読み込み] をクリックします。 フィルター ファイルに移動して、[開く] をクリックします。
モデルを強調表示し、現在のフィルター ファイルを使用して現在の解析レポートを更新する。	行った変更に関して、[適用] または [元に戻す] をクリックします。 モデルは更新されたフィルターの規則に基づいて強調表示されます。 [結果の概要] ウィンドウまたは結果インスペクター ウィンドウで、[HTML] または [PDF] をクリックします。
空のフィルター ファイルを作成する。	[新規フィルター] をクリックします。 .
フィルター エクスプローラーからフィルターを削除する。	[適用済みのフィルター] にある対応するノードを右クリックし、[削除] を選択します。 .
アクティブな sldvData 内のすべての Unsatisfiable、Falsified、および Dead Logic オブジェクティブを正当化するフィルター ファイルを作成する。	[違反とデッド ロジックの正当化規則をアクティブな sldvData から作成] をクリックします。 [名前を付けて保存] をクリックします。 フィルター ファイルのファイル名とフォルダーを指定して、[保存] をクリックします。

制限

Simulink Design Verifier では、プロパティ証明解析に関連付けられたオブジェクティブのフィルター処理はサポートされません。

関連するトピック

• Design Verifier ペイン
• カバレッジ フィルターの規則の作成、編集、表示 (Simulink Coverage)
• 結果の確認