このページの内容は最新ではありません。最新版の英語を参照するには、ここをクリックします。
設計要件の指定と検証
安全要件はモデルにおいて望ましくない動作を定義します。Simulink® Design Verifier™ はプロパティ証明を使用して、モデル要件に関連付けられているプロパティが、すべての可能な入力値に有効であることを検証し、また違反を引き起こす反例を提供します。Simulink Design Verifier を使用して、設計要件をプロパティとしてモデル化し、次にモデルのプロパティの証明を行います。
ブロック
関数
トピック
はじめに
- Simulink Design Verifier を使用したモデル プロパティの証明
プロパティ証明の概要。 - モデルのプロパティの証明
モデル プロパティを証明する過程を、例を使って順に確認していきます。 - パラメーター テーブルを使用した制約の検索
解析でパラメーターを変数として指定する方法の例。 - 信号範囲の指定
シミュレーション中に信号が到達できる最小値と最大値を指定する。設計を完全に指定し、シミュレーション中に信号が到達できる最小値と最大値を指定することでデータ型と生成コードを最適化します。 - 最小値と最大値の入力制約
Simulink Design Verifier 解析が、指定された入力の最小値および最大値をどのように考慮するかについての概要。 - Simulink 要素と Stateflow 要素に対する入力範囲の指定
解析で Simulink 要素と Stateflow® 要素の最小値および最大値がどのように処理されるかについて説明する。 - モデルおよびコードの検証と妥当性確認
要件を定義し、モデルとコードをテストし、設計エラーの有無をチェックし、標準に準拠しているかどうかを確認し、テスト カバレッジを測定する。
検証と妥当性確認のための要件のモデル化
- Simulink 要素と Stateflow 要素に対する入力範囲の指定
解析で Simulink 要素と Stateflow 要素の最小値および最大値がどのように処理されるかについて説明する。 - 要件に基づくテストに対する仕様モデルの使用
要件に対して設計モデルを検証する体系的なアプローチに従います。 (R2022b 以降)
プロパティ証明による検証
- モデルのプロパティの証明
モデル プロパティを証明する過程を、例を使って順に確認していきます。 - モデルのプロパティの設計と検証
Simulink® Design Verifier™ を使用して、設計要件をプロパティとしてモデル化し、モデル内のプロパティを証明することができます。 - モデル スライサーを使用したプロパティ証明違反のデバッグ
モデル スライサーを使用して、Assertion ブロックで設計をデバッグします。 - 検証モデルを使用したシステムレベル プロパティの証明
検証モデルを使用してシステムレベル プロパティを証明する例。 - サブシステムのプロパティの証明
サブシステムのプロパティを証明する方法を説明します。 - 指定された最小値および最大値の違反チェック
モデルを解析して、指定された設計の最小値および最大値が守られていることを検証する方法を説明します。 - sldvData フィールドの入力範囲の指定
入力の最小値および最大値に使用するsldvDataフィールドについて説明します。 - MATLAB Function ブロックを使用したプロパティ証明
この例では、シート ベルト リマインダーの設計モデルを検証する方法を示します。 - MATLAB Truth Table ブロックを使用したプロパティ証明
この例では、一番上のブロックで参照されるシート ベルト リマインダーの設計モデルを検証する方法を示します。 - Assumption ブロックによるプロパティ証明
この例では、Proof Assumption ブロックを使用した、Simulink® Design Verifier™ のプロパティ証明の実行方法を示します。 - 無効なプロパティを含むプロパティ証明
この例では、Simulink® Design Verifier™ のプロパティ証明解析を使用した、無効なプロパティの検索方法を示します。 - 大規模モデルのプロパティの証明
大規模モデルでプロパティを証明するためのワークフローとベスト プラクティスについて説明します。
注目の例
モデル プロパティの解析による要件の検証
プロパティとしてモデル化された要件への準拠について、制御システムモデルを解析し、依存関係の分析を使用してプロパティの違反を調べます。
クルーズ コントロール のプロパティ証明ワークフロー
この例では、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 を使用してモデルのプロパティを証明する。
