概要

この例では，エンジン逆噴射装置システムの4の要件に基づくモデルプロパティを解析します。プロパティ解析で得られた反証結果は,システムの設計要件が不完全(次の要件のいくつかに違反する動作がシステムで許容されている)であることを示唆しています。

モデルの動作をよりよく理解するため,システムに必要な制御ロジックがないために望ましくないモデルの動作を引き起こす時系列入力の依存関係を解析します。次に，プロパティ解析をパスする改訂された制御システムモデルを解析します。

安全性プロパティの解析

1.[モデルを開く]ボタンをクリックして元のモデルを開き，サンプルファ。

安全属性サブシステムはSimulink®设计验证器™金宝appラブラリの验证子系统ブロックです。安全属性の検証ロジックは安全性要件をモデル化します。たとえば，対気速度の要件は次によって検証されます。

验证子系统ブロックの詳細にいては，验证子系统を参照してください。

2.要件を表示します。モデルで右下の[パ，スペクティブビュ，を表示します]ア电子邮箱コンをクリックし，[要件]を選択します。[要件]ペ@ @ンが開きます。thrust_reverser_safety_requirementsを展開します。

安全性要件は安全属性サブシステムの断言ブロックにリンクされます。断言ブロックは証明オブジェクティブとみなされます。各要件の検証の状態に，対応する断言ブロックのプロパティ解析結果が反映されます。

3.要件の検証の状態が表示されます。ブラウザ，でいずれかの要件を右クリックし，[検証の状態]を選択します。(验证)の列は，要件が実行されていないことを示しています。

4.モデルプロパティを解析します。[アプリ]タブで，(设计验证器)をクリックします。(设计验证器)タブで，[プロパティ証明]をクリックします。

プロパティ解析が完了したら，[更新]ボタンをクリックして(验证)列の状態を更新します。この結果は，4。つまり,解析によって,プロパティを反証し,したがって要件に違反する信号条件が見つかったということです。

反例を使用したモデルの動作の解析

[金宝appSimulink Design Verifierの検証結果の概要]ウィンドウで[HTML]をクリックして詳細な解析レポ，トを開きます。第4章で，反証されたそれぞれのプロパティには反例がリストされます。たとえば，対気速度の要件を反証する反例は次のようになります。

反例の時系列は,シミュレーションでは遭遇することが難しいような条件を示していますが,それでも,要件に違反するモデルの動作を引き起こしています。反例での信号の依存関係を解析して，その動作を調べます。

1.(设计验证器)タブで[モデル内で強調表示]ボタンをクリックします。

2.>安全属性>空速属性サブシステムで空速有效断言ブロックを選択します。

3.(设计验证器)タブで[スラeconp econpサを使用したデバッグ]ボタンをクリックします。モデルで空速有效断言の依存関係が強調表示され,T = 0.2での信号の値が表示されます。

4.モデルで1上のレベルの安全属性サブシステムに移動します。反例シミュレ，ション時間のステップを戻します。[シミュレ，ション]タブで，[ステップを戻す]をクリックします。

5.T = 0.1で，平均対気速度はしきい値を下回っており，逆噴射装置が配置されます。ステップを進めてT = 0.2で,平均対気速度はしきい値を上回っており,逆噴射装置はまだ配置されています。これは要件に違反しています。

反証されたプロパティと依存関係解析は,制御システムのアルゴリズムが不完全な設計であり,要件が不完全であることを示唆しています。

再設計されたシステムの解析

制御システムの再設計には，要件の再考が必要となります。この場合では,中間のスタンバイステートがないことで,入力が突然変化するときに望ましくないシステムの動作が生じる余地があります。逆噴射装置の応答を遅らせる中間配置モ，ドを追加することで，この問題を解決します。

reqs_validation_property_proving_redesigned_modelモデルを開きます。thrustReversersチャ，トを開きます。

追加の設計要件は，一時停止後に逆噴射装置が配置されることを示しています。再設計されたモデルには次のものが含まれます。

再設計されたモデルの検証ブロックから要件へのリンクを作成します。

1.モデルで，[アプリ]タブから[要件マネ，ジャ，]をクリックします。

2.[要件]タブで[要件エディタ]をクリックします。

3.[要件エディタ]でthrust_reverser_safety_requirementsを開きます。

4.要1.1件の空速条件について,安全属性>空速属性サブシステムの空速有效ブロックにリンクします。要件ブラウザーから,R1.1をモデルの空速有效ブロックにドラッグします。

5.要件エディタの[詳細]ペereplicationンの[リンク]に，新しいリンクが表示されます。

6.元のモデルのassertブロックへのリンクを削除します。元のモデルが閉じている場合は，このリンクは未解決として表示されます。リンクの隣の[リンクの削除]ア@ @コンをクリックします。

7.再設計されたモデルで，他の3の要件と検証ブロックにいて繰り返します。

改訂されたモデルに対してプロパティ解析を実行します。結果が[要件]ペ操作系统ンに表示されます。

結果は，プロパティが有効であることを示しています。