Simulink Design Verifier を使用したモデルプロパティの証明

"プロパティ" とは、Simulink^® または Stateflow^® 内における、あるいは各種 MATLAB Function または Requirements Table ブロックを使用した、モデル化要件の 1 つです。シミュレーション時に特定の値または値の範囲に達しなければならないモデル内の信号など、単純な要件をプロパティとして指定できます。

証明が必要な論理式としてモデル化された多数の入力信号および出力信号を含むモデルの要件もプロパティになる場合があります。

Simulink Design Verifier™ ソフトウェアは、モデルの形式的解析を実行し、指定されたプロパティを証明または反証します。解析が完了したら、結果をレビューするためにいくつかの方法が提示されます。

モデル上での強調表示
テストケースを含むハーネスモデル
詳細な HTML レポート

プロパティ証明を指定する Proof ブロック

Simulink Design Verifier ソフトウェアには、Simulink モデルでプロパティ証明を指定できる 2 つのブロックが用意されています。

Proof ブロック	説明
Proof Objective	証明する信号の値を定義します。
Proof Assumption	証明時に信号の値を制約します。

Simulink ソフトウェアの Model Verification ライブラリのブロックは、Simulink Design Verifier 証明時に Proof Objective ブロックのように動作します。Assertion ブロックや他の Model Verification ブロックを使用して、モデルのプロパティを指定できます。これらのブロックの詳細については、Model Verificationを参照してください。

プロパティ証明を指定する証明関数

Simulink Design Verifier ソフトウェアには、Simulink モデルまたは Stateflow チャートのプロパティ証明を指定する Stateflow および MATLAB^® のコード生成関数が 2 つ用意されています。

証明関数	説明
`sldv.prove`	証明オブジェクティブを指定
`sldv.assume`	証明の前提を指定

これらの関数は、

ブロックパラメーターを使用するより自然にできる形でプロパティの証明の数学的関係を特定します。
モデルを複雑化することなく、複数のオブジェクティブ、前提または条件の指定をサポートします。
MATLAB の機能へのアクセスを提供します。
検証とモデル設計の分離をサポートします。

これらの証明関数の使用方法の例は、sldv.prove のリファレンスページを参照してください。

メモ

Simulink Design Verifier ブロックおよび関数はモデルと共に保存されます。Simulink Design Verifier ライセンスのない MATLAB インストール環境でモデルを開くと、ブロックおよび関数は表示できますが、結果は生成されません。

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

設計モデルのプロパティを証明するには、以下のワークフローを使用します。

要件の仕様などに基づき、設計モデルの検証オブジェクティブを決定します。
設計モデルをインストルメント化して、証明オブジェクティブおよび証明前提を指定します。
- 単純なプロパティの場合、証明オブジェクティブを指定するブロックまたは MATLAB 関数を含むモデルをインストルメント化します。
- システムレベルプロパティの場合、設計モデルを参照する Model ブロックを含む検証モデルを構築し、同じ入力および出力を使用して設計モデルインターフェイスのプロパティを定義します。
Proof Assumption ブロックまたは sldv.assume を使用して解析の制約を定義します。これらの制約は、すべての有効な証明オブジェクティブに適用されます。
メモ
証明前提は、すべての有効な証明オブジェクティブに適用されます。矛盾する前提が指定されていると解析全体が無効になる場合があるので、指定されていないことを確認してください。
Simulink Design Verifier によるモデルのプロパティ証明の制御オプションを指定します。
Simulink Design Verifier 解析を実行して結果をレビューします。

このワークフローの実証演習は、モデルのプロパティの証明を参照してください。