形式的手法の発祥の地,欧州では
「同手法についてよくある誤解」とのテーマが学会などで語られる。
一方,日本ではその存在すらほとんど認知されておらず
よくある誤解などが発生する以前の状態だ。
こうした中,国内でも先駆的に形式的手法を活用し成果を上げた企業がある。
研究者の興味の対象でしかなかった形式的手法が,いよいよ日本でも現場に広がり始めた。
仕様記述と形式検証(モデル検査)。
形式的手法を構成するぞれぞれの分野での最新事例を紹介する。

 形式的手法は,主に2つに大別される。1つは,ソフトウエアの仕様を「形式的な仕様記述言語」を使って論理的に記述したり,検査したりすることで,少しでも早い段階でバグを洗い出す「仕様記述」。もう1つは,形式的な仕様記述言語とは別の専用言語で記述したシステムの状態遷移をコンピュータに入力することで,振る舞いにバグがないかどうかを高速かつ自動的に探索する「形式検証(モデル検査)」である。いずれも形式的手法の一種ではあるものの,使いこなしの観点や利点はかなり趣を異にしている(表1)。

表1 形式的手法は2つに大別
[画像のクリックで拡大表示]

 形式的手法は1970年代に欧州で生まれ,企業内での実践もこれまでは欧州が中心だったが,最近では国内でも少数ながら成功事例が出始めている。手法の研究過程ではなく,日々,製品開発のプレッシャーにさらされ業務と向き合っている現場だからこそ生み出せた,形式的手法の使いこなしの術。難しいと思われがちな同手法を真摯しんしに学び,ソフトウエア開発の現場に導入した先駆的な事例を紹介する。

デバッグにモデル検査を使う,既存製品の未知のバグも発見
――メルコ・パワー・システムズ

 2005年8月。既に実機を使った出荷試験の段階まで開発が進んでいたメルコ・パワー・システムズの電力設備保全システム。変電所に設置され,落雷時などの事故データを記録する非常に重要な装置である。この装置のソフトウエアに,非常にまれではあるが計測したデータのログが保存できなくなる不具合があることが,試験の過程で判明した(図1)。

図1 出荷試験段階で原因不明の不具合発生
図1 出荷試験段階で原因不明の不具合発生
電力設備保全システムは,変電所において電流値を観測し,雷の事故データを記録する装置である。データ収集ドライバとデータ解析アプリケーションから成る。この装置の出荷試験段階で,非常にまれだが,データを保存できなくなる不具合が検出された。(図:メルコ・パワー・システムズ)