Main Content

単純なモデルの解析

この単純なモデルには 2 つの Logical Operator ブロックと 1 つの Memory ブロックが含まれています。このモデルの永続的な情報は、Memory ブロックのブール値に制限されます。モデルの入力は単一の論理値です。次の表では、任意の長い入力列から導き出される動作を含め、モデルの完全な動作を説明します。

#入力メモリ値XOR ブロックの出力 = 次のメモリ値AND ブロックの出力
1falsefalsefalsefalse
2truefalsetruefalse
3falsetruetruefalse
4truetruefalsetrue

テスト オブジェクティブは、出力が 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 になるパスのみを検索したりするように指定できます。

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

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