設計要件の指定と検証
安全要件はモデルにおいて望ましくない動作を定義します。Simulink® Design Verifier™ はプロパティ証明を使用して、モデル要件に関連付けられているプロパティが、すべての可能な入力値に有効であることを検証し、また違反を引き起こす反例を提供します。Simulink Design Verifier を使用して、設計要件をプロパティとしてモデル化し、次にモデルのプロパティの証明を行います。
ブロック
関数
トピック
- Simulink Design Verifier を使用したモデル プロパティの証明
プロパティ証明の概要。
- モデルのプロパティの証明
指定するモデル プロパティを、Proof Objective ブロックを使用して証明する。
- モデル スライサーを使用したプロパティ証明違反のデバッグ
モデル スライサーを使用して、Assertion ブロックで設計をデバッグします。
- 検証モデルを使用したシステムレベル プロパティの証明
検証モデルを使用してシステムレベル プロパティを証明する例。
- Proof Objective ブロックを使用したプロパティ証明
Simulink® Design Verifier™ を使用して、設計要件をプロパティとしてモデル化し、モデル内のプロパティを証明することができます。
- MATLAB Function ブロックを使用したプロパティ証明
この例では、シート ベルト リマインダーの設計モデルを検証する方法を示します。
- MATLAB Truth Table ブロックを使用したプロパティ証明
この例では、一番上のブロックで参照されるシート ベルト リマインダーの設計モデルを検証する方法を示します。
- Assumption ブロックによるプロパティ証明
この例では、Proof Assumption ブロックを使用した、Simulink® Design Verifier™ のプロパティ証明の実行方法を示します。
- 無効なプロパティを含むプロパティ証明
この例では、Simulink® Design Verifier™ のプロパティ証明解析を使用した、無効なプロパティの検索方法を示します。
- デバウンス時相プロパティ
プロパティ証明とテスト ケース生成のために、時相システム要件をモデル化する。
- パワー ウィンドウ コントローラー時相プロパティ
この例では、Simulink® Design Verifier™ の Temporal Operator ブロックを使用してパワー ウィンドウ コントローラー モデルの時相システム要件をモデル化し、プロパティ証明とテスト ケースの生成を行う方法を説明します。
- 大規模モデルのプロパティの証明
Simulink Design Verifier ワークフローとベスト プラクティスを使用して、大規模モデルでプロパティを証明する。
- モデルおよびコードの検証と妥当性確認
要件を定義し、モデルとコードをテストし、設計エラーの有無をチェックし、標準に準拠しているかどうかを確認し、テスト カバレッジを測定する。
- オブザーバーによる検証ロジックの分離
Observer ブロックを使用してモデル内の検証ロジックを分離する。
注目の例
モデル プロパティの解析による要件の検証
プロパティとしてモデル化された要件への準拠について、制御システムモデルを解析し、依存関係の分析を使用してプロパティの違反を調べます。
クルーズ コントロール のプロパティ証明ワークフロー
この例では、Simulink® Design Verifier™ のプロパティ証明解析を使用した、プロパティ違反の検出方法を示します。安全要件をプロパティとしてモデル化してから、要件に対して設計モデルを検証します。
逆噴射装置のプロパティ証明ワークフロー
この例では、逆噴射装置の設計モデルで安全性のプロパティを検証する方法を示します。その下の Properties ブロックには 4 つの安全性プロパティが含まれています。Simulink® Design Verifier™ は正確性を検証または反例を同定するために、設計モデルおよび安全性プロパティを解析します。モデル参照を使用すると設計モデルに検証内容を追加する必要がなくなるため、検証内容を設計から独立して配置することができます。
複数のプロパティによるプロパティ証明
この例では、複数のプロパティによるプロパティ証明解析の実行方法を示します。このモデルは次の証明を試行する解析用に設定されます。
ブロック置換による固定小数点のクルーズ コントロールのプロパティ証明ワークフロー
この例では、固定小数点のクルーズ コントロール アルゴリズムによるプロパティの証明方法を示します。これは、モデル参照を使用して設計モデルを参照するため、元の設計モデルは変更されません。ブロック置換ルールにより、オーバーフローが可能かどうかをチェックするプロパティが指定されます。検証サブシステムにより、プロパティ証明中の速度入力の範囲に対する仮定が指定されます。このモデルは、参照モデルで固定小数点 PI コントローラーの Outport を接続する Sum ブロックにブロック置換を適用し、オーバーフローを示す反例が返されるように Simulink® Design Verifier™ を設定します。
Observer Reference ブロックを使用したプロパティ証明解析
Observer Reference ブロックを使用して、プロパティ証明解析を実行する。
Requirements Table ブロックでのプロパティの証明
Requirements Table ブロックと Simulink Design Verifier を使用してモデルのプロパティを証明する。
