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

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

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