Main Content

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

検証モデルを使用したシステムレベル プロパティの証明

プロパティ証明に検証モデルを使用するタイミング

モデルの動作に影響するシステム全体のプロパティがモデルにある場合、設計モデルを変更しないままでそのプロパティを証明することが必要になる場合があります。そのためには、以下を含む "検証モデル" を作成します。

  • 設計モデルを参照する Model ブロック

  • プロパティおよび必要な制約を定義する 1 つ以上の検証サブシステム

この例について

この設計モデル sldvdemo_sbr_design では、シート ベルトの警告灯のロジックをモデル化しています。エンジンの開始時にシート ベルトが締められていない場合、車が一定の速度を超えると、シート ベルトの警告灯が点灯します。

sldvdemo_sbr_verification モデルは、いくつかの制約を定義し、sldvdemo_sbr_design モデルのプロパティを検証する検証モデルです。検証モデルの Model ブロックは設計モデルを参照し、これにより検証ロジックは検証モデル内にのみ存在します。

制約が無効であるため、sldvdemo_sbr_verification モデルには、反証されているプロパティが含まれます。sldvdemo_sbl_verification_fixed モデルでは、制約が有効であり、すべてのプロパティは有効であることが証明されています。

検証モデルの理解

検証モデルの仕組みを理解するために、次の手順に従います。

  1. 検証モデルを開きます。

    Design Model ブロックは、sldvdemo_sbr_design を参照する Model ブロックです。設計モデル内の SBR Stateflow® チャートは、最初の KEY 入力として 0 を想定しています。

  2. 証明しようとする設計モデルのプロパティを指定する Safety Properties サブシステムを開きます。

    このサブシステムには、MATLAB Property と呼ばれる MATLAB Function ブロックが含まれます。このブロックのコードは、エンジンのスタート時にシート ベルトが締められていず、速度が 15 未満であれば、シート ベルト警告灯が点灯するというプロパティを指定しています。

  3. Safety Properties サブシステムを閉じます。

  4. Input Constraints サブシステムを開きます。

    このサブシステムでは次の制約を定義しています。

    • キーの取り得る位置は 3 つ: 0, 1, 2

    • 速度は 10 ~ 30 に制約される。

    • キーは 0 で開始しなければならず、一度に 1 段階しか変更できない。たとえば、キーは 0 から 1 や 1 から 2 へは変更できますが、0 から 2 へは変更できません。この検証モデルでは、この制約は有効ではありません。

  5. Input Constraints サブシステムを閉じて、sldvdemo_sbr_verification モデルは開いたままにしておきます。

設計モデルのプロパティの証明

sldvdemo_sbr_verification モデルを解析してプロパティを証明します。

  1. sldvdemo_sbr_verification モデル ウィンドウで [実行] ボタンをダブルクリックして解析を開始します。

    解析が完了すると、Simulink® Design Verifier™ のログ ウィンドウに、1 つのオブジェクティブが [反証 - シミュレーションが必要] であることが示されます。詳細については、反証されたオブジェクティブ - シミュレーションが必要を参照してください。

  2. 反証されたオブジェクティブを特定するには、[解析結果をモデル上で強調表示] をクリックします。

    Safety Properties サブシステムがオレンジで強調表示されます。

  3. Safety Properties サブシステムを開き、MATLAB Property ブロックをクリックします。

    Simulink Design Verifier の [結果] ウィンドウにステートメント

    sldv.prove(implies(activeCond,SeatBeltIcon))

    が少なくとも 1 タイム ステップの間 false であったことが示されます。

  4. [反例を表示] をクリックして、このプロパティに違反する信号値を表示します。

    Signal Builder ブロックが開き、反例が表示されます。KEY 入力は最初 2 でしたがこれは無効です。

Safety Properties サブシステムで指定されたプロパティを検証するには、KEY の初期値が 0 であることを確認しなければなりません。

検証モデルの修正

検証モデルの Input Constraints サブシステムには 3 つの制約が含まれていました。3 番目の制約は、KEY の初期値は 0 であり、KEY は 1 段階のみ変更できるというものですが、これは無効になっています。

3 番目の制約が有効な場合にこのプロパティがどのように検証されるかを確認するには、次の手順に従います。

  1. sldvdemo_sbr_verification モデルで [Open Fixed Model] をクリックします。

    sldvdemo_sbr_verification_fixed 検証モデルが開きます。

  2. Input Constraints サブシステムを開きます。

    ここでは 3 番目の制約が有効で、KEY は初期値が 0 で 1 段階ずつ変更されます。

  3. Input Constraints サブシステムを閉じます。

  4. sldvdemo_sbr_verification_fixed モデルで、Run ブロックをダブルクリックして解析を開始します。

    解析によりプロパティの有効性が証明されます。

関連するトピック