Simulink Design Verifier

要求仕様に対する設計の検証

離散システムの機能要求仕様は、システムに予期される動作と発生してはならない動作についての明示的なステートメントとなっています。発生してはならない動作は、安全要求仕様と呼ばれています。

Simulink での機能要求仕様の表現

設計がこれらの要求仕様に従って動作することを形式的に検証するには、まず要求仕様のステートメントを人間の言語から形式解析エンジンが理解できる言語に翻訳する必要があります。Simulink Design Verifier を使用すると、SimulinkMATLAB® 関数および Stateflow を使用して形式的な要求仕様を表現することができます。Simulink での各要求仕様には、1 つまたは複数の検証オブジェクティブが関連付けられています。これらの検証オブジェクティブは、設計が機能要求仕様と安全要求仕様を満たすかどうかのレポートに使用されます。

Simulink Design Verifier には、検証オブジェクティブの定義と整理に使用できる一連の基本ブロックと関数が用意されています。ブロック ライブラリには、テスト オブジェクティブ、証明オブジェクティブ、アサーション、制約用のブロックと関数、および時相で検証オブジェクティブをモデル化するための専用の時相演算子が含まれています。

個々の要求仕様とそれぞれに関連する検証オブジェクティブをライブラリにまとめて、設計とは個別に管理、確認することができます。

Simulink Design Verifier library of property examples.
Simulink Design Verifier のプロパティ ライブラリの例。

Simulink Verification and Validation™ で Simulink Design Verifier を Requirements Management Interface と併用すると、要求仕様と検証オブジェクティブを取得するために使用するブロックと関数を、Simulink 外にあるさらにレベルの高い要求仕様記述とリンクすることができます。

要求仕様に対する設計の実証

要求仕様と検証オブジェクティブが検証モデルに取り込まれたら、形式的手法を使用して設計の妥当性を証明することができます。

機能要求仕様を検証してシステムを望ましい状態へ導くため、Test Objective ブロックと MATLAB 関数を使用してテスト オブジェクティブを定義することができます。テストの生成中、Simulink Design Verifier は指定されたオブジェクティブを満たす有効なテスト ケースを見つけ出そうとします。オブジェクティブを満足させることができない場合、設計は特定の解析制約に対して要求される機能を実行することができません。

設計が安全要求仕様に対して妥当であることを検証するには、Proof Objective ブロックと MATLAB 関数を使用して証明オブジェクティブを定義します。解析中、Simulink Design Verifier は好ましくない動作の原因となりうる考えられる入力条件をすべて検証し、結果を生成します。指定された証明オブジェクティブに対し、設計が有効であると証明されるか、安全要求主要に違反しているという結果が報告されます。違反が検出された場合、Simulink Design Verifier はシミュレーションで違反を再現できるテスト ベクトルを生成します。

Simulink Design Verifier report for verifying a design against safety requirements represented with proof objectives.
証明オブジェクティブで表される、安全要求仕様に対して設計を検証するための Simulink Design Verifier レポート。このレポートは、設計が有効であると証明されたオブジェクティブのリストと、解析で反例が見つかったオブジェクティブのリストを示します。

解析結果の検証

Simulink、MATLAB 関数および Stateflow で表現されている要求仕様は、設計と並行してシミュレーションすることができます。それらを使用して SIL モードまたは PIL モードで同時にシミュレートしながら生成されたコードを検証することもできます。モデル カバレッジ ツールはシミュレーション中に検証オブジェクティブのアクティベーションに関する情報を蓄積し、Simulink Design Verifier カバレッジ メトリックによってカバレッジ結果を提供します。違反時にシミュレーションを停止する安全要求仕様を表す証明オブジェクティブを使用して、根本的な原因の解析とデバッグを高速化できます。

次のトピック: モデル カバレッジの解析

製品評価版の入手または製品の購入

評価版 Simulink Design Verifier

評価版ソフトウェアを入手する

モデルベースデザインの基本環境クイック・デモ

Web セミナーを表示する