Simulink Design Verifier が検証結果を使用して近似をレポートする方法

Simulink^® Design Verifier™ は解析時に近似を実行します。近似の存在を識別し、Simulink Design Verifier HTML レポートのオブジェクティブのステータスの章にある各オブジェクティブステータスのレベルで近似をレポートします。詳細については、Role of Approximations During Model Analysisおよびオブジェクティブのステータスの章を参照してください。

シミュレーション時にテストケースまたは反例を検証するために、モデルは高速リスタートモードでロックされます。詳細については、高速リスタートの方法論を参照してください。

たとえば、近似の効果を確実にするため、テスト生成解析では、解析時にテストケースがカバレッジデータに対して検証されます。

オブジェクティブステータスへの近似の影響

解析時に近似による影響を受けるオブジェクティブに対して、テストケースまたは反例が提供されます。これらのオブジェクティブは、テスト生成解析の場合はテストケースで未判定のオブジェクティブとして、プロパティ証明解析の場合は反例で未判定のオブジェクティブとしてレポートされます。

近似による影響を受ける可能性のあるオブジェクティブが、デッドロジック、有効、非達成のいずれかとして確認されます。次の表は、すべての解析モードに関してこれらのオブジェクティブをまとめたものです。

解析モード	オブジェクティブのステータス
設計エラー検出	近似におけるデッドロジック近似において有効なオブジェクティブ
テスト生成	近似において非達成のオブジェクティブ
プロパティ証明	近似において有効なオブジェクティブ

解析モード

オブジェクティブのステータス

設計エラー検出

テスト生成

近似において非達成のオブジェクティブ

プロパティ証明

近似において有効なオブジェクティブ

以下のケースでは、検証結果によってオブジェクティブのステータスを確認することはできません。

オブジェクティブがブロック置換によって導入されている場合。詳細については、ブロック置換とはを参照してください。
Verification Subsystemが関数sldv.testまたはsldv.proveで構成されている場合。
[Simulink Design Verifier の結果の概要] ウィンドウの [停止] ボタンを使用して解析を中止した場合、またはソフトウェアの最大解析時間を超過した場合。これらの場合、一部のオブジェクティブが解析時に検証されないままになり、オブジェクティブのステータスは確認できません。
オブジェクティブをもつブロックが Simulink テストハーネス内に存在するが、テスト対象のコンポーネント外である場合。詳細については、テストハーネスとモデルの関係 (Simulink Test)を参照してください。

次の表は、前述のケースのオブジェクティブのステータスをまとめたものです。オブジェクティブのステータスを確認するには、テストケースまたは反例のシミュレーションを追加で実行しなければなりません。

解析モード	オブジェクティブのステータス
設計エラー検出	アクティブロジック - シミュレーションが必要オブジェクティブのエラー - シミュレーションが必要
テスト生成	達成されたオブジェクティブ - シミュレーションが必要
プロパティ証明	反証されたオブジェクティブ - シミュレーションが必要

検証結果による近似の効果の特定

ライブスクリプトを開く

この例では、Switch ブロックのオブジェクティブステータスに対して近似がどのように影響するかを示します。sldvApproximationsExample モデルでは、Constant ブロックで 1./3 および 2./3 を計算すると、解析時にFloating-Point to Rational Number Conversionが行われます。

入力端子 In2 が -1 に等しい場合、Switch ブロックの入力 2 は、シミュレーション中に 0 に等しくはなりません。したがって、Switch は入力端子 In3 を出力として選択しません。テスト生成解析とプロパティ証明解析の場合、解析時の近似の影響により、Switch ブロックのオブジェクティブ logical trigger input false(output is from 3rd input port) は未判定になります。

1.sldvApproximationsExample: モデルを開きます。

open_system('sldvApproximationsExample');

2.テスト生成解析を実行するには、[Design Verifier] タブで [テストの生成] をクリックします。モデルがシミュレートされ、カバレッジデータに対してテスト結果が検証されます。

3.詳細な解析レポートを表示するには、[Simulink® Design Verifier™ の結果の概要] ウィンドウで [HTML] をクリックします。

次の図は、生成される解析レポートのテストオブジェクティブのステータスセクションを示しています。近似の影響を受けるテストケースが 2 つ示されています。

テストオブジェクティブのステータス - 達成されたオブジェクティブ

テストオブジェクティブのステータス - テストケースで未判定のオブジェクティブ

4.プロパティ証明解析を実行するには、[Design Verifier] タブの [モード] セクションで、[プロパティ証明] を選択します。[プロパティの証明] をクリックします。

次の図は、生成される解析レポートの証明オブジェクティブステータスのセクションを示しています。

証明オブジェクティブステータス - 反例で未判定のオブジェクティブ

近似の影響を受ける反例が 1 つ示されています。

メモ: sldvApproximationsExample のモデル例ではあらかじめ、有理近似のインスタンスを減らすために追加の解析を実行オプションが Off に設定されています。このオプションを有効にして解析を実行する場合、Undecided with Testcases テストオブジェクティブは Unsatisfiable としてレポートされ、証明オブジェクティブは Valid. としてレポートされます。