形式手法　T-VEC Model-Driven Verification and Validation

Mark R. Blackburn, Ph.D.

　Air Force Research Labs (AFRL), National Science Foundation (NSF), Defense Research Project Agency (DARPA), NASA の主要研究者が参加する "Safe & Secure Systems & Software Symposium June, 2010" の講演スライド（日本語・ノート付き）を公開。　

実践的に活用できる形式手法（フォーマルメソッド）として評判

　・形式手法（フォーマルメソッド）を活用して仕様・設計モデルの正しさを証明
　・リニア・ノンリニアな解析にも対応する唯一の定理証明ツール
　・テストベクタを自動生成（フロートやダブルなどのデータ型の制約が無い）
　・数学的知識を必要としないで容易に取組める
　・モデルの再利用性により更なる工数の削減

画像クリックで日本語スライド（PDF）へ　　"インターフェイスドリブンなモデリングは開発しながら適応させることに飛躍的な効果が認められた。理想的にはテストエンジニア（モデラー）が開発者と共にインターフェイスを安定させて、要件を精練し、イテレーティブに反復して開発・テストできるようなモデルを作る。テストエンジニアはモデルを介して製品の要件（通常殆ど不完全なままの）を精練する、それは数百・数千行ものテストスクリプトを書く代わりに。そして形式手法を用いて仕様・設計モデルを定理証明し、テストベクタ（入力と期待値）・テストドライバーを自動生成。イテレーティブに反復される開発の中、コンポーネントの振舞い、インターフェイス、要件などが変更される場合、モデルは修正され、テストケースとドライバーが再生成され、再実行できる。このツールの特筆すべき優位性は、テストのプロセスが通常の開発と同時に行えること。Lockheed Martin 社など主な顧客は、50％以上テストの工数が削減できたことや、早期段階で要求仕様の解析（形式手法による定理証明）をすることで要件上の欠陥を排除し手戻り作業を飛躍的に軽減できたことを公言している"

原文はこちら
Ｔ－ＶＥＣ製品情報へ