情報系の実稼働システムを対象とした形式手法適用実験報告書

  国民生活にとって、ソフトウェアおよびそれらが構成するシステムは、あらゆる業界のビジネスを進める基盤や社会インフラとして、なくてはならないものとなっています。同時に、システムの不具合が経済や国民生活に与える影響も大きくなり、 社会問題化する事例も増えています。

  このような背景から、IPA/SECでは、高信頼性ソフトウェア開発に有効な手法と言われている 「形式手法（*1）」に着目し、普及に向けた活動に取り組んでいます。しかし、実際の開発現場ではあまり普及が進んでおらず、形式手法の導入を検討する際に必要な情報が不足していることが、その要因の一つとしてあげられます。
  そこで、IPA/SECでは次の情報収集を目的とし、適用実験を行いました。

• どのように形式手法を利用するのか、またどのような効果があるか
• 形式手法には、どの程度の作業工数が必要か

  具体的な実験内容としては、株式会社東京証券取引所様のご協力のもと、実際に開発され運用されている情報システムの設計書を対象に、形式手法を適用した検査を行いました。

  その結果、従来は後工程で見つかっていた問題を、基本設計の段階で発見することができました。このことから、設計書の検査に形式手法を適用することで、「ソフトウェアやシステムの信頼性向上」、「問題の早期発見による開発コスト低減」の可能性を示すことができました。

  本報告書では、この実験結果に対する分析および考察、また実験で行った作業内容と工数に関する詳しい情報を掲載しています。ソフトウェア開発の現場において、形式手法の導入を検討するきっかけとなり、また導入する際の参考書として活用されることを期待します。


【脚注】
（*1）開発工程において、設計品質を向上させるための取り組みのひとつ。数学的な表現で仕様記述の曖昧性を排除し、数学的な証明技法により記述が正しいことを保証できる。

注：当ページのコンテンツはPDF形式での提供となっております。

・「情報系の実稼働システムを対象とした形式手法適用実験報告書」[1.05MB]

・「情報系の実稼働システムを対象とした形式手法適用実験報告書（別冊　詳細報告書）」[5.04MB]