T-VEC　モデル検証、テスト自動生成ツール

T-VEC

要件モデル（TTM）、Simulink/Stateflow のモデル検証、テスト入力と期待値を自動生成　形式手法

更新日 2010-02-16 | 作成日 2007-12-01

　 LinkIcon ＜T-VEC/TTM レンタル開始 19万8千円より＞

IEC61508、ISO26262 などから話題になっている形式手法ですが、ビジネスを前提に実践的に利用できるツールは殆どありません。T-VEC/TTMなら、要件を表形式で簡単にモデル化し、形式手法を用いて自動検査するだけでなく、テストベクタが自動生成される。そして最も時間の掛かる検証作業とトレーサビリティの自動化支援により、多くの開発工数が削減できるようになります。
Simulink/Stateflow対応版のレンタルもございます。

実践的に採用されるフォーマルメソッド（形式手法）、モデル検証ツール

IEC61508、ISO26262、DO178Bを一貫してサポート

モデル検査だけでは、コードの動的検証はカバーされません！

形式手法によるモデル検査とテストベクタ生成　近年IEC61508やISO26262でフォーマル検証が提案され、これに便乗する多くのフォーマルメソッドのツールが市場に氾濫しています。それら多くのツールはテストベクタを生成するわけではありませんので、コード自身の正しさを評価することは出来ません。モデルの正しさや、コード生成機能の正しさを謳えたとしても、コードが正しく動作することの保証にはなりませんので、それらのツールではテストケースと期待値の生成、実行、解析作業と言った作業から開放されるわけではありません。他のモデル検査ツール、フォーマルメソッドに比較して、T-VECが製品開発に実践的に用いられる理由は、モデルの検証結果からテストベクタが生成されることです。

モデル検証、テスト入力と期待値を自動生成、要求～テストのトレーサビィティ

要求仕様～テストまでのトレーサビリティ　T-VECはフォーマルメソッドを利用したモデルベース検証ツールです。要求モデル（TTM）やデザインモデル（Simulink/Stateflow）を解析しモデル上の欠陥を抽出。解析の結果得られる入力値と期待値をテストベクタとして、ソースやオブジェクトコードがモデルと一致しているか、コードに欠陥が無いかを検証出来ることが特徴です。他のフォーマルメソッド、モデル検査ツールに対するT-VECの優位点は、
＊フローティング、ダブルなどにも対応（インテジャー、ブーリアンなどのみでは無い）
＊リニア、ノンリニア式共に対応
＊サブシステムごとに上流のコンストレインツを加味した入力で検証（状態爆発しない）
＊検証結果の成果物として得られる入力値と期待値をテストベクタとして、ソースやオブジェクトコードがモデルと一致しているかの検証が出来る
＊要求モデル、デザインモデル（Simulink/Stateflow）の両方に対応している
以上の特徴をもって、大規模な組み込みシステムで実践的に採用されているモデル検証ツール（モデル検査のみではない）がT-VECです。 LinkIcon T-VEC カタログ

RAVE/TTM　要求仕様書をフォーマル化～自動テスト生成・実行

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

T-VEC 社 TTM 要求仕様モデリングツールについて pdf LinkIcon

Simulink Tester　Simulinkモデル～自動テスト生成・実行

　T-VEC Tester for Simulink は､ Simulink・Stateflow デザインモデル上の問題・欠陥を解析し、検証のための包括的なテストを生成します。

Simulinkモデルからテストベクタを生成　*複雑かつ大規模モデルから包括的なテストを体系的に生成
*MC/DC テストカバレッジ
*起こり得ないモデル上の欠陥を特定
*自動生成されるコードに対してのテストドライバーを生成
*テストシーケンスベクタ生成（ダイナミックなシステムの振舞いやフィードバックの検証）
*シミュレーション用 .ｍスクリプト生成（モデルの実証 model validation）
*モデル上の欠陥とその要素の関連付けを画面上のハイパーリンクで容易に
*リグレッションテストを自動化
*進捗確認・評価のためのステータス等のレポート表示
*ツールとしての承認（qualification ）対応
*TTM要求仕様モデルとの一致性の検証

フォーマルメソッドによるモデル検証要求からコードへのトレーサビリティ pdf LinkIcon

MATLAB EXPO 2007、2008講演資料

”フォーマルメソッドによるモデル検証、要求～のトレーサビリティ”　T-VEC Simulinkモデル検証を中心に、デモを交えて発表を行いました。

LinkIcon MATLAB EXPO 2007 講演スライド

プロダクトライン・ライフサイクルに於けるテストの自動化プロセスをテーマに、Ｓｉｍｕｌｉｎｋモデルベース開発の、プロダクトライン開発支援、モデル検証、テスト自動化、要件のトレーサビリティ・マトリクス（RTM）の各ツールを統合し、デモを交えて発表を行いました。

LinkIcon MATLAB EXPO 2008 講演スライド

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) 計画で達成された特筆すべき成果について公開されました。　　　 LinkIcon この論文に関するT-VEC社のサイトはこちら
画像クリックで日本語版

お勧めソフトウエアテスト関連記事のご紹介

　”航空機のソフトウエア技術に焦点を当てた特集記事”　 LinkIcon 日経エレクトロニクス2008年7月28日号　pp.41-74

”ソフトウエアの検証にモデルを使う、テストケース設計支援解説記事”　日経エレクトロニクス2008年4月21日号　pp.101-107

　モデル検証、フォーマルメソッド、テストベクタ自動生成、DO-178B、178Cガイドラインなど高信頼性システム向けのテスト手法、アプローチなど広範に解説されています。弊社で扱っている、T-VEC社、LDRA社などの事例も取り上げられています

T-VEC Wiki 日本語版を公開

　T-VEC wiki では、T-VECツールの情報、使用方法、その他関連情報を提供します。DO-178B、DO-178C、フォーマルメソッド、要件からテストまでのトレーサビリティ、要求モデル、デザインモデル、モデルチェッキング、MC/DCカバレッジ、モデルカバレッジ、テストベクタ、など高信頼性システムの V&V に関する幅広い情報を、T-VECツールの観点から紹介しています。
LinkIcon T-VEC Wiki へ

ロッキードマーチン社における成功事例

事例紹介ページへ

次期有人宇宙船（スペースシャトル） CEV で採用

　CEV (Project Orion)の主契約企業であるロッキードマーチン社は，このプロジェクトにT-VECのTTM要求仕様モデルとSimulinkのモデル検証機能をサブコントラクタも含めて採用することを表明している．

IEC61508、ISO26262、DO178B を一貫してサポート

　T-VECは要求モデル、Simulinkモデルを“Formal proof”し、各機能要求の取り得る入力範囲の境界値を評価するテストケースと期待値を生成し（more than Probabilistic testing)、その動的テストの結果はLDRAでカバレッジ解析（Dynamic analysis and testing) されます。また、LDRAによりソースコードは静的解析、複雑度解析(Static analysis, Software complexity metrics)することができます。