Main Content

このページの翻訳は最新ではありません。ここをクリックして、英語の最新版を参照してください。

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

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

形式的要件の定義

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

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

This is the appearance of the Requirements Table block.

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

  • インデックス – 各要件の一意の識別子。この列は読み取り専用です。

  • 概要 – 要件のテキストベースの概要。この列のエントリはブロックの動作に影響しません。この列はオプションです。

  • 前提条件 – 残りの要件を評価するために指定の持続期間にわたって true でなければならない論理式。

  • 持続時間 – 残りの要件を評価するために前提条件が true でなければならない時間 (秒数)。この列はオプションです。空白のままにすると、持続時間は 0 になります。この列を使用するには、前提条件を指定する必要があります。[持続時間] 列の使用を参照してください。

  • 事後条件 – 関連付けられた前提条件が指定の持続時間にわたって true である場合に true でなければならない論理式。前提条件を含めていない場合、ブロックは各タイム ステップで事後条件をチェックします。

  • アクション – 関連付けられた前提条件が指定の持続時間にわたって true である場合にブロックで実行されるアクション。アクションを使用して、ブロックの出力を定義したり、関数を呼び出したりできます。前提条件を含めていない場合、ブロックは各タイム ステップでアクションを実行します。

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

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

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

形式的要件の式の作成

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

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

たとえば、次のテーブルでは、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 以下であるかどうかをチェックします。

次のテーブルでは、前提条件で u12、または 3 のいずれかと等しいかどうかをチェックしています。事後条件では、データ y1y2 について、表記法が異なる同じ論理式を使用して評価しています。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] と入力します。コンマ区切り値の場合は、~ のみを使用します。

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

ブロック データの定義

ブロックでデータを使用するには、それらを要件で入力し、[シンボル] ペインで定義する必要があります。[シンボル] ペインを開くには、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 ブロックは、サブシステムの入力をデータ u1u2 で取得し、サブシステムの出力をデータ y1y2 で取得します。ブロックではデータを入力データとして定義しており、ブロックはサブシステムの信号をブロックの入力として取得できます。

モデルを実行すると、Requirements Table ブロックにより、Subsystem ブロックの入力が前提条件を満たすかどうかがチェックされます。サブシステムの動作が要件を満たす場合、Requirements Table ブロックにより、Subsystem ブロックの出力が事後条件を満たすかどうかがチェックされます。モデルがすべての要件の両方の事後条件を満たす場合、シミュレーションが警告なしで実行されます。

モデルの動作の生成

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

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

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

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

不完全な要件セット、矛盾する要件セット、書き込み前の読み取りのエラーのトラブルシューティング

形式的要件では、前提条件、事後条件、およびアクションで使用されるデータがシミュレーションのタイム ステップごとに一意に定義されている必要があります。この原則に違反する可能性があるシナリオは 3 つあります。

  • 少なくとも 1 つのデータが定義されていないシナリオがブロックで実行される可能性がある場合、"不完全" な要件セットになります。

  • 要件セットで定義されている少なくとも 1 つのデータがシミュレーション時に複数の値と等しくなる可能性がある場合、"矛盾" した要件セットになります。

  • データを書き込み前に使用する要件を定義した場合、その要件セットで書き込み前の読み取りのエラーが発生する可能性があります。

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

参考

関連するトピック