Requirements Table ブロックを使用した形式的要件の作成

R2022a 以降

形式的要件をモデル化するには Requirements Table ブロックを使用します。シミュレーション時に目的のモデルの動作が発生するかどうかをチェックする論理式を使用して形式的要件を確立します。Requirements Table ブロックで要件を作成すると、要件エディターでも等価な要件が作成されます。形式的要件のプロパティの構成を参照してください。

形式的要件の定義

形式的要件は、数学的に表現した明確な仕様のセットであり、シミュレーションを通じて実行されます。各形式的要件は、少なくとも 1 つの条件が指定の持続時間にわたって true である場合に実行されます。要件の実行時、指定したシミュレーション動作がブロックで検証され、追加のシミュレーションデータが生成されます。

形式的要件を定義するには、モデルに Requirements Table ブロックを追加します。

This is the appearance of the Requirements Table block.

新しい Requirements Table ブロックを開くと、空白の要件が表示されます。既定では、[要件] タブでブロックが開きます。テーブルの各行が要件を表します。列は各要件の評価に使用される情報を指定します。次の列があります。

インデックス — 各要件の一意の識別子。この列は読み取り専用です。
概要 — 要件のテキストベースの概要。この列のエントリはブロックの動作に影響しません。この列はオプションです。
前提条件 — 残りの要件を評価するために指定の持続期間にわたって true でなければならない論理式。
持続時間 — 残りの要件を評価するために前提条件が true でなければならない時間 (秒数)。この列はオプションです。空白のままにすると、要件に持続時間が含まれません。この列を使用するには、前提条件を指定する必要があります。[持続時間] 列の使用を参照してください。
事後条件 — 関連付けられた前提条件が指定の持続時間にわたって true である場合に true でなければならない論理式。前提条件を含めていない場合、ブロックは各タイムステップで事後条件をチェックします。
アクション — 関連付けられた前提条件が指定の持続時間にわたって true である場合にブロックで実行されるアクション。アクションを使用して、ブロックの出力を定義したり、関数を呼び出したりできます。前提条件を含めていない場合、ブロックは各タイムステップでアクションを実行します。

This shows the inside of a new Requirements Table block. It contains one blank requirement.

要件、前提条件、事後条件、およびアクションは複数作成できます。列と要件の管理には、[テーブル] タブで利用可能なオプションを使用します。また、要件のインデックスまたは列ヘッダーのセルを右クリックすると、コンテキストメニューから追加のオプションにアクセスできます。

[仮定] タブでは、システムの物理的な制約を定義する仮定も指定できます。要件への仮定の追加を参照してください。

形式的要件の式の作成

前提条件、事後条件、およびアクションは式を使用して定義します。前提条件と事後条件には論理式を使用し、アクションの定義には単一の等号 = を使用します。前提条件セルと事後条件セルのそれぞれの式は、スカラー logical として評価される必要があります。

式では、信号値、ワークスペース変数、定数値などの情報を "データ" を使用して管理します。式に数値や関数を含めることもできます。たとえば、前提条件 u >= 0 はデータ u が 0 以上であるかどうかをチェックし、アクション y = 0 はデータ y を 0 に設定します。

前提条件、事後条件、およびアクションを定義するには、要件セルで各式全体を明示的にリストするか、列ヘッダーで式の左辺をリストし、要件で式の右辺を定義します。[前提条件] 列および [事後条件] 列でヘッダーを使用する論理式を記述するには、目的の論理関係演算子を使用し、左側を空白のままにして目的の値を入力します。ヘッダーを使用するアクションを記述するには、セルにアクションの値を入力します。

たとえば、次のテーブルでは、1 つ目の事後条件はヘッダーでデータ y1 を指定し、2 つ目は要件セルで y2 を指定し、アクションは y3 を値のベクトルに設定しています。

This image shows a Requirements Table block that uses both header and non header syntaxes. The expressions evaluate the same content.

[前提条件] 列および [事後条件] 列で、スカラーヘッダーが単一の値、複数の値、または値の範囲と等しいかどうかをチェックすることもできます。次の構文を使用してチェックする値を指定します。

構文	説明
`value`	ヘッダーのデータが `value` と等しいかどうかをチェックします。
`value1,value2,value3,`...`,valueN`	ヘッダーのデータがいずれかのコンマ区切り値と等しいかどうかをチェックします。
`[value1,value2]`	ヘッダーのデータが `value1` 以上 `value2` 以下であるかどうかをチェックします。
`(value1,value2)`	ヘッダーのデータが `value1` よりも大きく `value2` よりも小さいかどうかをチェックします。
`[value1,value2)`	ヘッダーのデータが `value1` 以上で `value2` よりも小さいかどうかをチェックします。
`(value1,value2]`	ヘッダーのデータが `value1` よりも大きく `value2` 以下であるかどうかをチェックします。

次のテーブルでは、前提条件で u が 1、2、または 3 のいずれかと等しいかどうかをチェックしています。事後条件では、データ y1 と y2 について、表記法が異なる同じ論理式を使用して評価しています。1 つ目の事後条件では区間の表記法でヘッダーのデータを使用し、2 つ目の事後条件ではヘッダーのデータを使用せずに明示的な論理演算子を使用しています。

This image shows a requirements table that uses both header and non header syntaxes with interval notation. The expressions evaluate the same expression using different notation.

ヘッダーのデータを複数の区間について評価するには、それらを論理 OR 演算子を使用して組み合わせます。たとえば、[0.3, 0.5] || (0.1, 0.2) は有効です。区間では、実数に加え、境界を無限にして評価するために Inf も使用できます。Inf を含む区間には前後いずれかに小かっこが必要です。Inf を含む区間は、セルに含まれる区間が 1 つだけであれば簡略化できます。たとえば、(0.3, Inf) は > 0.3 と等価です。

ヘッダーのデータが式と等しくないことを指定するには、セルの値の左に ~= または ~ を入力して論理 NOT 演算子を使用します。この演算子は、単一値、コンマ区切り値、または区間に適用できます。たとえば、ヘッダーのデータ u が区間 [0.3, 0.5] の範囲外になることを指定するには、~[0.3, 0.5] または ~=[0.3, 0.5] と入力します。コンマ区切り値の場合は、~ のみを使用します。

要件セルに多くの内容が含まれる場合、セルのサイズによっては式全体が表示されない場合があります。すべての内容を表示するには、セルのサイズを調整するか、新しい行を追加します。新しい行を追加するには、最初の行を ... で終了し、Alt+Enter を押します。

`X` プレースホルダーの使用

ヘッダーに式を入力する場合、その列のセルでヘッダーの式を再利用しないでください。たとえば、ヘッダーにデータ u が格納されている場合、関連する列のセルでは u >= 0.5 && u <= 0.3 のような式は入力しないでください。代わりに、X をヘッダーのプレースホルダーとして使用します。たとえば、ヘッダーに u がある前提条件の式 X >= 0.5 && X <= 0.3 は、ヘッダーに u がない u >= 0.5 && u <= 0.3 と等価です。

This image shows a requirement with header data u and the placeholder X in the expression.

X プレースホルダーを使用すると、ヘッダーが長い場合の可読性が向上します。

前提条件と事後条件の配列データのチェック

前提条件と事後条件で配列データを使用する場合、ブロックはデータの各要素が論理式を満たすかどうかを確認し、logical 配列を生成します。前提条件または事後条件が値の配列を満たすかどうかを確認するには、関数 isequal や all など、評価結果がスカラー logical となる関数を使用します。たとえば、y1 が 1 行 4 列の配列である場合に、[1 2 3 4] と等しいかどうかを確認するには、isequal(y1,[1 2 3 4]) または all(y1 == [1 2 3 4]) をセルに入力します。

Requirements Table ブロックでの関数の使用

要件セルと列ヘッダーの Requirements Table ブロックで関数と演算子を使用できます。MATLAB^® で変数を使用するのと同様に、データを関数または演算子の引数として入力します。以下のテーブルでは、セル u1 + u2 == 2 とヘッダー u3 + u4 の下にあるセルはどちらも、2 つの入力データの合計が 2 に等しいかどうかを確認します。

This image shows a requirement that checks if the sum of the data is greater than 0 using the header and non-header notations.

Requirements Table ブロックは、グローバル変数または内部状態に書き込む関数を、ヘッダーではサポートしません。たとえば、ヘッダーでは関数 rand を使用できません。rand は数値を生成する度に内部状態に書き込むからです。

ブロックデータの定義

ブロックでデータを使用するには、それらを要件で入力し、[シンボル] ペインで定義する必要があります。[シンボル] ペインを開くには、Requirements Table ブロックを開きます。[モデル化] タブの [データの設計] セクションで [[シンボル] ペイン] をクリックします。

[シンボル] ペインでは、[タイプ] 列のアイコンでデータのスコープが示されます。データのスコープは [入力]、[出力]、[ローカル]、[定数]、または [パラメーター] に設定できます。名前、初期データ値、および端子番号も変更できます。その他のプロパティを変更するには、データの名前を右クリックし、[検査] を選択してプロパティインスペクターを開きます。詳細については、Requirements Table ブロックのデータの定義を参照してください。

This image shows the Symbols pane with the name of an input data u and an output data y, along with the data names, data types, and port numbers.

要件の編集時、Requirements Table ブロックにより未定義のデータが検出され、[シンボル] ペインで [未定義のシンボル] アイコンのマークが付けられます。未解決のデータがあると、コンパイル時にエラーの原因になることがあります。データを解決するには、[未定義のシンボルを解決] ボタンをクリックします。

モデルの動作の観察と生成

Requirements Table ブロックを使用してモデルの要件をチェックできます。モデルの動作を観察するか、モデルの動作と比較できる動作を生成します。

モデルの動作の観察

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

モデルを開く

Requirements Table ブロックを使用して、アクションは実行せずにモデルの動作を観察できます。モデルの動作が前提条件を満たさない場合、関連する事後条件はブロックでチェックされません。モデルの動作が要件の前提条件を満たし、事後条件を満たさない場合、Requirements Table ブロックは診断ビューアーに警告を出力します。Requirements Table ブロックを使用して要件を観察するには、前提条件を使用してモデルの入力動作を指定し、事後条件を使用してモデルの出力動作を指定します。モデルの入力と出力を区別するために、事後条件で指定したデータのプロパティインスペクターで [解析用の設計モデル出力として扱う] プロパティを有効にします。解析用の設計モデル出力として扱うを参照してください。

次のモデルには、2 つの入力を受け取って 2 つの値を出力する基本的なサブシステムをテストする Requirements Table ブロックが含まれています。Requirements Table ブロックは、前提条件と事後条件の論理定義を使用して、サブシステムの入力と出力が指定された要件を満たすかどうかをチェックします。

Requirements Table ブロックを開き、サブシステムの入力と出力に対して指定されている要件を確認します。要件では、サブシステムの入力ごとに、サブシステムの出力に対して論理的制約を指定しています。Requirements Table ブロックは、サブシステムの入力をデータ u1 と u2 で取得し、サブシステムの出力をデータ y1 と y2 で取得します。ブロックではデータを入力データとして定義しており、ブロックはサブシステムの信号をブロックの入力として取得できます。

モデルを実行すると、Requirements Table ブロックにより、Subsystem ブロックの入力が前提条件を満たすかどうかがチェックされます。前提条件が満たされると、Requirements Table ブロックにより、Subsystem ブロックの出力が事後条件を満たすかどうかがチェックされます。

この例の Subsystem ブロックは前提条件と事後条件を満たします。警告を生成するには、最初の要件の事後条件を y1 < 0 に設定し、再度シミュレーションを実行します。[診断ビューアー] には警告メッセージが表示されます。

モデルの動作の生成

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

モデルを開く

Requirements Table ブロックを使用して、モデルが対応する前提条件を満たす場合にアクションを実行することもできます。各要件のアクションは [アクション] 列を使用して指定します。

次のモデルには、2 つの入力を受け取って 2 つの出力を作成するサブシステムをテストする Requirements Table ブロックが含まれています。Requirements Table ブロックは、サブシステムの入力を受け取り、前提条件を満たす場合に値のセットを出力します。Requirements Table ブロックの各出力が、サブシステムからの出力のいずれかに対応します。サブシステムの出力が Requirements Table ブロックからの対応する出力信号と等しくない場合、Assertion ブロックはシミュレーションを停止してエラーを出力します。

Requirements Table ブロックを開き、サブシステムの入力に対して指定されている 2 つの要件を確認します。要件では、入力に対して論理的制約を指定しています。ブロックではデータ u1 と u2 を入力データとして定義しており、ブロックはサブシステムの入力をブロックの入力として取得できます。ブロックではデータ y1 と y2 を出力データとして定義しています。

モデルを実行すると、Requirements Table ブロックにより、Subsystem ブロックの入力が前提条件を満たすかどうかがチェックされ、出力信号が [アクション] 列で指定されている値に割り当てられます。その後、Subsystem ブロックからの出力が Requirements Table ブロックからの出力信号と比較されます。この例では、出力は等しくなり、アサーションにパスします。