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

正解

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

正答率 42.9%（7人中 3人が正解）

問題の解説

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

選択肢ごとの解説

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