情報処理安全確保支援士試験 情報処理安全確保支援士試験 令和6年度春期 午前Ⅱ 問23: ソフトウェアの品質を確保するための検証に形式手法を用いる。このとき行う検証方法の説明として，適切なものはどれか。

問題本文

ソフトウェアの品質を確保するための検証に形式手法を用いる。このとき行う検証方法の説明として，適切なものはどれか。

選択肢

• ア.進行役（モデレーター），記録役などの役割を決めた複数人で，成果物に欠陥がないかどうかを検証する。
• イ.プログラムの内部構造とは無関係に，プログラムが仕様どおりに機能するかどうかを検証する。
• ウ.プログラムの内部構造に着目し，プログラムが仕様どおりに動作するかどうかを検証する。
• エ.明確で厳密な意味を定義することができる言語を用いてソフトウェアの仕様を記述して，満たすべき性質と仕様とが整合しているかどうかを論理的に検証する。

正解

エ. 明確で厳密な意味を定義することができる言語を用いてソフトウェアの仕様を記述して，満たすべき性質と仕様とが整合しているかどうかを論理的に検証する。

解説

形式手法は、意味を厳密に定義できる形式言語で仕様を記述し、満たすべき性質と仕様が論理的に整合するかを数学的・論理的に検証する技法。エが正しい。実務では曖昧さに起因する仕様の欠陥を実装前に排除でき、高い信頼性が求められるシステムの安全性証明に用いられる。テスト実行による検証(ブラックボックス/ホワイトボックス)やレビューとは性質が異なる。

選択肢ごとの解説

• ア.役割を決めた複数人で欠陥を探すのはインスペクション等の説明で、形式手法ではない。
• イ.内部構造に依らず機能を確認するのはブラックボックステストで、形式手法ではない。
• ウ.内部構造に着目して動作を確認するのはホワイトボックステストで、形式手法ではない。
• エ.厳密な言語で仕様を記述し性質との整合を論理的に検証する記述で形式手法として正しい。