今回はキャッツと福岡知的クラスター研究所，九州大学の3者が共同開発したモデル検査ツール「Garakabu」の使いこなし方について解説する。前回取り上げた「センサ・スイッチ」システムやカー・ステレオなどの例題を基に，検証できる性質を説明する。（進藤 智則＝本誌）

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

　前回は，形式的手法（フォーマル・メソッド）の一種であるモデル検査の概要と原理について簡単に述べた。今回は筆者らが独自開発した状態遷移表ベースのモデル検査ツール「Garakabu」を取り上げ，使い方や検証できる性質などについて例題を挙げて解説する。