Main Content

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

仕様モデルとは

設計モデルを要件に対して体系的に検証する場合、開発プロセスには各要件に対するテスト ケースの生成が含まれます。これらのテストは、量産コードの生成に使われる設計モデルを検証し、設計モデルが要件を満たすことについて信頼度を得るのに有用です。"仕様モデル" は、Simulink® Design Verifier™ 機能を活用することにより、要件に基づくテストを実行できる実行可能なエンティティです。

自然言語テキストで記述された一連の要件がある場合、Simulink を使用してそれらを形式的な (実行可能な) 仕様に変換できます。そうすることで、これらは "仕様モデル" となります。設計モデルとは異なり、仕様モデルで指定できるのは "実行すべき内容であり、実行方法ではありません"。これは、上位の要件を取得し、下位の詳細は非表示にします。

仕様モデルを使用する利点は、次のとおりです。

  • 体系的な方法で一連の要件を検証します。

  • 要件に基づくテストを自動化します。

  • 不足している要件、設計エラー、または要件における矛盾を特定し、開発段階の初期にモデルを設計する場合に役立ちます。

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

要件に基づくテストでは、仕様モデルから生成されたテスト ケースを使用して、要件に対して設計モデルを検証します。仕様モデルを使用した要件に基づくテストでは、次の手順に従います。

  1. 要件エディターで要件を作成する。設計対象のシステムの動作を説明する自然言語テキストで要件を記述します。

  2. 仕様モデルを作成する。仕様モデルを要件の実行可能な表現として設計します。このアクティビティにより、要件の絞り込みにつながる問題が明らかになる可能性があります。

  3. 要件をリンクする。個別の要件またはサブ要件を仕様モデルの部分にリンクします。

  4. 仕様モデルに対してテストを生成する。その要件への適合性を示すテストを要件ごとに少なくとも 1 つ生成します。

  5. テスト変換サブシステムを作成する。仕様モデルと設計モデルが同じ入出力インターフェイスを使用しない可能性があります。テスト変換システムを使用して、手順 4 で生成されたテスト ケースを変換します。

  6. 設計モデルを開発する。要件ドキュメントを使用して設計モデルを個別に開発します。要件を設計モデルにリンクします。

  7. 設計を検証し、カバレッジを解析する。手順 5 で生成されたテストを、手順 6 で開発された設計モデルで実行し、結果が仕様モデルおよび要件と一致するかどうか検証します。設計モデル カバレッジ レポートを生成し、未達カバレッジを特定して、必要に応じて要件を絞り込みます。

Specification Model Workflow

仕様モデルの作成

要件に基づくテストに対する仕様モデルの使用に示す自動操縦コントローラー モデルについて考えます。このデモで、要件は論理的開ループ条件と時間的開ループ条件で構成されます。

要件に対して仕様モデルを作成するには、次の手順に従います。

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

要件に関連する仕様モデルの入力信号と出力信号をリストします。対象の要件に関連しない信号は無視できます。

要件に基づく自動操縦コントローラーの入力信号は次のとおりです。

  1. 自動操縦の係合スイッチ: 自動操縦コントローラーを有効/無効にする

  2. 機首の係合スイッチ: 係合すると、HDG_HOLD_MODE が有効になる。そうでない場合、ROLL_HOLD_MODE はアクティブである

  3. ロール参照ターゲット回転ノブ: 目的のロール角の値を自動操縦コントローラーに送るダイヤル

  4. 機首参照回転ノブ: 機首方位モードの設定値を指定する

  5. 航空機ロール角: 航空機の現在の瞬時ロール角

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

  1. Aileron コマンド: 補助翼アクチュエータへの出力

  2. Roll Ref コマンド: 補助翼アクチュエータの設定値を示す表示ウィンドウの出力

信号値の上位レベルの表現を使用する

一部の信号は仕様の上位レベルで表現されます。仕様モデルの範囲など、上位レベルの表現を使用して信号を表現することが推奨されます。

入力信号の航空機ロール角について考えます。これは、航空機の現在のロール角を表し、-180 ~ +180 度の範囲で任意の値を取ります。

要件は、自動操縦コントローラーの動作をゾーンの観点で説明します。これらのゾーンは列挙型 Range を使用してモデル化されます。

これらの 5 つのゾーンを次の図に示します。

上位レベルの動作モードを特定する

要件は、次のように上位レベルの AP コントローラー モードと、それぞれのアクティブな条件を指定します。

自動操縦モード自動操縦の係合スイッチ機首の係合スイッチ
OFFオフDon't care
ROLL_HOLD_MODEオンオフ
HDG_HOLD_MODEオンオン

各要件の前提条件、効果、期待される出力を特定する

次の要件について考えます。

"コックピットの回転ノブのロール参照ターゲット回転ノブ (Roll_Ref_TK) が正常な範囲 ([-30, -3] 度または [+3, +30] 度) で指示している場合は常に、ロール参照 (Roll_Ref_Cmd) は Roll_Ref_TK に設定される。"

前提条件と影響を特定する-  上記の要件は 2 つの項で構成されます。

  1. 前提条件: Roll_Ref_TK は負の正常な範囲 [-30, -3] または正の正常な範囲 [+3, +30] のいずれかである。

    この前提条件は単純な論理 OR 演算子なので、真理値表を使用して論理前提条件を表します。

  2. 効果: Roll_Ref_CmdRoll_Ref_TK に設定します。効果の項は、想定される範囲の出力信号値を指定します。

要件の前提条件の項はアクティブになるタイミングを決定し、効果の項はアクティブになった後に実行する要件を決定します。

上記の要件は、Aileron コマンド Ail_Cmd 出力に影響しないため Range.All とみなされ、取り得るすべての一連の値を表します。

要件の真理値表を作成する

  • 要件の前提条件の項を真理値表の [条件テーブル] セクション、効果の項を [アクション テーブル] セクションにエンコードします。

  • 各要件を個別に追跡するには、ローカル変数 REQ_ID を対応する要件 ID 2.1 に設定します。

  • Simulink Design Verifier のオブジェクティブをステートメント sldv.test (REQ_ID==2.1) を使用して [アクション テーブル] に追加します。Simulink Design Verifier は REQ_ID 2.1 が満たされるとテストを検索します。

最終仕様モデル

上記のワークフローを使用して取得された最終仕様モデルは次のようになります。

参考