Main Content

このページの内容は最新ではありません。最新版の英語を参照するには、ここをクリックします。

モデルのプロパティの設計と検証

スクリプトを開く

Simulink® Design Verifier™ を使用して、設計要件をプロパティとしてモデル化し、モデル内のプロパティを証明することができます。モデル要件に関連付けられたプロパティが、すべての可能な入力値に収まることを検証するため、プロパティ証明解析を使用します。要件が失敗した場合、Simulink Design Verifier は、失敗をデバッグするための反例を提供します。

この例では、Proof Objective ブロックを使用して、設計要件をプロパティとしてモデル化した後、単純なクルーズ コントロール モデルの解析に記載した簡略化されたクルーズ コントロール モデルでこのプロパティを検証する方法を説明します。

手順 1: Verification サブシステムを使用したプロパティの設計

モデル sldvexSimpleCruiseControlProperties には Verification サブシステムが含まれており、その中には Proof Objective ブロックを使用してモデル化された機能要件が含まれています。

load_system('sldvexSimpleCruiseControlProperty');
open_system('sldvexSimpleCruiseControlProperty/Verification Subsystem');

手順 2: プロパティ証明解析の実行

[アプリ] タブの [アプリ] セクションの右端にある矢印をクリックします。[モデルの検証とテスト] ギャラリーで [Design Verifier] をクリックします。

プロパティ証明解析を実行するには、[プロパティの証明] をクリックします。モデルが解析され、[結果の概要] ウィンドウに結果が表示されます。1 のオブジェクティブが近似において有効であるという結果が表示されます。

手順 3: 解析結果のレビュー

[Design Verifier] タブの [結果の確認] セクションで、[モデル内で強調表示] をクリックします。

近似において有効なプロパティがオレンジ色で強調表示されます。Proof Objective ブロックをクリックします。結果インスペクター ウィンドウに、Proof Objective ブロックのオブジェクティブが表示されます。

HTML レポートを表示するには、[結果の確認] セクションで [HTML レポート] をクリックします。「証明オブジェクティブ ステータス」の章に、近似において有効であることがわかった証明オブジェクティブがリストされます。

参考