前回までは，組み込みソフトウエア向けの検証手法について概観した。今回はその中でも特に最近注目を浴びている形式検証の1つ，モデル検査について解説する。連載を担当する筆者のキャッツと福岡知的クラスター研究所が開発したツールを軸に語ってもらう。（進藤　智則＝本誌）

穴田　啓樹
キャッツ 中部事業所　技術マネージャ
松本　充広
福岡知的クラスター研究所　研究員

　前回までは，レビューやテストなど組み込みソフトウエアの検証手法について，動的/静的といった軸から概要を述べた。今回と次回は，これら検証手法の中でも最近注目が集まっているモデル検査の基本について解説するとともに，我々が開発しているモデル検査ツール「Garakabu」の概要とその使い方を説明する。