令和6年度 春期 情報処理安全確保支援士試験 午前Ⅱ 問23
テクノロジ／開発技術ソフトウェアの品質を確保するための検証に形式手法を用いる。このとき行う検証方法の説明として，適切なものはどれか。
出典：令和6年度 春期 情報処理安全確保支援士試験 午前Ⅱ 問23
- ア進行役（モデレーター），記録役などの役割を決めた複数人で，成果物に欠陥がないかどうかを検証する。
- イプログラムの内部構造とは無関係に，プログラムが仕様どおりに機能するかどうかを検証する。
- ウプログラムの内部構造に着目し，プログラムが仕様どおりに動作するかどうかを検証する。
- エ明確で厳密な意味を定義することができる言語を用いてソフトウェアの仕様を記述して，満たすべき性質と仕様とが整合しているかどうかを論理的に検証する。
正解：エ
解説
形式手法（フォーマルメソッド）を用いた検証では，曖昧さのない厳密な意味（形式的意味論）を定義できる形式言語を用いてソフトウェアの仕様を数学的に記述し，その仕様が満たすべき性質（要求事項）と整合しているかどうかを論理的・数学的に検証します。これにより，レビューやテストでは発見しにくい仕様上の矛盾や欠陥を網羅的に検出できる可能性があります。
選択肢ごとの解説
- ア誤り。進行役や記録役などの役割を決めて複数人で欠陥を検証する手法はインスペクションの説明であり，形式手法ではありません。
- イ誤り。プログラムの内部構造とは無関係に仕様どおりに機能するかを検証する手法はブラックボックステストの説明であり，形式手法ではありません。
- ウ誤り。プログラムの内部構造に着目して動作を検証する手法はホワイトボックステストの説明であり，形式手法ではありません。
- エ正しい。明確で厳密な意味を定義できる言語を用いて仕様を記述し，満たすべき性質と仕様との整合性を論理的に検証するのが形式手法です。