第5回：国内でも成功事例が出現，形式的手法の壁は高くない形式的手法の発祥の地，欧州では 「同手法についてよくある誤解」とのテーマが学会などで語られる。 一方，日本ではその存在すらほとんど認知されておらず よくある誤解などが発生する以前の状態だ。 こうした中，国内でも先駆的に形式的手法を活用し成果を上げた企業がある。 研究者の興味の対象でしかなかった形式的手法が，いよいよ日本でも現場に広がり始めた。 仕様記述と形式検証（モデル検査）。 形式的手法を構成するぞれぞれの分野での最新事例を紹介する。 形式的手法は，主に2つに大別される。1つは，ソフトウエアの仕様を「形式的な仕様記述言語」を使って論理的に記述したり，検査したりすることで，少しでも早い段階でバグを洗い出す「仕様記述」。もう1つは，形式的な仕様記述言語とは別の専用言語で記述したシステムの状態遷移をコンピュータに入力することで，振る舞いにバグがないかどうかを高速かつ自動的に探索する「形式検証（
