仕様モデルとは

R2022b 以降

モデルを要件に対して体系的に検証する際に、各要件に対するテストケースを生成します。これらのテストは、量産コードの生成に使用できるモデルを検証し、モデルが要件を満たすことについて信頼を高めることができます。要件を満たすテストを作成するには、"仕様モデル" を作成します。仕様モデルは、Simulink^® Design Verifier™ および Requirements Toolbox™ を使って要件に基づくテストを実行するために使用できる、実行可能なエンティティです。

自然言語テキストで記述された一連の要件がある場合、Requirements Table ブロックを使用してそれらを形式的要件として表すことができます。1 つ以上のブロックで要件を定義すると、ブロックと信号が仕様モデルになります。"設計モデル" と呼ばれているテスト対象のモデルとは異なり、仕様モデルで指定できるのは実行すべき内容であり、実行方法ではありません。

仕様モデルを使用して、以下ができます。

一連の要件を体系的かつ定量的な方法で検証する。
要件に基づくテストを自動化する。
設計モデルと要件を使用して問題を特定する。

要件に基づくテストでの仕様モデルの使用

仕様モデルを作成し、展開するには、次の手順に従います。

要件を作成する — 設計対象のシステムの動作を説明する要件を自然言語テキストで記述します。要件エディターで直接作成するか、インポートします。要件のインポートの詳細については、サードパーティ製アプリケーションからの要件のインポートを参照してください。
仕様モデルを作成する — 少なくとも 1 つの Requirements Table ブロックを使用して、要件の正式な表現として仕様モデルを設計します。
要件をリンクする — Requirements Table ブロックで要件を作成するたびに、要件エディターで等価な要件が作成されます。形式的要件のプロパティの構成を参照してください。上位レベルの要件を仕様モデルの形式的要件にリンクします。
形式的要件の完全性と一貫性を解析する — 不完全で整合性のない要件セットを手動で特定することは困難な場合があります。Requirements Table ブロックを使用すると、要件のこうした問題を自動的に解析できます。矛盾する形式的要件セットおよび不完全な形式的要件セットの特定を参照してください。
仕様モデルに対してテストを生成する — その要件への適合性を示すテストを要件ごとに少なくとも 1 つ生成します。テスト生成の詳細については、サブシステムのテストケースの生成 (Simulink Design Verifier)を参照してください。Simulink Design Verifier は、Requirements Table ブロックで定義された要件からテストオブジェクティブを自動的に作成します。
仕様モデルと設計モデルとのインターフェイスをとる — 仕様モデルと設計モデルは、多くの場合、同一の入力および出力信号を使用しません。両方のモデル間のインターフェイスを作成して、ステップ 5 で生成したテストケースを変換します。
設計モデルを作成する — 要件を使用して設計モデルを作成します。要件を設計モデルにリンクします。
設計を検証し、カバレッジを解析する — 手順 5 で生成したテストを設計モデルで実行し、結果が仕様モデルおよび要件と一致するかどうか検証します。カバレッジレポートを生成し、未達カバレッジを特定して、必要に応じて要件を絞り込みます。

次のフローチャートにこのプロセスを示しています。

This image shows the flowchart that illustrates the steps described in the previous list. The requirements are iteratively developed through the first four steps, and the design model and specification model are

仕様モデルの作成

要件に基づくテストに対する仕様モデルの使用に示す自動操縦コントローラーモデルについて考えます。この例では、出力を定義する論理条件と時相条件を含む要件を作成します。

仕様モデルインターフェイスの特定

テスト対象の要件に関連する仕様モデルの入力信号と出力信号をリストします。要件で指定されていない信号や、テストされた出力に影響しない信号は無視します。この例では、要件によって 5 つの入力と 2 つの出力が指定されます。仕様モデルの入力信号は次のとおりです。

自動操縦の係合スイッチ — 自動操縦コントローラーを有効または無効にするスイッチ
機首の係合スイッチ — 自動操縦スイッチがオンになっている場合に、自動操縦コントローラーのモードを指定するスイッチ
ロール参照ターゲット回転ノブ — 目的のロール角の値を自動操縦コントローラーに送るノブ
機首参照回転ノブ — 機首方位モードの設定値を指定するノブ
航空機ロール角 — 航空機の現在のロール角

出力信号は次のとおりです。

補助翼コマンド — 補助翼アクチュエータへの出力
ロール参照コマンド — 補助翼アクチュエータの設定値を示す、表示ウィンドウの出力

各要件の前提条件、事後条件、およびアクションの特定

検証が必要な要件について、テキストの要件を事前条件、事後条件、およびアクションとして表すことができる論理式に変換します。事前条件、事後条件、アクションを組み合わせて形式的要件を定義します。

前提条件 — 残りの要件を評価するために指定の持続期間にわたって true でなければならない条件
事後条件 — 関連付けられた前提条件が指定の持続時間にわたって true である場合に true でなければならない条件
アクション — 関連付けられた前提条件が指定の持続時間にわたって true である場合に実行しなければならない動作

一部の要件では事後条件またはアクションを交互に使用することができ、あるいは事後条件とアクションの両方を使用できる場合もあります。設計モデルの構成に基づいて、どちらを使用するかを指定します。

たとえば、自動操縦コントローラーのモードを指定する、上位レベルの要件について考えてみましょう。

自動操縦コントローラーモードは次によって決まります。

自動操縦の係合スイッチがオフの場合、自動操縦コントローラーは OFF です。
自動操縦の係合スイッチがオンで、機首の係合スイッチがオフの場合、自動操縦コントローラーは ROLL_HOLD_MODE です。
自動操縦の係合スイッチと機首の係合スイッチの両方がオンの場合、自動操縦コントローラーは HDG_HOLD_MODE です。

これらの要件は、次の論理式で記述できます。

要件	前提条件	アクション
`1`	`AP_Engage_Switch == false`	`Mode = Off`
`2`	`AP_Engage_Switch == true && HDG_Engage_Switch == false`	`Mode = ROLL_HOLD_MODE`
`3`	`AP_Eng_Switch == true && HDG_Engage_Switch == true`	`Mode = HDG_Hold_Mode`

残りの要件に対してこの処理を繰り返します。

要件内の設計値の表現を特定

要件は、設計モデルが満たさなければならない値の範囲を指定する場合があります。あるいは、各要件内で評価する値をパラメーター化する必要がある場合があります。これらの値は、必ずしもリテラル値で簡単に記述できるとは限りません。Requirements Table ブロックを使用すると、式内の値を定数またはパラメーターデータとして表すことができます。Requirements Table ブロックのデータの定義を参照してください。データはシミュレーション全体を通じて変更できます。数値をデータに割り当てるだけでなく、ブロックは文字列、列挙、範囲といった他のデータ型をサポートします。要件に合った値の表現を使用してください。

自動操縦コントローラーモデルでは、航空機のロール角のしきい値を要件で指定します。次のグラフィックスは、しきい値を等価の数値と言語で示しています。

This image shows the roll angle values and ranges that correspond to the high-level representation of the design values.

Requirements Table ブロックの作成

形式的要件で使用する信号の表現、値、および式を特定したら、各要件の [前提条件]、[事後条件]、および [アクション] 列にそれぞれ事前条件、事後条件、およびアクションの論理式を記述します。要件に子または依存関係がある場合、それらの関係をブロックに含めることができます。Requirements Table ブロックの階層の確立を参照してください。

Requirements Table ブロックで要件を作成するたびに、要件エディターで等価な要件が作成されます。エディターでは、要件の追加のテキストプロパティ (説明など) を更新します。形式的要件のプロパティの構成を参照してください。

自動操縦コントローラーモデルでは、仕様モデルに 2 つの Requirements Table ブロックが含まれています。AP_Mode_Determination は、自動操縦コントローラーモードの形式的要件を定義します。

This image shows the requirements for the autopilot controller mode. It contains three requirements that are derived from the plain text requirements in the example model.

他の Requirements Table ブロック Cmd_Determination は、補助翼コマンドとロール参照コマンドの目的の出力を記述します。

This image shows the requirements for the autopilot commands. It contains requirements that are derived from the plain text requirements in the example model.

最終仕様モデル

Requirements Table ブロックを入力、出力、および互いに接続すると、最終的な仕様モデルは次のようになります。

This image shows the final specification model.

テスト生成のための仕様モデルの準備

Simulink Design Verifier は、Requirements Table ブロックで定義された要件からテストオブジェクティブを自動的に作成します。テストオブジェクティブの値を制約する必要がある場合は、信号ソースに指定するか、ブロックの [仮定] テーブルに含めることで指定できます。要件への仮定の追加を参照してください。テスト生成用の仕様モデルを準備するには、モデルカバレッジオブジェクティブを設定します。[Design Verifier] タブの [準備] セクションで、[テスト生成設定] をクリックします。[コンフィギュレーションパラメーター] ウィンドウで、[Design Verifier] リストを展開し、[テスト生成] をクリックします。[モデルカバレッジオブジェクティブ] を、目的のカバレッジを最も適切に取得するオプションに設定します。