ソフトウェアが、情報システムのみならず、自動車、航空機、情報家電、インフラ制御等の身の周りの様々なものに深く浸透するに伴い、ソフトウェアの不具合に起因する事故・障害等による損害が増えています。このような背景のもと、ソフトウェアの正しさを論理的に検証し、その安全性や信頼性を確保するための方法として、形式手法に注目が集まっています。形式手法は、欧米では産業応用が進みつつありますが、国内では、一部の開発現場における適用にとどまり、開発現場への普及が進んでいません。
開発現場に普及しない理由として、形式手法の適用において必要となるモデリングやモデルの抽象化などに関する実践的な方法論が整備されていないことや、導入コストと効果の関係など意思決定者に必要な情報が見えていないことなどが挙げられます。
株式会社三菱総合研究所、日立ソリューションズ、株式会社ＮＴＴデータ、国立情報学研究所、北陸先端科学技術大学院大学は、2008年10月から、経済産業省の「新世代情報セキュリティ研究開発事業」により、形式手法の普及を妨げる問題を解決するために、情報家電等の実システムに対する形式手法適用のケーススタディを実施し、開発現場に形式手法を普及促進させるためのガイダンスの作成を開始しました。
上記ガイダンスにおいては、費用対効果についての考え方や、組織等において適用する際の体制や方針策定に関する情報をまとめています。これらの情報を世の中に広く公開するとともに、さらに最新のニュース、実際の手法紹介や事例紹介といった形式手法に関する総合的な情報集約・共有の場を提供するため、形式手法実践ポータルサイトを開設致します。皆さまからのご意見、ご要望をお聞かせいただきながら、幅広い内容に渡る情報提供を進めて参ります。