sldv.prove

Stateflow チャートおよび MATLAB Function ブロックの証明オブジェクティブ関数

構文

sldv.prove(expr)

sldv.prove(expr) は、プロパティの証明時に expr がすべての評価に対して真であることを指定します。expr には有効な論理式を使用します。

この関数はなにも出力しないため、expr を評価する間接的な副作用があるだけで、親関数には影響を与えません。MATLAB^® コマンドラインからこの関数を実行しても、効果はありません。

コード内に sldv.prove の証明の前提を組み入れるか、前提を分離して検証スクリプトに組み入れます。

MATLAB Function ブロックを使用して、モデル sldvdemo_sbr_verification のプロパティ証明オブジェクティブおよび証明の前提を指定します。

以下のコマンドは、sldvdemo_sbr_verification モデルがアタッチされている例を開きます。モデルを開きます。

openExample('sldv/SldvexCCallerBlockExample')

sldvdemo_sbr_verification を ex_sldvdemo_sbr_verification として保存します。

Safety Properties サブシステムを開きます。

MATLAB Function ブロックである MATLAB Property ブロックを開きます。

関数 check_reminder の定義の最後に sldv.assume(Inputs.KEY==0 | 1); を追加します。この関数定義の最後の 2 行は次のようになります。

sldv.prove(implies(activeCond, SeatBeltIcon));
sldv.assume(Inputs.KEY==0 | 1);

モデルを保存し、最上位モデルに戻ります。

安全性のプロパティを証明するには、Simulink^® エディターで Safety Properties サブシステムを選択します。[Design Verifier] タブで、[プロパティの証明] をクリックします。

または、Simulink エディターで Safety Properties サブシステムを右クリックし、[Design Verifier] 、 [サブシステムのプロパティを検証] を選択することもできます。

前提の式。論理式として指定します。たとえば、x > 0 です。

関数 sldv.prove を使用する代わりに、Proof Objective ブロックをモデルに挿入できます。Proof Objective ブロックと sldv.prove の違いの詳細については、プロパティ証明とはを参照してください。

関数 sldv.prove を使用せずに、MATLAB をコード生成に使用して証明オブジェクティブを指定することもできます。コードの生成に MATLAB を直接使用するのではなく、sldv.prove を使用すると、次の処理が不要になります。

R2009b で導入