プロパティ証明とは
"プロパティ" とは、Simulink® または Stateflow® 内における、あるいは各種 MATLAB Function または Requirements Table ブロックを使用した、モデル化要件の 1 つです。シミュレーション時に特定の値または値の範囲に達しなければならないモデル内の信号など、単純な要件をプロパティとして指定できます。
証明が必要な論理式としてモデル化された多数の入力信号および出力信号を含むモデルの要件もプロパティになる場合があります。
Simulink Design Verifier™ ソフトウェアは、モデルの形式的解析を実行し、指定されたプロパティを証明または反証します。解析が完了したら、結果をレビューするためにいくつかの方法が提示されます。
モデル上での強調表示
テスト ケースを含むハーネス モデル
詳細な HTML レポート
Proof ブロック
Simulink Design Verifier ソフトウェアには、Simulink モデルでプロパティ証明を指定できる 2 つのブロックが用意されています。
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 インストール環境でモデルを開くと、ブロックおよび関数は表示できますが、結果は生成されません。