Main Content

このページは前リリースの情報です。該当の英語のページはこのリリースで削除されています。

要件のモデル化

プロパティ証明を使用した設計要件のモデル化および検証

ブロック

Proof Assumptionモデルのプロパティを証明する場合に、信号値を制限する
Proof Objectiveモデルのプロパティを証明する場合に信号で達成されなければならないオブジェクティブを定義する
Assertion信号がゼロかどうかのチェック
Detector入力が true となる期間の検出と、出力タイプに基づく出力が true となる期間の作成
Extender入力が true となる期間の延長
Implies特定の応答を生成する条件の指定
Within Implies目的の期間内に応答が発生するかを確認する
Verification Subsystemシミュレーション結果や生成済みのコードに影響を与えることなく、証明オブジェクティブまたはテスト オブジェクティブを指定する

関数

sldv.assumeStateflow チャートおよび MATLAB Function ブロックについて証明の前提となる関数
sldv.proveStateflow チャートおよび MATLAB Function ブロックの証明オブジェクティブ関数
sldvextractサブシステムまたはサブチャートの内容を解析用の新しいモデルに抽出する
sldvoptions設計検証オプション オブジェクトの作成
sldvrunモデルの解析
sldvreportSimulink Design Verifier レポートを生成する

トピック