情報処理学会 第77回全国大会講演要旨

近年，ソフトウェアの高信頼化に向けた取り組みとして形式手法の適用が組込み系ソフトウェアを中心に広まっているが，エンタプライズ系システムに対しても形式手法を適用しようという動きがある。しかし，コスト対効果を考えると，検証の有効性を確保しつつ形式手法の適用にかかる工数を低減することが現実的な方策として望ましい。そこで，過去のプロジェクトにおける上流工程の成果物を題材として，検証対象をユースケースシナリオに絞り，VDM++を用いた検証実験を行った。本稿では，実験において検証に要した工期，検知した欠陥とその重要度を比較することにより，検証対象をユースケースシナリオに絞った場合の検証の有効性について述べる。