SEA関西プロセス分科会（モデル検査）

昨日はSEA関西プロセス分科会に参加してきた。出席者は30人ほど。講師はイーソルの藤倉俊幸氏。前半はアシスタントの方（？）が要求分析、FSP式の記述、LTSAによるモデル検査などを説明していたが、あまりにマニュアル棒読みなので少々酷い。LTSAを初めて見る人には、とても理解できるとは思えない説明だった。

後半は、藤倉氏による講演で、UMLを設計へ落とし込む方法、シーケンス図の曖昧性、タスクの設計技法、検査モデルの作成方法などの説明が行われた。さすがに経験豊富なコンサルの方だけに充実した内容で、参考になる点が多かった。LTSAの場合、ツールを使って状態遷移の様子を見れるため、SPINよりは手軽にモデル検査が出来るように思う。個人的にはEnterprise ArchitectのUML図面から一気にLTSAへ落とし込むツールの存在が気になった。これさえ有れば検証作業はもう少し楽に出来るかも知れない。LTSAについて書かれた書籍は多くないが、例えば下記の本は参考になる。書名は「組み込みソフトウェア」だが、モデルの検証は他の分野のソフト開発でも充分に応用可能。使い方はアイデア次第だ。

組み込みソフトウェアの設計&検証―割り込み動作からRTOSを使った設計、ツールによる動作検証まで (TECH 1「Embedded Software」)