Main Content

Proof Objective

モデルのプロパティを証明する場合に信号で達成されなければならないオブジェクティブを定義する

このページをすべて展開する
  • Proof Objective block

ライブラリ:
Simulink Design Verifier / Objectives and Constraints

説明

プロパティ証明モードで動作する場合、Simulink® Design Verifier™ ソフトウェアは、モデルのプロパティが指定された基準を満たしていることを証明します (プロパティ証明とはを参照)。このモードでは、Proof Objective ブロックを使って、モデル内の信号の証明オブジェクティブを定義できます。

[値] パラメーターでは、ブロックの入力信号の許容値を指定できます。任意のタイム ステップで信号値が許容値から逸脱している場合、プロパティ違反が発生し、証明オブジェクティブが反証されます。このブロックは、指定された [値] パラメーターを入力信号に適用します。Simulink Design Verifier ソフトウェアは、モデルのプロパティが指定された基準を満たしていることを証明または反証します。

このブロックのパラメーター ダイアログ ボックスでは、以下の操作も実行できます。

  • オブジェクティブを有効または無効にします。

  • Simulink エディターで、ブロックの [値] パラメーターを表示するように指定します。

  • ブロックの出力端子を表示するように指定します。

メモ

Simulink と Simulink Coder™ ソフトウェアは、それぞれモデルのシミュレーション時とコード生成時に、Proof Objective ブロックを無視します。Simulink Design Verifier ソフトウェアは、モデル プロパティの証明時にだけ Proof Objective ブロックを使用します。

Proof Objective の指定

[値] パラメーターを使って、証明シミュレーション時に信号が達成されるべき値を定義します。MATLAB® の cell 配列形式で、スカラー値と間隔の組み合わせを指定します。cell 配列の詳細については、cell 配列を参照してください。

ヒント

[値] パラメーターが 1 つのスカラー値だけを指定する場合は、MATLAB の cell 配列形式で入力する必要はありません。

各スカラー値は、配列内の単一のセルを構成します。次に例を示します。

{0, 5}

閉区間は、配列内のセルとして 2 要素ベクトルを構成します。この場合、各要素は間隔のエンドポイントを指定します。

{[1, 2]}

あるいは、引数として単一値を受け入れる Sldv.Point コンストラクターを使用してスカラー値を指定することもできます。Sldv.Interval コンストラクターを使用して間隔を指定できます。2 つの引数 (間隔の上限と下限) が必要です。オプションで、間隔の端点を含めるか排除するかを指定する 3 番目の入力引数として次のいずれかの値を指定できます。

  • '()' — 開区間を定義します。

  • '[]' — 閉区間を定義します。

  • '(]' — 左開右閉区間を定義します。

  • '[)' — 左閉右開区間を定義します。

メモ

既定では、3 番目の引数を省略すると、Sldv.Interval は間隔を閉じているとみなします。

たとえば、[値] パラメーター

{0, [1, 3]}

は、次のように指定します。

  • 0 — スカラー値

  • [1, 3] — 閉区間

[値] パラメーター

{Sldv.Interval(0, 1, '[)'), Sldv.Point(1)}

は、次のように指定します。

  • Sldv.Interval(0, 1, '[)') — 左閉右開区間 [0, 1)

  • Sldv.Point(1) — スカラー値

Proof Objective ブロックに対して複数のスカラー値と間隔を指定した場合、Simulink Design Verifier ソフトウェアはプロパティ証明中に論理 OR 演算子を使って、これらの値を組み合わせます。この場合、単一のスカラー値または間隔が満たされると、証明オブジェクティブ全体が達成されたとソフトウェアは認識します。

端子

入力

すべて展開する

Proof Objective ブロックは、Simulink ソフトウェアがサポートするすべての組み込みデータ型の信号を受け入れます。Simulink ソフトウェアがサポートするデータ型の詳細は、Simulink でサポートされているデータ型を参照してください。このブロックは、複素数入力信号をサポートしていません。

データ型: single | double | int8 | int16 | int32 | int64 | uint8 | uint16 | uint32 | uint64 | Boolean | fixed point | enumerated | bus

パラメーター

すべて展開する

このブロックが有効かどうかを指定します。選択すると (既定の設定)、Simulink Design Verifier ソフトウェアはモデルのプロパティの証明時にこのブロックを使用します。このオプションをオフにすると、ブロックが無効になります。すなわち、Simulink Design Verifier ソフトウェアは Proof Objective ブロックが存在しないかのように動作します。選択されていない場合は、Simulink エディターでこのブロックがグレー表示になります。

証明オブジェクティブを指定します (Proof Objective の指定を参照)。

Simulink エディターで、ブロックが [値] パラメーターの内容を表示するかどうかを指定します。既定ではこのオプションが選択されています。

Simulink エディターで、ブロックが出力端子を表示するかどうかを指定します。このチェック ボックスを選択すると (既定の設定)、ブロックは出力端子を表示し、入力信号をブロックの出力としてパス スルーすることができます。選択されていない場合は、ブロックは出力端子を非表示にして、入力信号を終了します。次の図は、各ケースのブロックの外観を示しています。

[パス スルー スタイル]: 選択した場合

[パス スルー スタイル]: 選択しない場合

[値] パラメーターで指定したプロパティに違反する信号がシミュレーションで発生した場合に、シミュレーションを停止するかどうかを指定します。

このパラメーターを選択してモデルをシミュレートした場合は、指定したプロパティに違反が発生するとシミュレーションが停止します。

拡張機能

バージョン履歴

R2007a で導入

参考

|