このページの翻訳は最新ではありません。ここをクリックして、英語の最新版を参照してください。
要件のモデル化
ブロック
| 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™ を使用して、設計要件をプロパティとしてモデル化し、モデル内のプロパティを証明することができます。
Simulink® Design Verifier™ による解析のパラメーター コンフィギュレーションの概要。
Simulink Design Verifier ブロック ライブラリにはサブライブラリ Example Properties が含まれています。
解析でパラメーターを変数として指定する方法の例。
パラメーター制約値の指定によりフル モデル カバレッジを達成する方法の例。
Simulink Design Verifier による解析モデルのプロパティ証明方法を制御するオプションを指定します。
Simulink Design Verifier によるモデル解析時のパラメーター コンフィギュレーションの使用を制御するオプションを指定します。
Simulink Design Verifier の [検証結果の概要] ウィンドウで解析結果をレビューする。
仕様モデルおよび要件に基づく検証での使用に関する概要。
Simulink Design Verifier のオブザーバーによるサポートの説明。
注目の例
You can also select a web site from the following list:
Americas
- América Latina (Español)
- Canada (English)
- United States (English)
Europe
- Belgium (English)
- Denmark (English)
- Deutschland (Deutsch)
- España (Español)
- Finland (English)
- France (Français)
- Ireland (English)
- Italia (Italiano)
- Luxembourg (English)
- Netherlands (English)
- Norway (English)
- Österreich (Deutsch)
- Portugal (English)
- Sweden (English)
- Switzerland
- United Kingdom (English)
