三菱総合研究所などが形式手法の実用化へ共同研究を開始
08 11/3
三菱総合研究所、日立ソフトウェアエンジニアリング、ＮＴＴデータ、国立情報学研究所、北陸先端科学技術大学院大学は、ソフトウェアの開発現場にソフトウェアの信頼性を論理的に検証する形式検証技術（形式手法＝フォーマルメソッド）を導入し、実用化するための共同研究を開始した。現在ソフトウェアの検証作業は、テストデータを用いて不具合のチェックを行う方法で行われているが、人力に依存するため信頼性に限界がある。形式手法は理論的に安全性を証明できるため、特に高信頼性が求められる組込みソフト開発における安全対策として普及が期待されている。
ソフト開発の現場では、開発するコード数の増加に伴って各作業の効率化が求められている。検証の場面でも、現在の手法では不具合を部分的に発見できても論理的に信頼性を保証できないため、信頼性を高めることができないという問題を抱えている。
形式検証技術は、ソフトウェアの信頼性を専用の形式仕様記述言語を用い、数学的な方法論によって証明するという手法で、アカデミック分野では研究が進められているものの、理論の難しさから一般には普及に至らず、ようやく自動車などの組込みソフト開発への適用が模索されているという段階にある。
形式手法は大きく「モデル検査」と「演繹（えき）推論」に分れるが、今回採用するのは「モデル検査」で、同手法は検証作業を自動で行う方式のため、検証作業の知識がなくても導入しやすいという特徴がある。ちなみに後者は、ＣＳＫシステムズやキャッツなどがサービスを提供している。
同プロジェクトは、経済産業省の「新世代情報セキュリティ研究開発事業」の一環として3年間実施する。情報家電の組込みソフトに対する形式検証技術の適用に関するケーススタディを行い、効果や適用する場面などを具体的に示す。
さらに、国内の形式検証技術の専門家およびソフト技術者で構成する委員会を立ち上げ、形式検証技術の利用における組織管理的な障害と技術的な障害を取り除き、ソフト開発現場への導入をスムーズに行うためのガイドラインを作成する。
これらの形式手法は、組込みソフト開発だけでなく、エンタープライズ系の開発にも適用可能となる。開発したガイドラインは、業界団体などを通じて産業界に普及させる予定だ。
関連サイト