Main Content

このページの内容は最新ではありません。最新版の英語を参照するには、ここをクリックします。

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');

approximations_example.png

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

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

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

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

approximations_test_generation_results.png

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

approximations_test_generation_results1.png

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

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

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

approximations_prove_properties_results.png

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

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

関連するトピック