Modeling

提供: T-VEC Wiki
移動: 案内検索

たくさんの種類のモデルやモデリング表記法があります。T-VECツールが提供するのは、要求モデル(Requirement Models)、デザインモデル(Design Models)、そしてハイブリッドモデル(Hybrid Models)です。

モデルの種類

図のように、TTMは、要求モデルを定義するための、構造や専用言語を提供します。Simulink/Stateflowは、デザインモデルを定義するための、構造や専用言語を提供します。TTMやT-VEC Simulink Tester(SL2TVEC)でサポートされるアサーションメカニズムでは、プロパティ(安全、セキュリティ)を定義するための、言語や仕組みを提供します。

Model Spectrum

High Level Representation

TTMとsl2tvec両方のトランスレータは、T-VECサブシステムを構成するT-VECプロジェクトと呼ばれるhigh-level representationに、モデルを変換します。サブシステム言語は、T-VEC標準形式で、テキスト形式(ASCII)の言語です。簡単に言うと、各サブシステムは、1つ以上のFunctional Relationships(FRs)を持ち、これは、1つ以上のDisjunctions (constraints)を伴います。ビルド工程の間、T-VECコンパイラは、この言語をlow-level representationに変換します。このレベルにおけるT-VECサブシステムは、TTMの構造物(例えば、condition tablesなど)やSimulinkサブシステムのモデリング構成から得られたものです。

T-VEC標準言語は、従来の論理演算(AND,OR)やリレーショナル演算子(>,=,<)に加え、あらゆるアプリケーションドメインをサポートする、機能的振る舞いを指定するための数学的演算子(三角法、intrinsic、積分、量子化、マトリクス)のサポートも提供します。サブシステムは、上位層から下位層(ユーティリティと呼ばれる)への参照があるような、階層構造を持つこともできます。サブシステム参照のための、呼び出し構文も持っています。(例:output = function(input1, ..., inputN))

Low Level Representation

lowest-level representationには、プレディケイトの論理積(AND)である Domain Convergence Paths (DCPs) (それぞれのDCPは、Functional Relationship(FR)(それ自体もプレディケイトとして扱われる)を伴う)があります。higher-level representationのサブシステム内部では、DCPの組合せが、グループを成します。 1つのDCPは、単純な事前条件(precondition)/事後条件(postcondition)の関係ですが、複雑な関係を表現することもできます。これにより、Test Sequence Vectors を生成するようなことも出来ます。

ツールの流れ

test vector generator は、テストベクタ生成過程において、各階層内のレベルでDCPごとの model checking を実行します。そして、T-VEC VGSは、defects のレポートを生成します。モデル上の欠陥の簡単な例は、以下のような論理的矛盾です。

(x > 0) & (x < 0)

(x > 0) & (x < 0) は、DCP詳述です。階層的に構成されるサブシステムのモデルチェックは、上下のサブシステム間(grandparentとchild)の、機能、あるいはコンストレインツの、充足の確認が伴われます。例えば図にあるように、上位から下位に至るDCP内に、x > 0 というコンストレインツが存在する場合、少なくとも1つの上位から下位に至るDCPはx > 0 を充足される必要が有ります。上位サブシステムで、そのようなコンストレインツが満たされない場合、そのDCPの入力は空(i.e., null)であり、テスト入力が選択されなくなります。これが model defect です。カバレッジレポートは、TTMやSimulinkモデルにサブシステム標準形式を介して、DCPの不具合の詳細なエラーレポートにリンクします。

もしDCPsにエラーがなければ、VGSは、副産物としてテストベクタを生成します。そして、test driver generator と統合され、あらゆる言語・実行環境用に、テストドライバを生成し、その実行と結果の解析まで、自動化します。