モデルの準備と解析

この例では、Signal Editor の Inputs ブロックを使用してテスト ハーネス モデルをシミュレートすることにより、モデル カバレッジ レポートを生成する方法を説明します。Signal Editor ダイアログ ボックスでアクティブなシナリオを選択することにより、単一のテスト ケースまたは反例をシミュレートできます。詳細については、Signal Editor の Inputs ブロックを使用したハーネス モデルのシミュレートを参照してください。

この例では、入力値の制約方法を示します。Test Condition ブロックは、入力値を 0 または 1 にします。

この例では、2 つのカスタムの Test Objective ブロックの使用について示します。ブロック "True" は出力信号を 2 にします。"Masked Objective" 内のブロック "Edge" は 2 から 1 への出力信号の変換を指定します。

Observer Reference ブロックを使用してテスト ケースを生成する。

この例では、パラメーター コンフィギュレーション ファイルを使用して Simulink® Design Verifier™ の解析用にパラメーターを調整する方法を説明します。モデルには、アクティブなコントローラーを有効にして、その出力をモデル出力として選択するパラメーター control_mode が含まれます。Simulink Design Verifier はこのパラメーターを 1 または 2 に制約される入力として処理し、各テスト ケースに適切な値を生成します。

この例では、Simulink® Design Verifier™ の Temporal Operator ブロックを使用して時相システム要件をモデル化し、プロパティ証明およびテスト ケースの生成を行う方法を説明します。

この例では、Simulink® Design Verifier™ の Temporal Operator ブロックを使用してパワー ウィンドウ コントローラー モデルの時相システム要件をモデル化し、プロパティ証明とテスト ケースの生成を行う方法を説明します。