要件のモデル化
ブロック
Proof Assumption | モデルのプロパティを証明する場合に、信号値を制限する |
Proof Objective | モデルのプロパティを証明する場合に信号で達成されなければならないオブジェクティブを定義する |
Assertion | 信号がゼロかどうかのチェック |
Detector | 入力が true となる期間の検出と、出力タイプに基づく出力が true となる期間の作成 |
Extender | 入力が true となる期間の延長 |
Implies | 特定の応答を生成する条件の指定 |
Within Implies | 目的の期間内に応答が発生するかを確認する |
Verification Subsystem | シミュレーション結果や生成済みのコードに影響を与えることなく、証明オブジェクティブまたはテスト オブジェクティブを指定する |
関数
sldv.assume | Stateflow チャートおよび MATLAB Function ブロックについて証明の前提となる関数 |
sldv.prove | Stateflow チャートおよび MATLAB Function ブロックの証明オブジェクティブ関数 |
sldvextract | サブシステムまたはサブチャートの内容を解析用の新しいモデルに抽出する |
sldvoptions | 設計検証オプション オブジェクトの作成 |
sldvrun | モデルの解析 |
sldvreport | Simulink Design Verifier レポートを生成する |
トピック
- プロパティ証明とは
プロパティ証明の概要。
- モデル プロパティ証明のワークフロー
モデルのプロパティを証明する処理の概要を説明します。
- モデルのプロパティの証明
モデル プロパティを証明する過程を、例を使って順に確認していきます。
- 検証モデルを使用したシステムレベル プロパティの証明
検証モデルを使用してシステムレベル プロパティを証明する例。
- サブシステムのプロパティの証明
サブシステムのプロパティを証明する方法を説明します。
- モデル スライサーを使用したプロパティ証明違反のデバッグ
モデル スライサーを使用したプロパティ証明違反のデバッグ
- モデルのプロパティの設計と検証
Simulink® Design Verifier™ を使用して、設計要件をプロパティとしてモデル化し、モデル内のプロパティを証明することができます。
- Parameter Configuration for Analysis
Overview of parameter configuration for Simulink® Design Verifier™ analysis.
- モデル要件
Simulink Design Verifier ブロック ライブラリにはサブライブラリ Example Properties が含まれています。
- パラメーター テーブルの使用
解析でパラメーターを変数として指定する方法の例。
- Specify Parameter Configuration for Full Coverage
An example of how to specify parameter constraint values to achieve full model coverage.
- Design Verifier ペイン: プロパティ証明
Simulink Design Verifier による解析モデルのプロパティ証明方法を制御するオプションを指定します。
- Design Verifier Pane: Parameters and Variants
Specify options that control how Simulink Design Verifier uses parameter configurations when analyzing models.
- 解析結果のレビュー
Simulink Design Verifier の [検証結果の概要] ウィンドウで解析結果をレビューする。
- 仕様モデルとは
仕様モデルおよび要件に基づく検証での使用に関する概要。
- オブザーバーによる検証ロジックの分離
Simulink Design Verifier のオブザーバーによるサポートの説明。