研究紹介シリーズ（第4回)
FMBoK (Formal Methods Body of Knowledge) に向けて（FMET） – 形式手法（フォーマルメソッド）の知識体系の構築プロジェクト
2006年6月に公表された経済産業省の「情報システムの信頼性向上に関するガイドライン」（注）や電気・電子関連機器の国際安全規格である「ISO／IEC 61508」で形式手法（フォーマルメソッド）が盛り込まれたことをきっかけに、ここ数年、形式手法への関心が高まってきている。しかし、形式手法と一言で言っても表記法、検証技術も複数あり、またこれらを使いこなすための知識体系もまだ十分に確立されているとはいえない。
こうした状況を鑑み、国立情報学研究所アーキテクチャ科学研究系の田口研治特任教授は、国際標準の確立も視野に入れながら、形式手法に関する知識の体系化に積極的に取り組んでいる。
■形式手法とは
アーキテクチャ科学研究系 田口研治特任教授
形式手法とは、ソフトウェアの品質と安全性の向上を目的としたプログラム開発手法（ツール）で、システムが正しく動作することを保証するためのものだ。とくに、仕様書を記述する際とモデル検査の際に重要な役割を果たす。
仕様書を自然言語や図形表現で記述してしまうと、どうしても内容が曖昧になりがちになる。また、仕様が正しいことを証明することもできない。しかし形式手法は数学的な理論をベースとしており、論理的な矛盾のない正しい仕様を作成することができる。
設計したモデルの検査に関しても同様だ。特に大規模で複雑なシステムの場合、想定し得る検査項目（ケース）は莫大となり、全てのケースを網羅することは困難だ。しかし、形式手法を使えば、レビューや100%の網羅性を持たないテスティングだけで検証するのとは異なり、設計したモデルを第三者でも論理的に検証することができる。特にツールによって自動的に検証できるので効率性も高い。
「実は海外ではかなり以前からロケットや飛行機、原子炉の制御といったミッションクリティカルなシステムにおいて形式手法が利用されてきました」
こう語るのは、形式手法の教育・研究を専門分野とする国立情報学研究所（以下、NII）アーキテクチャ科学研究系の田口研治特任教授だ。田口特任教授は、まだ知識体系が構築されていない形式手法の体系化に、国際標準の確立も視野に入れ取り組んでいる。
ミッションクリティカルなシステムの開発に不可欠な形式手法の知識体系の構築を目指す
田口特任教授が具体的に行っているのは、形式手法を学生やシステムエンジニアに教えるための整合性の取れた体系的なガイドラインの作成とカリキュラムの整備である。
現在、電気・電子関連機器の機能安全に関する安全度水準は、SIL（Safety Integrity Level）で4段階に区分されているが、ISO／IEC 61508では、SIL2以上で形式手法の利用を推奨している。また、IT製品のセキュリティの関する国際標準ISO／IEC 15408では、情報セキュリティの実現度を、EAL（Evolution Assurance Level：評価保証レベル）で表しており、EAL1〜7の7段階中、EAL5とEAL6で、形式手法の利用を推奨、EAL7では形式手法の利用を必須としている。日本においても、海外と取引がありミッションクリティカルなシステムを担当する企業や、パソコンや携帯電話の組み込みソフトを開発する企業にとって形式手法の利用は必須条件となっている。
「ISO／IEC 15408ではEAL5以上で形式手法を使うことになっています。ところが、仕様書の記述言語もモデルの検証技術も複数あり、知識体系も十分に確立されているとはいえません。ソフトウェア開発の現場では、熟練のシステムエンジニアが若手エンジニアに対して経験に基づき教えているというのが現状です。しかしそれでは、教えた内容が本当に正しいかどうか分かりません。また、どの程度まで教えれば十分かといった基準もありませんから、システムエンジニアの形式手法に対する知識やスキルを客観的に評価することもできません。」
田口特任教授は、現在形式手法が抱えている問題をこう指摘する。そして、問題を解決するにはまず形式手法の知識体系を構築する必要があると強調する。
形式手法の知識体系の国際標準化、資格認定試験の整備も視野に
田口特任教授が形式手法に対する問題意識を強く感じるようになったのは、「トップエスイープログラム」への参画がきっかけだ。同プログラムは、次世代ソフトウェア産業を牽引するスーパーアーキテクトを養成する講座で、文部科学省の支援の下、NIIを中心に産業界、他大学が数多く参画。実践的な教材の開発と産業界に貢献できる人材の育成に取り組んでいる。
「トップエスイープログラムでは、様々な講義が行われています。講義毎に学習目的が定められ、その目的に向かってどういう教材を利用し、どういうことを教えていくか、そして結果として学生の知識やスキルはどれくらい向上したのかなどを評価します。もちろん、形式手法に関する多くの講義が行われています。ところが形式手法は十分に確立された知識体系がないため、そもそも教えている内容自体が一定の要求レベルをクリアしているのかを評価することができないのです。そこで、自ら形式手法の知識体系の構築に着手することにしたのです」
手始めとして、田口特任教授は、2008年に形式手法に関する国際ワークショップ「FMET（Formal Methods Education and Training）」を北九州市にて開催。このワークショップでは形式手法の知識体系の構築方法や大学、産業界における教育方法などの議論が活発に行われた。今後、ワークショップでの議論を基に、形式手法の知識体系として「FMBoK（Formal Methods Body of Knowledge）」の国際標準化を目指す。
FMBoKの国際標準化に向けて 産業界のサポートを期待しています （田口特任教授）
また、形式手法の中のモデル検査に関する知識体系の構築にも取り組んでいる。
「現在、産業技術総合研究所（システム検証研究センター）、北陸先端科学技術大学院大学、企業と共同でプロジェクトを進めています。2009年には、『MCBOK（Model Checking Body of Knowledge）2008：ソフトウェア開発のためのモデル検査知識体系』をまとめました」
今後は、FMBoKの概念を広く発信していくことで社会的な認識の向上に努めると同時に、FMBoKの国際標準化に向けた活動も行っていく。2010年にはFMBoKの標準化に関するキックオフミーティングの開催を予定している。各種の情報処理技術者試験のように、FMBoKに関する資格認定試験の整備も視野に入れている。
形式手法の知識体系の構築は世界初の試みとなります。形式手法はミッションクリティカルなシステムはもちろん、今後、さらなるシステム化が進む自動車などあらゆる電気・電子関連機器の組み込みソフトを開発する上で重要な開発手法となります。是非ともセキュアなシステム開発に対して強い問題意識を持っている産業界の方に参加していただき、一緒に形式手法の知識体系の国際標準化を目指していきたいと思っています。
関連情報
情報システム供給者は、自然言語による要求仕様作成作業の誤りを極力排除し、ソフトウェア設計の一層の精度向上を図るため、形式手法（仕様記述言語による仕様記述とモデル検証）及びツール等の適用可能性及び効果等を評価の上、積極的に活用を検討することが望ましい。＜実施例＞設計段階において、特に高い水準の信頼性・安全性が求められる部分に対して形式手法を適用する。
（構成：山田久美）
