ＭＲＩと経済産業省が形式手法の導入支援ガイドを開発
11 4/4
三菱総合研究所（ＭＲＩ）は、経済産業省の新世代情報セキュリティ研究開発事業として、ソフトの情報セキュリティ、安全性や信頼性を向上させるための技術である「形式手法（フォーマルメソッド）」に関する文書「フォーマルメソッド導入ガイダンス」を開発した。国内外の事例、各形式手法の特徴、費用対効果、現場への導入の手引きなどを解説しており、4月末頃に公開される予定だ。先般のみずほ銀行をはじめ、大きなシステムトラブルが目立つなか、経産省はガイドの公開により、高い安全性と生産性を両立する開発手法である形式手法の普及・定着を目指す。
形式手法は、数学的理論に基づいた言語を用いてシステムの設計や要求仕様が正しいかを検証する手法で、「Ｂメソッド」「ＳＰＩＮ」「ＶＤＭ」など複数の手法があり、適用領域は仕様の記述と検証に分かれている。
これにより、ソフトの品質が論理的に保証される。また、開発工程の早期に不具合を取り除くことで、その後の開発が効率化され、テスト工程の大幅削減と手戻りの防止によるコストの削減効果も見込める。
欧州では20年程前から形式手法の実践応用が進められ、欧米では鉄道や航空制御システムなどの高い安全性が求められる分野で普及している。一方、日本では学術的な研究が進んでいる段階で、導入事例も少なく、実案件で導入するための情報が整備されていなかった。
今回ＭＲＩは、形式手法を普及させるためのガイドラインを作成するプロジェクトを約２年半展開した。そのなかで、ブルーレイディスクの制御用ミドルウェアと入退室管理システムの２つの実開発案件に形式手法を採用し、事例としてまとめ、内閣官房、重要インフラや組込みシステムなどの業界団体、学会、ＭＲＩなどでセミナーを行うなどの普及活動も行ってきた。
ガイドラインには、手法やツールの使い方の紹介など技術情報に加えて、費用対効果やマネージメントの手法など、これまで形式手法の普及の障害となっていた点を解決するための有用な情報が掲載され、技術者と管理者に対して訴求する内容となっている。
関連リンク