三菱総合研究所、日立ソフトウェアエンジニアリング(日立ソフト)、NTTデータ、国立情報学研究所(NII)、北陸先端科学技術大学院大学は28日、経済産業省の「新世代情報セキュリティ研究開発事業」に基づき、ソフトウェアの開発現場においてソフトウェアの信頼性を論理的に検証する形式検証技術を導入するための実用化に関する共同研究を開始したと発表した。2011年度までの3カ年計画の予定。

現在ソフトウェアの開発現場では、テストデータを用いた不具合のチェックを行う方法による検証が行われているが、この方法では不具合を部分的に発見できるものの、論理的な信頼性を保証できないため高い信頼性を確保できなかったとしている。一方、ソフトウェアの信頼性を数学的な方法論によって証明する形式検証技術は、学術研究の分野では研究が進められているが、数理的な理論の理解などの困難性から、実際のソフトウェア開発現場への導入が進んでいなかったという。

同プロジェクトでは、実際の情報家電の組込みソフトウェアに対する形式検証技術の適用に関するケーススタディを実施するとともに、国内の形式検証技術の専門家およびソフトウェア技術者で構成する委員会を発足させ、形式検証技術の利用における組織管理的な障害と技術的な障害を取り除き、ソフトウェア開発現場への導入をスムーズに行うためのガイドラインを作成する。

また、業界団体等の協力を得てガイドラインを産業界に普及させることで、ソフトウェアの信頼性向上に寄与する先端技術の普及促進を目指すとしている。