プロパティとしてモデル化された要件への準拠について、制御システムモデルを解析し、依存関係の解析を使用してプロパティの違反を調べます。

この例では、Simulink® Design Verifier™ のプロパティ証明解析を使用した、プロパティ違反の検出方法を示します。安全要件をプロパティとしてモデル化してから、要件に対して設計モデルを検証します。

この例では、逆噴射装置の設計モデルで安全性のプロパティを検証する方法を示します。その下の Properties ブロックには 4 つの安全性プロパティが含まれています。Simulink Design Verifier は正確性を検証または反例を同定するために、設計モデルおよび安全性プロパティを解析します。モデル参照を使用すると設計モデルに検証内容を追加する必要がなくなるため、検証内容を設計から独立して配置することができます。

この例では、複数のプロパティによるプロパティ証明解析の実行方法を示します。このモデルは次の証明を試行する解析用に設定されます。

この例では、固定小数点のクルーズ コントロール アルゴリズムによるプロパティの証明方法を示します。これは、モデル参照を使用して設計モデルを参照するため、元の設計モデルは変更されません。ブロック置換ルールにより、オーバーフローが可能かどうかをチェックするプロパティが指定されます。検証サブシステムにより、プロパティ証明中の速度入力の範囲に対する仮定が指定されます。このモデルは、参照モデルで固定小数点 PI コントローラーの Outport を接続する Sum ブロックにブロック置換を適用し、オーバーフローを示す反例が返されるように Simulink Design Verifier を設定します。

この例では、仕様モデルを使用して要件に基づくテストを実行する方法を説明します。この例では、要件に対して設計モデルを検証する体系的なアプローチに従います。仕様モデルの詳細な説明については、仕様モデルとはを参照してください。