テスト入力と期待値の自動生成・形式手法

T-VEC Technologies

 

T-VECは形式手法を活用するモデルベースドテストツール。要件や設計をモデル化して、仕様上の矛盾・欠陥を検出(定理証明)。成果物としてMCDCを満たすテストケースを自動生成することにより、要件ベーステスト(Requirement Based Test)でコード内のエラーの不在証明とトレーサビリティを支援

 

要件ベーステストの自動化を支援

 
IEC 61508やISO 26262などのスタンダードに求められるプロセスを効率化するには、要件ベーステストの自動化が決定打であることや、その成果が要件トレーサビリティを支援することはあまり知られていない。
T-VEC のモデルベースドテストは、モデル化した仕様を定理証明した成果物としてテストベクタ(入力・期待値)を自動生成して、開発後工程の検証作業を削減できる。またモデルによる抽象化でテストの変更・構成管理も軽減されるので派生開発やSPLEにも有効。
 

モデル検査だけでは要件ベーステストによるランタイムなエラーの不在証明はカバーされない

 
近年 IEC 61508 、ISO 26262 などで形式手法(Formal Methods)の活用が推奨され、様々なツールが市場に出回るが、それらで仕様・設計の正しさを証明できても、コードが仕様・設計通りに動作することを検証するための、テストの生成・実行・解析作業から開放されるわけではない。
たとえコード自動生成ツールの正しさ、あるいはB2Bテストで設計とコードの一致性を証明しても、要件ベーステストによるランタイムなエラーの不在証明が必要なことは、航空業界の国際スタンダードDO-178B/Cでも明らかにされている。
 
従来の形式手法(フォーマルメソッド)やモデル検査ツールに比較して、T-VECが製品開発に実践的に用いられる理由は、要件・設計モデルの検証結果(定理証明)の成果物として自動生成されるテストベクタが、要件ベーステストとしてコードの一致性検証に活用できることです。 これはスタンダード認証に求められる要件トレーサビリティの取得・管理にも貢献します。
 

 

要件~テストのトレーサビリティを支援
IEC61508、ISO26262、DO178B/C 認証取得をサポートするモデルベースドテスト

 
定理証明の成果物として自動生成されるテストベクタは、要件ベーステスト(Requirement Based Test)の入力・期待値として、コード内のエラーの不在証明に用いられ、構造化カバレッジ(Structural Coverage)のMCDCレベルを満たし、トレーサビリティのエビデンスになる。
 

 

T-VECの優位点:

 
*フローティング、ダブル型にも対応(インテジャー、ブーリアンなどのみでは無い)
*リニア、ノンリニア式 に対応
*状態爆発しない(サブシステムごとに上流のコンストレインツを加味した入力で検証)
*入力・期待値を自動生成(要件ベーステスト、トレーサビリティを支援)
*要件、設計モデルの両方に対応
 
大規模な組込みシステムで実践的活用される形式手法、モデル検証ツール(モデル検査のみではない)
 

RAVE/TTM 要求仕様や設計を表でモデル化~テスト自動生成 

T-VEC 社 RAVE/TTMは、証明された手法を統合し、要求仕様や設計の欠陥防止および自動テストの為のツール。 T-VEC Tabular Modeler (TTM)は、要求仕様を表形式のGUI を用いてフォーマルにモデル化するフロントエンドツール。この要求のフォーマルモデルをテストベクタ生成システムでモデル検証(形式検証)し、要求仕様に基づいたテストベクタ生成、実行、結果判定を行う。
 
*T-VEC Tabular Modeler (TTM)  要求仕様を記述、管理、欠陥解析(表形式のモデルツール)
*テストベクタ生成(機能テストの為のテストケース)
*テストドライバー生成(テストベクタをテストスクリプトとしてテスト実行)
*レポート生成(モデル上の問題・欠陥、テスト結果解析、テストカバレッジなど)によるテスト進捗評価・確認
 
 

 

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

 

TTMモデリングは、テストエンジニアが対象コンポーネントの特定インターフェイスに対してテストを開発することと同等

 

テスト入力と期待値の自動生成と定理証明の原理

テスト入力と期待値の自動生成は、モデルベースドテストを実現可能にする技術であり、その最も初期の、そして最も重要なアプローチの1つがDNFメソッドである。仕様はDNF(Disjunctive Normal Form =加法標準形)に変換されて、各入力ドメインのパーティションは論理和集合の事前条件から形成される。論理和は論理的にANDされたブール値条件の集合である。テストケースはパーティションの各サブドメインから引き出される。[1]
 
T-VEC TTMは、デシジョンテーブルやステートマシン、制御システム、コードなどの表現に基づいて、要件、設計、アプリケーションの特性(安全性など)をモデル化するツールである。そして、TTMにモデル化された仕様を独自の階層的 Disjunctive Normal Form(DNF) に変換して、この形式に於ける各機能要求(入出力間の振舞い)の入力域に対するコンストレインツを Domain Conversion Path (DCP)として抽出する。このDCPに対してT-VEC VGS(Vector Generation System)は、上流の制約を受けて伝播されてくる入力範囲内で期待値との組合せを生成する。[2]
 
そしてテストベクタを生成できない DCP は,モデル上の矛盾・欠陥として検出される(定理証明、あるいはモデル検査)。
 
T-VEC VGS テストベクタ生成システムは、フロート,ダブルなど各種データ型や,リニア/ノンリニア式をサポートする。また入力の上下限の境界値や0などを優先的に選択するテストの達人の知見が組み込まれている。
 

モデルベースでテストを生成して実行する流れ

 
[1] Rob.Hierons. http://www.brunel.ac.uk/~csstrmh/research/test_z.html.
 
[2] Blackburn, M.R., R.D. Busser, Automatic Generation of Test Vectors for SCR-Style Specifications. Proceeding of the 12th Annual Conference on Computer Assurance, June, 1997. http://www.t-vec.com/download/papers/tvec_scr2tvec.pdf

各種資料

インターフェイス・ドリブンなモデルからのテスト自動生成

 
形式手法(フォーマルメソッド)を活用してテストベクタ、テストドライバーの自動生成をサポートできるアプローチを紹介。
 

 
 

C5-M輸送機開発における T-VEC TTM の成果をSTSC CrossTalk で公開

 
STSC CrossTalk (The Journal of Defence Software Engineering)の2009年2月の”Requirement Modeling for the C-5 Modernization Program©”で、T-VEC社 TTM要件モデリングツールを用いて、Lockheed Martin Aeronautics Company の C-5 Modernization (C-5M) 計画で達成された特筆すべき成果について
 

 

形式手法:モデルベース検証とテスト自動生成の資料

 

 
 

モデルベースドテスト 要件トレーサビリティを支援

 

 

間違いだらけの形式手法

 

テストは人手に頼らない

 

テストを容易にするモジュール構成

 
モデルベース開発を、小さな機能スレッドから始めて、その後に、チーム開発されるレベルに移行。また、一部では、プロダクトラインを展開
 

 

火星探査機の事故は T-VEC で回避できていた

 

 

ロッキードマーチン社 成功事例