ソフトウエアの品質，信頼性向上の手段として「形式手法（formal methods）」が注目を集めている。産業機器などに向けた国際安全規格「IEC 61508」や，自動車向けの同規格「ISO 26262」のドラフトに盛り込まれるなど，その名前が登場する頻度が増えている。しかし，その実像は日本でほとんど知られていない。形式手法は，英文で「methods」と複数形で表されることからも分かるように，本来，多様な手法の総称である。こうした幅の広さ，多様性を持った分野にもかかわらず，形式手法全体を俯瞰する文献は非常に少ない。現在は「形式手法が良いか悪いか」という大まかな議論ではなく，形式手法の中の各技術を個別に理解し，採用を検討すべき時期に来ている。そこで，同分野の研究に取り組む国立情報学研究所 教授の中島震氏に，形式手法の全体を俯瞰し，各技術の概要を解説してもらう。 （進藤　智則＝本誌）

中島　震
国立情報学研究所　総合研究大学院大学　科学技術振興機構SORST