形式手法 定理証明 と テストベクタ生成 T-VEC Tabular Modeler

　T-VEC Tabular Modeler (TTM) トレーニングコースで提供される題材を基に、使用方法や機能などを解説するチュートリアルの連載を開始しました。

１：TTMモデリングツールについて

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

続きを読む　TTM モデリングツールについて

2：Max Positive

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

続きを読む　Max Positive

３：ATM

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

続きを読む　ATM

４：Regulator


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



続きを読む　Regulator

５：Vertical Tracker 1


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


続きを読む　Vertical Tracker 1

６：Vertical Tracker ２

モデルの各種要素を再利用
　再利用・共有の為のモデル構成に関して、以下を紹介。

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

続きを読む　Vertical Tracker ２

7：Vertical Tracker 3

　TTM に強化された、以下の拡張機能を紹介。

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


続きを読む　Vertical Tracker 3

今後の予定

· traffic_signal　
· tracking_avoidance　　
· sudoku3　

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

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

実践活用される形式手法の各種資料は、こちらから