形式手法　T-VEC　モデル検証、テスト自動生成ツール　実践的に活用できるフォーマルメソッド

IEC61508、ISO26262、DO178B/C 認証取得をサポート

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

形式手法によるモデル検査とテストベクタ自動生成
　近年 IEC 61508 や ISO 26262 で形式手法（フォーマルメソッド）が提案され、これに便乗する多くの形式検証ツールや、それに関わるセミナーなどが市場に出回っています。それらツールで仕様・設計の正しさや、仕様・設計モデルからのコード生成の正しさを謳えたとしても、コードがターゲットで正しく動作することの証明にはならないので、テストケースの生成、実行、解析などの作業から開放されるわけではありません。

また要件トレーサビリティの必要性が言及されるようになりましたが、これには要求仕様や設計に基づいたテストケースが欠かせません。しかしながらこれを人手に頼り多くの工数を費やすことになるのは周知のとおりです。

要求仕様～テストまでのトレーサビリティ
　T-VECは形式手法（フォーマルメソッド）を活用するモデルベース検証ツールです。要求仕様や設計モデルを解析し欠陥を抽出（定理証明）。解析の結果得られる入力値と期待値をテストベクタとして、ソースやオブジェクトコードがモデルと一致しているか、コードに欠陥が無いかを検証出来ることが特徴です。


他の形式手法（フォーマルメソッド）、モデル検査ツールに対するT-VECの優位点は、

＊フローティング、ダブルなどにも対応（インテジャー、ブーリアンなどのみでは無い）
＊リニア、ノンリニア式 に対応
＊サブシステムごとに上流のコンストレインツを加味した入力で検証（状態爆発しない）
＊検証結果の成果物として得られる入力値と期待値をテストベクタとして、 ソースやオブジェクトコードがモデルと一致しているかの検証が出来る
＊要求モデル、設計モデルの両方に対応している

以上の特徴をもって、大規模な組み込みシステムで実践的に採用されている形式手法、モデル検証ツール（モデル検査のみではない）がT-VECです。

T-VEC カタログ

TTM 表形式で要求仕様をモデリング
　T-VEC 社　RAVE/TTMは、証明された手法を統合し、要求仕様や設計の欠陥防止および自動テストの為のツールです。　T-VEC Tabular Modeler (TTM)は、要求仕様を表形式のGUI を用いてフォーマルにモデル化するフロントエンドツールです。この要求のフォーマルモデルをテストベクタ生成システムでモデル検証（形式検証）し、要求仕様に基づいたテストベクタ生成、実行、結果判定を行います。

*T-VEC Tabular Modeler (TTM) 　要求仕様を記述、管理、欠陥解析（表形式のモデルツール）
*テストベクタ生成（機能テストの為のテストケース）
*テストドライバー生成（テストベクタをテストスクリプトとしてテスト実行）
* レポート生成（モデル上の問題・欠陥、テスト結果解析、テストカバレッジなど）によるテスト進捗評価・確認

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

　T-VEC Tester for Simulink は､ Simulink・Stateflow デザインモデル上の問題・欠陥を解析（形式手法による定理証明、あるいは形式検証）し、検証のための包括的なテストを生成します。

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

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

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

ノンリニアにも対応できる唯一の形式手法（フォーマルメソッド）

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

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

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

間違いだらけの形式手法

間違いだらけの MDD、形式手法、ソフトウエアプロダクトライン開発

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) 計画で達成された特筆すべき成果について公開されました。　

資料はこちらから

　Simulink モデルベース開発の派生開発を支援するプロダクトライン開発・モデル検査・テスト自動生成ツールの統合
　＜キーワード：　派生開発、プロダクトライン開発 (SPLE)、フォーマルメソッド（形式手法）、テストベクタ自動生成、モデル検証（Model Based Verification）、要件からテストへのトレーサビリティ・マトリクス＞

Simulink/派生開発を支援するSPLE・モデル検査・テスト自動生成

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

MATLAB EXPO 2008 講演スライド

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

MATLAB EXPO 2007 講演スライド