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

R2022a 以降

Requirements Table ブロックの使用時に、矛盾する要件セットや不完全な要件セットを特定し、排他性や書き込み前の読み取りのエラーを見つけることができます。これらの問題は、要件セットの問題が原因になっている場合もあれば、個々の要件のセマンティックエラーに起因している場合もあります。

ブロックの解析

形式的要件では、前提条件、事後条件、アクション、および指定された子の評価で使用されるデータがシミュレーションのタイムステップごとに一意に定義されている必要があります。要件を解析することで、これらのガイドラインを満たさないブロックを特定できます。解析で次の問題が特定されます。

少なくとも 1 つのデータに値が割り当てられていないシナリオがブロックで実行される可能性がある場合、"不完全" な要件セットになります。
要件セットで定義されている少なくとも 1 つのデータがシミュレーション時に複数の値と等しくなる可能性がある場合、"矛盾" した要件セットになります。
データを書き込み前に使用する要件を定義した場合、その要件セットで書き込み前の読み取りのエラーが発生する可能性があります。
排他的かつ網羅的な要件が複数アクティブになっているか 1 つもアクティブになっていない場合、要件に排他性の問題があります。

一般に、これらのシナリオではシミュレーション時にエラーが生成されますが、手動で検出するのは難しい場合があります。Simulink^® Design Verifier™ がある場合は、このようなシナリオの原因を検出できます。要件を解析するには、Requirements Table ブロックを開きます。[テーブル] タブの [解析] セクションで [テーブルの解析] をクリックします。

不整合の問題

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

This table illustrates the results of analysis that shows the inconsistent requirements and how the table highlights them.

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

This shows an example of incompatibilities results that occurs when you analyze the requirements shown above.

不完全性の問題

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

This shows an example of incompleteness results that occurs when you analyze the requirements in the generator_mode_example model.

これらの問題を解決するには、u1 と u2 が 0 以下になる状況を定義する要件を導入するか、u1 と u2 を 0 以上に制約する仮定を作成します。仮定を記述する方法の詳細については、要件への仮定の追加を参照してください。

書き込み前の読み取りの問題

書き込み前の読み取りの問題は、まだ定義されていないデータを要件で読み取ろうとすると発生します。ほとんどの場合、書き込み前の読み取りの問題については、前提条件と事後条件で出力データを呼び出さないようにするか、要件を順番に指定することで、発生する可能性を最小限に抑えることができます。詳細については、Requirements Table ブロックの階層の確立を参照してください。たとえば、次のテーブルでは、出力データ y2 に値が代入される前に最初の要件で y2 を読み取っています。

This image shows an example table that produces a read-before-write issue. The action for the first requirement reads y2 before it is written.

要件を解析すると、書き込み前の読み取りの問題がブロックで検出されます。

This image shows the analysis results from the table shown previously.

要件を順番にリストし、ブロックで [前提条件で出力を有効にする] プロパティを有効にすると、出力データに依存する要件の前提条件を作成できます。前提条件で出力を有効にするを参照してください。たとえば、要件の順序の使用例で使用しているモデルでは、他の要件で必要になる前にローカルデータを指定しているため、この要件の順序では要件の問題は発生しません。要件の順序を変更して要件 3 と 4 を先にリストすると、要件の解析時に書き込み前の読み取りの問題が 2 つ検出されます。

メモ

記述された要件に書き込み前の同じデータを読み取る要件が 2 つよりも多く含まれている場合、解析では問題がある要件のうちの最初にリストされている要件についてしか問題が検出されません。その問題を解決した後、解析を再度実行して、次の書き込み前の読み取りの問題を検出してください。

排他性の問題

要件に排他性の問題があると見なされるのは、排他的かつ網羅的な要件が複数アクティブになっている場合、または排他的かつ網羅的な要件が 1 つもアクティブになっていない場合です。排他的かつ網羅的な要件に排他性の問題がある場合、親要件がテーブルで赤で強調表示され、警告アイコンが表示されます。たとえば、次のテーブルには排他性の問題が 2 つあります。

An example table with a exclusivity errors. The parent requirement is highlighted red and includes an alert icon.

[解析結果] ペインに、排他性の問題に関する追加の情報が表示されます。

This image shows the analysis results pane information for the two exclusivity issues in the table above.

1 つ目の問題を修正するには、u が 3 より大きい場合のオーバーラップがなくなるように既存の要件を変更します。2 つ目の問題を修正するには、u が -4 以上 0 以下である場合について定義する要件を導入します。

解析にモデル全体を含める

既定では、Requirements Table ブロックの入力データは独立して生成されるものと仮定されます。入力データが独立していない場合、問題を防ぐために要件を過剰に指定しなければならないことがあります。この問題は次のようにして回避できます。

原因のデータをモデル全体のコンテキストで特定するようにブロックを構成します。[テーブル] タブの [解析] セクションで、[テーブルの解析] メニューを展開し、[モデル全体を含む] を有効にします。
物理的または数学的な制限によってデータが特定の値にならない状況に基づいて仮定を指定します。要件への仮定の追加を参照してください。

厳格な要件と柔軟な要件の解析

データ間の関係の定義方法に応じて、"厳格" と "柔軟" の 2 種類の要件を確立できます。個々の要件に加え、ブロック内の要件のセットも厳格または柔軟にすることができます。

厳格な要件

要件の事後条件で正確な値を指定する場合、または要件でアクションのみを指定する場合、その要件は "厳格" になります。このような要件の事後条件は 2 つの等号 == で表現します。たとえば、事後条件が y == 0 である要件は厳格です。要件セットの各要件が厳格であれば、その要件セットは厳格になります。

柔軟な要件

要件の事後条件で値の範囲を満たすことができる場合、その要件は "柔軟" になります。たとえば、事後条件が y >= 0 や y >= 0 && y < -2 である要件は柔軟です。さらに、複数の値を指定する事後条件の場合も柔軟な要件が作成されます。たとえば、事後条件が u == 3 || u == 4 である要件は柔軟です。要件セットの少なくとも 1 つの要件が柔軟であれば、その要件セット全体が柔軟になります。