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

この例では、検証モデルを使用してシステムレベルプロパティを証明する方法を示します。

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

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

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

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

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

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

open_system('sldvdemo_sbr_verification')

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" ブロックをダブルクリックして解析を開始します。

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

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