モデルプロパティの解析による要件の検証

この例では次を使用します。

個別の要件をモデル化するプロパティを解析して、要件セットを検証します。反証されたプロパティは、設計と要件セットの不完全性を示しています。

概要

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

対気速度が 150 ノットより大きい場合、逆噴射装置を配置しない。
Weight on Wheel センサーの値が示すように、航空機が空中にある場合、逆噴射装置を配置しない。航空機が空中にある場合、2 つの Weight on Wheel (WOW) センサーのそれぞれの信号値は false です。
いずれかの推力センサーの値が正である場合、逆噴射装置を配置しない。
着陸装置の車輪の回転速度がしきい値より小さい場合、逆噴射装置を配置しない。

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

安全性プロパティの解析

1.[モデルを開く] ボタンをクリックして元のモデルを開き、サンプルファイルの作業ディレクトリを作成します。

Safety Properties サブシステムは Simulink® Design Verifier™ ライブラリの Verification Subsystem ブロックです。Safety Properties の検証ロジックは安全性要件をモデル化します。たとえば、対気速度の要件は次によって検証されます。

Verification Subsystem ブロックの詳細については、Verification Subsystem (Simulink Design Verifier)を参照してください。

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

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

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

4.モデルプロパティを解析します。[アプリ] タブで、[Design Verifier] をクリックします。[Design Verifier] タブで、[プロパティの証明] をクリックします。

プロパティ解析が完了したら、[リフレッシュ] ボタンをクリックして [Verified] 列の状態を更新します。この結果は、4 つのオブジェクティブのうち 3 つが反証されたことを示します。つまり、解析によって、プロパティを反証し、したがって要件に違反する信号条件が見つかったということです。

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

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

t = 0.1 では、対気速度がしきい値を下回る場合に逆噴射装置を配置させる。
t = 0.2 では、対気速度がしきい値を上回るが逆噴射装置はまだ配置されている。

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

1.[Design Verifier] タブで [モデル内で強調表示] ボタンをクリックします。

2.Test Unit > Safety Properties > airspeed property サブシステムで airspeed valid assertion ブロックを選択します。

3.[Design Verifier] タブで [スライサーを使用したデバッグ] ボタンをクリックします。モデルで airspeed valid assertion の依存関係が強調表示され、T = 0.2 での信号の値が表示されます。

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

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

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

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

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

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

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

追加の aboutToBeDeployed ステート。
undeployed に戻る、拡大された遷移条件。

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

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

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

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

4.要件 1.1 の Airspeed Condition について、Safety Properties > airspeed property サブシステムの airspeed valid ブロックにリンクします。要件ブラウザーから、R1.1 をモデルの airspeed valid ブロックにドラッグします。

5.要件エディターの右側のペインの [リンク] に、新しいリンクが表示されます。

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