設計要件の指定と検証

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

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

ブロック

すべて展開する

設計要件の検証

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 要素と Stateflow 要素に対する入力範囲の指定
解析で Simulink 要素と Stateflow^® 要素の最小値および最大値がどのように処理されるかについて説明する。

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

仕様モデルとは
仕様モデルおよび要件に基づく検証での使用に関する概要。 (R2022b 以降)
モデル要件
Simulink Design Verifier ブロックライブラリにはサブライブラリ Example Properties が含まれています。
オブザーバーによる検証ロジックの分離
Simulink Design Verifier のオブザーバーによるサポートの説明。
指定入力の最大および最小制約値としての使用
この例では、Simulink® Design Verifier™ でのテスト生成時とプロパティ証明時の両方について、解析の制約として入力端子の最小値と最大値を使用する方法を示します。
要件に基づくテストに対する仕様モデルの使用
要件に対して設計モデルを検証する体系的なアプローチに従います。 (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 を設定します。