モデル検査ツールLTSAのメモ

モデル検査ツールLTSAについてのメモ。
LTSAについてのリンク一覧は、garyoさんのはてぶから辿ればいい。

はてなブックマーク - Junk☆Bookmark臥龍 - LTSA

【他の参考資料】
LTSAによる組み込みソフトウエアのモデリングと動作検証
→これが一番分かりやすい。
　LTSAというツールが状態遷移図のモデリングに大変有効である理由と例が説明されている。
　特に組込み機器のように、デッドロックや並行性、セマフォなどを考慮する必要がある時に役立ちそう。

LTSA Tutorial ― Yamamoto Lab. Web Site
→LTSAのツールの使い方が説明されている。分かりやすい。

Concurrency スライド
→LTSAの英語本を大学の講義録として公開されている。読みやすい。

LTSA - Labelled Transition System Analyser
→LTSAの総本山

LTSA Eclipse - Imperial College London
→EclipseのLTSA用プラグイン

LTSA 　FrontPage - PukiWiki

UMLモデリング・ツール「Enterprise Architect」からモデル検査ツール「LTSA」用のファイルを出力できるらしい。

モデル検査やAUTOSARなどに関連したツールが登場　――第11回 組込みシステム開発技術展（ESEC）レポート（2）｜Embedded and Electronics Engineers Network

eSOL - イーソル株式会社 : リサーチコンサルティング

形式手法(Formal Method)、モデル検査(Model Checking)の目的は、設計工程で仕様をモデル化して、その矛盾をなくす作業に使う。
過去に、野中さん、藤倉さん、佐原さんなどの講演をSEA関西で何度か聞いてきたから、雰囲気は分かるが、率直に言って、あまり役立つとは思っていなかった。
これらの手法は、仕様をモデル化するためにある種のプログラミング言語で実装するが、そのプログラムは動作しないし、実装プログラミング言語と同じぐらいの労力がかかる。
だから役立たないと思っていた。

でも、今の僕の課題として、設計工程の品質アップ、テスト設計の品質アップがある。
形式手法を使って、設計工程で状態遷移図のモデリング作業に使えるかもしれない。
形式手法で書いたモデルからJavaなどのソースを自動生成するよりも、テストケースを自動生成してくれる方が正直ありがたい。

形式手法は色んな種類があるけれど、LTSAはJavaで作られたGUIアプリがあり、状態遷移図を生成してくれるので、他の手法よりも分かりやすい。

システム設計の一番の肝は、状態遷移図だと思う。
業務は知っているがシステム化を知らないSEと、システム化できるSEの差は、状態遷移図でシステムを表現できる能力があるか否かだと思う。
フロー図やクラス図はあくまでもお絵かき。たくさんの漏れがある。
システム化する時に一番大事なのは、状態を見抜き、そのパターンを全て洗い出すことだ。
それが状態遷移図であり、デシジョンテーブルになる。
そしてそれが仕様になり、テストケースになる。

組込みSEならば、例えば、CDプレーヤーの状態遷移図は書けるだろうか？
情報処理試験に受かっているならば、缶ジュースの自動販売機の状態遷移図は書けるだろうか？
状態遷移図に出てくる状態は普通は、Cのグローバル変数として表現されるだろう。
だから、状態を扱うのは慎重でなければならない。

業務系SEならば、状態はDBにあるテーブルのフラグとして表現される。
画面遷移やトランザクションの推移によって、フラグの値が状態遷移図として表現される。

フラグの個数が増えるたびに、フラグの値が増えるたびに、状態遷移図はどんどん複雑になる。
フラグのビジネスルールは条件分岐で表現されるから、プログラムも複雑になっていく。

システム開発が難しいのは、状態遷移図が複雑になりやすく、状態爆発しやすいからだ。
状態が多いほど、テストケースも増えて、開発期間中に全てのフローを検証できないままリリースに至ってしまう。
だが、むしろもっと危険なのは、設計された状態遷移図で実装してみたら、たくさんの穴が見つかったという事態だろう。
特に組込系ならば、並列に走らせて特別なタイミングでデッドロックに至るバグなどは、手書きの状態遷移図では分かりえない。
オブジェクト指向やDOAも確かに役立つけれど、状態遷移図を補完するモデリング手法と捕らえた方が使いやすいと思う。

この10年、RailsやSeasar、Ajax、MapReduce、レコメンドエンジンなど、下流工程では多くの技術革新があった。
しかし、プロジェクト管理やモデリングに関しては、XPを代表とするアジャイル開発が多少あるぐらいで、10年前の技術と何ら変わっていないように思う。
その間、システム開発の大規模化、短納期化が進み、システム開発の難易度は10年前よりもはるかに上がっている。

おそらく今の日本では、人海戦術や組織力でこの流れに対抗しようとしているが、技術力を軽視していないだろうか？
プロジェクト管理やテスト管理を人海戦術による手作業からIT化したり、設計手法にDSLや形式手法を用いてソフトウェアでモデリングしていくなどの発想はないのだろうか？

ソフトウェア開発の諸問題はソフトウェアでしか解決できない範囲が広がっているのではないだろうか？