sldv.prove

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

構文

sldv.prove(expr)

説明

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

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

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

例

プロパティ証明オブジェクティブおよび証明の前提の指定

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

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] 、 [サブシステムのプロパティを検証] を選択することもできます。

入力引数

expr — 前提の論理式

論理式

MATLAB 式。たとえば、x > 0。

代替方法

関数 sldv.prove を使用する代わりに、Proof Objective ブロックをモデルに挿入できます。Proof Objective ブロックの代わりに sldv.prove を使用すると、プロパティ証明とはで説明されているとおり、いくつかの利点が得られます。

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

• Simulink ブロックを使用したオブジェクティブの表現。

• 証明の出力の Simulink ブロックへの明示的な接続。

参考

Proof Assumption | Proof Objective | sldv.condition | sldv.prove | sldv.test | Test Condition | Test Objective

トピック

• モデルのプロパティの証明
• モデル プロパティ証明のワークフロー

R2009b で導入