HOME | products | T-VEC | 形式手法 仕様・設計をモデル検査・テスト自動生成

モデルベースドテスト
T-VEC TTMモデリング講座

TTM (T-VEC TABULAR MODELER)

TTMではシステムの入/出力間のリレーションシップを表形式にモデル化します。具体的には、振舞いの要件をデシジョンテーブル(コンディション・イベント)とステートマシンで定義します。プログラミング言語と同等の記述法を用いてモデル化できるので、実装担当者なら数日で学習できます。プログラムはシーケンシャルに実装しますが、表を用いて離散的に表現するといったイメージです。あるいはテスト仕様書に相当すると考えることもできます。
 

1:TTM モデリング概要

 
T-VEC Tabular Modeler (TTM)は、要求仕様・設計をモデル化して形式手法(フォーマルメソッド)を活用するためのツール。モデル化された仕様・設計に対して、形式手法を用いて欠陥の自動解析(モデル検査、定理証明)、テスト自動生成が、T-VEC Test Vector Generation System (VGS)を用いて行われます。TTM モデル言語は、米国海軍研究試験所(Naval Research Lab)にて開発された、SCR(Software Cost Reduction)を基にして開発された。
 

 

2:Max Positive

TTMを使って、max_positiveと呼ばれる仕様をモデル化。入出力インターフェイスの定義とアウトプットテーブルだけでモデリングできる簡単な題材を基に、形式手法によるテスト自動生成からコードに対する実行結果解析までT-VEC/TTMでできる全体像を紹介。
 

 

3:ATM

TTMを使って、銀行ATMの簡単な仕様をモデル化。 形式手法によるテストベクタ自動生成を介したモデル検査により、仕様間の矛盾や、レンジオーバーフローを検出できることを紹介。
 

 

4:Regulator

TTM のMode Machines テーブルを用いて簡単な状態遷移をモデル化します。 イベント式@T(式) や Guards Event(WHEN、WHERE、WHILE) を用いて状態遷移を定義します。
 

 

5:Vertical Tracker 1

要件トレーサビリティを支援するテストベクタ自動生成についての理解。
 

 

6:Vertical Tracker 2

再利用・共有の為のモデル構成に関して、以下を紹介。
 
· チーム開発で共有することを意図したモデル構築
· 振舞いの情報からインタフェースの定義を分離
· TTMモデルマネージャーを使用してモデルを再編集
· 再利用可能なテスト基盤となるモデルの構築
· プロジェクトで共通のスキーマ、オブジェクトマッピング、環境設定
· テストドライバ開発と生成を自動化
· 結果比較のために、テストベクタから期待値を抽出
· テストベクタをテストドライバ化して実装コードに実行
 

 

7:Vertical Tracker 3 

TTM に強化された、以下の拡張機能を紹介。
 
• Structures(構造体)サポート
• Functions テーブル
  パラメータで定義する振舞い(入力などに対してではなく)
• INTERM 変数(テンポラリなローカル変数)
  Function テーブルで活用
  例: INTERM_x = function(a, b, c)
• テストドライバジェネレータでCソースコード用のテストドライバを自動生成
• 期待値と結果出力を比較するテスト結果解析プログラムを実行
 

 

8: traffic_signal  

外部コントローラーからの入力に基づいて、約1秒間隔で状態を制御する交通信号機を例にして、時間に関するモデリング方法を2種類紹介。
 
Option 1: コンディションテーブルに明示的に状態を記述。
Option 2: Mode Machineを使用。