令和6年度 春期 情報処理安全確保支援士 午前II 問23

各選択肢の解説

ア

進行役(モデレーター),記録役などの役割を決めた複数人で、成果物に欠陥がないかどうかを検証する。

誤りです。進行役（モデレーター）や記録役などの役割を決め、複数人で成果物の欠陥を探すのはインスペクションの説明です。人がレビューする手法であり、形式言語で仕様を記述して論理的に証明する形式手法とは異なります。

イ

プログラムの内部構造とは無関係に、プログラムが仕様どおりに機能するかどうかを検証する。

誤りです。内部構造とは関係なく、入力と出力から仕様どおりに機能するかを確かめるのはブラックボックステストです。テストケースを実行して確認する動的テストであり、仕様と性質の整合性を数学的・論理的に検証する形式手法ではありません。

ウ

プログラムの内部構造に着目し、プログラムが仕様どおりに動作するかどうかを検証する。

誤りです。内部構造に注目し、命令網羅や分岐網羅などの基準で仕様どおりに動くかを確かめるのはホワイトボックステストです。有限個のテストケースを実行する手法であり、形式的な仕様記述に基づいて論理的に検証する形式手法とは異なります。

エ

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

正しいです。形式手法では、VDMやZ、B、TLA+など、厳密な意味が定義された形式仕様記述言語で仕様を書きます。そのうえで、満たすべき性質と仕様が矛盾しないかを、定理証明やモデル検査などで数学的・論理的に検証します。