矛盾する形式的要件セットおよび不完全な形式的要件セットの特定

R2022a 以降

Simulink^® Design Verifier™ がある場合、Requirements Table ブロックで矛盾する要件セットや不完全な要件セットを特定できます。不完全な要件セットと見なされるのは、少なくとも 1 つのデータに値が割り当てられていないシナリオがブロックで実行される可能性がある場合です。矛盾する要件セットと見なされるのは、要件セットで定義されている少なくとも 1 つのデータがシミュレーション時に複数の値と等しくなる可能性がある場合です。

不整合と不完全性の問題について要件を解析するには、Requirements Table ブロックを開きます。[テーブル] タブの [解析] セクションで [テーブルの解析] をクリックします。テーブル解析で検出される問題の詳細については、Analyze Requirements Table Blocks for Modeling Problemsを参照してください。

不整合の問題

不整合の問題は、入力値の単一の組み合わせに対してブロックで複数の動作が実行される可能性がある場合に発生します。たとえば、次のテーブルは矛盾する要件を示しています。テーブル解析により、不整合の問題が 2 つ検出されます。赤で強調表示され、警告アイコンのフラグが付いています。

Requirements table that defines an inconsistent requirement set.

[解析結果] ペインに、不整合の問題に関する追加の詳細が表示されます。

Input information for two inconsistency issues

不整合の問題は、入力値の単一の組み合わせに対して定義される動作が 1 つだけになるように要件を変更することで修正できます。このテーブルでは、u1 が 0 以上で u2 が 0 未満のときの y1 と y2 のブロック出力が要件 2.2 と 2.3 の両方で定義されています。不整合の問題を解決するには、要件 2.2 または 2.3 を削除するか、要件の前提条件を定義し直します。

不完全性の問題

要件に不完全性の問題があると見なされるのは、可能性があるすべての入力値に対する出力がブロックで指定されていない場合です。たとえば、モデルの動作の生成の例で使用しているモデルでは、テーブルに不完全性の問題が 2 つ含まれています。

Input information for two incompleteness issues

不完全性の問題は、可能性があるすべての入力値に対して出力を指定することで修正できます。たとえば、これらの不完全性の問題を解決するには、u1 と u2 が 0 以下になる状況を定義する要件を導入するか、u1 と u2 を 0 以上に制約する仮定を作成します。仮定を記述する方法の詳細については、要件への仮定の追加を参照してください。

不完全性の問題の抑制

出力に対する不完全性の問題は、シミュレーション時や解析時に抑制することができます。たとえば、要件セット全体をまだモデル化していない場合に他の問題についてモデルを解析するときは、不完全性の問題を抑制することができます。また、設計のスコープに含まれない要件があり、その出力について考慮する必要がないため不完全性のチェックから除外する場合も、不完全性の問題を抑制することができます。モデル出力に対する不完全性の問題を抑制してテーブルを解析すると、不完全なデータに不完全性のフラグが付けられず、[解析結果] ペインに問題が表示されません。

出力に対する不完全性の問題を抑制するには、関数 anyValue を使用します。anyValue は要件行の事後条件セルでのみ使用できます。

たとえば、Prove Properties with Requirements Table Blocksの例で使用しているモデルでは、エンジン逆噴射装置システムの形式的要件をテーブルでモデル化していますが、要件領域全体についてはモデル化していません。このテーブルのモデル化の問題について解析すると、[解析結果] ペインに不完全性の問題が表示されます。

Requirements table with four requirements. The postcondition data displays red higlighting, the alert icon with the cursor over it and additional information on the incompleteness issues to the right.

要件を定義する過程の初期の段階であり、不完全の問題を抑制するとします。事後条件が deploy == anyValue である既定の要件を定義できます。テーブルを解析するかモデルをシミュレートすると、テーブルで不完全性の問題が抑制されます。詳細については、anyValue を参照してください。

Requirements table with five requirements. The last requirement has a postcondition that verifies the design model output is equal to anyValue.

関数 anyValue は、不完全性の問題をグローバルに抑制するわけではありません。たとえば、次のテーブルで u が 10 より大きい場合の出力 y には不完全性のフラグが付けられませんが、このテーブルを解析すると、u が 0 以上 10 以下である場合の出力 y に対する不完全性の問題がブロックから返されます。この不完全性の問題を抑制するには、u が 0 以上 10 以下の場合についてチェックする前提条件が設定された要件を作成し、出力 y が anyValue と等しいことをチェックするように事後条件を定義します。

Requirements table with two requirements. The postcondition data displays red higlighting, the alert icon with the cursor over it and additional information on the incompleteness issues to the right.

参考

Requirements Table | anyValue