Main Content

設計要件の指定と検証

要件に対して設計を検証し、入力仮定を使用して反例を調整する

安全要件はモデルにおいて望ましくない動作を定義します。Simulink® Design Verifier™ はプロパティ証明を使用して、モデル要件に関連付けられているプロパティが、すべての可能な入力値に有効であることを検証し、また違反を引き起こす反例を提供します。Simulink Design Verifier を使用して、設計要件をプロパティとしてモデル化し、次にモデルのプロパティの証明を行います。

ブロック

すべて展開する

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 レポートを生成する

トピック

はじめに

検証と妥当性確認のための要件のモデル化

プロパティ証明による検証