Simulink Design Verifier の解析モードの確認

2 つの Logical Operator ブロックと 1 つの Memory ブロックが含まれている単純なモデルについて考えます。このモデルの永続的な情報は、Memory ブロックのブール値に制限されます。モデルの入力は単一の論理値です。

A simple model with two Logical Operator blocks and a Memory block. in represents input and out represents output.

次の表では、任意の長い入力列から導き出される動作を含め、モデルの完全な動作を説明します。

#	入力	メモリ値	XOR ブロックの出力 = 次のメモリ値	AND ブロックの出力
1	`false`	`false`	`false`	`false`
2	`true`	`false`	`true`	`false`
3	`false`	`true`	`true`	`false`
4	`true`	`true`	`false`	`true`

テストケース生成解析

テストオブジェクティブは、出力が true となるテストケースを生成することです。出力が true になるのは、入力が true であり、Memory ブロックの出力が true である場合です。テストケースの生成はパスに従ってこの条件に達しますが、これは最初のモデル条件によって異なります。

最初のメモリ値が true の場合、テストケースは入力が true の 1 タイムステップです。
最初のメモリ値が false の場合、テストケースは次の 2 タイムステップになります。
1. 入力値が true でメモリ値が false (2 行目)。したがって、XOR ブロックの出力は true になり、メモリ値も true になります。
2. この時点で、入力値とメモリ値はともに true (4 行目) になっているので、出力は true になり、解析はテストオブジェクティブを達成します。

無数のテストケースで出力が true になる可能性があり、また、状態値に関係なく、true になるまで任意の時間において出力が false のままの可能性があります。Simulink^® Design Verifier™ で検索が実行されると、オブジェクティブを達成させる最初に見つかったテストケースが返されます。このケースが常に最小のタイムステップのシミュレーションとなります。ただし、この結果は、非現実的であったり、他のテスト要件を満たさなかったりするために望ましくない場合もあります。

この例と同様の基本原則が、プロパティ証明およびテストケース生成に当てはまります。テストケース生成時には、オプションパラメーターにより検索条件が明示的に指定されます。たとえば、Simulink Design Verifier ですべてのブロック出力のパスを検索したり、ブロック出力が true になるパスのみを検索したりするように指定できます。

設計エラー検出解析

エラー検出解析時には、Simulink Design Verifier はデータのオーバーフローまたはゼロ除算エラーの発生があり得るオブジェクティブかどうかを特定します。解析により、どのようにエラーが発生し得るかを示すテストケースが作成されます。

プロパティ証明解析

プロパティ証明解析時は、出力が常に true など、Simulink Design Verifier で証明する機能要件、つまりプロパティを指定します。このプロパティに違反するパスが見つかることなく検索が完了すると、プロパティは証明されたことになります。出力が false となるパスが見つかると、出力が false となる反例が作成されます。