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

Requirements Table ブロックでのプロパティの証明

R2023a 以降

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

モデルを開く

この例では、Requirements Table ブロックと Simulink® Design Verifier™ を使用してエンジン逆噴射装置システムのプロパティを証明する方法を示します。

プロパティ証明に Requirements Table ブロックと Simulink Design Verifier を使用するときは、次のようになります。

  1. ブロックの各要件で、モデル、サブシステム、またはブロックのプロパティのテストに使用できる形式的要件が定義されます。この例の Requirements Table ブロックでは、要件を前提条件および事後条件として表します。

  2. ブロックの各要件で、要件エディターに対応する要件が生成されます。形式的要件のプロパティの構成を参照してください。

  3. Simulink Design Verifier で、要件セット内の要件の証明オブジェクティブが生成されます。通常はProof Objective (Simulink Design Verifier)ブロックで定義する論理条件が事後条件で定義されます。事後条件に関連付けられた証明オブジェクティブは、前提条件が true の場合のみブロックで評価されます。

詳細については、Requirements Table ブロックを使用した形式的要件の作成およびSimulink Design Verifier を使用したモデル プロパティの証明 (Simulink Design Verifier)を参照してください。

Requirements Table ブロックの要件の確認

モデル例 property_proving_reqtable を開きます。この例では、エンジン逆噴射装置システムのプロパティをテストします。これは、チャート ThrustReverserDeployLogic でモデル化されています。Requirements Table ブロックで、チャートの入力信号と deploy 出力信号を使用してチャートの動作を観察します。チャートの入力と出力を評価するために、ブロックではデータが式で定義されています。Requirements Table ブロックのデータの定義を参照してください。

各要件に関連付けられている検証ロジックを確認するには、Requirements Table ブロックを開きます。要件はモデル プロパティの解析による要件の検証 (Simulink Design Verifier)の例で使用されている要件セット内の要件に対応しています。ブロックで証明するプロパティは次のとおりです。

  1. 対気速度が 150 ノットより大きい場合、逆噴射装置を配置しない。

  2. Weight on Wheel センサーの値が示すように、航空機が空中にある場合、逆噴射装置を配置しない。航空機が空中にある場合、2 つの Weight on Wheel (WOW) センサーのそれぞれの信号値は false です。

  3. いずれかの推力センサーの値が正である場合、逆噴射装置を配置しない。

  4. 着陸装置の車輪の回転速度がしきい値より小さい場合、逆噴射装置を配置しない。

各要件はプロパティを定義します。前提条件が有効な場合、プロパティを証明するには事後条件も満たさなければなりません。

プロパティの証明

プロパティを証明するには、[Design Verifier] タブで [プロパティの証明] をクリックします。この例では、チャートのプロパティが証明されます。証明された証明オブジェクティブに関連付けられている事後条件は、Requirements Table ブロックによって緑で強調表示されます。

要件の証明オブジェクティブが反証された場合、その要件はブロックによって赤で強調表示されます。それ以外に、Simulink Design Verifier で証明オブジェクティブを証明または反証できない場合は、ブロックによって要件が黄色で強調表示されます。この動作については、この例のチャートをモデル プロパティの解析による要件の検証 (Simulink Design Verifier)の例で使用されているチャートの最初の反復に置き換えると調べることができます。

参考

トピック