ホーム > 情報処理安全確保支援士試験 > 2024年 春期
情報処理安全確保支援士試験 2024年 春期 午前2 問23
ソフトウェアの品質を確保するための検証に形式手法を用いる。このとき行う検証方法の説明として、適切なものはどれか。
ア：進行役 (モデレーター), 記録役などの役割を決めた複数人で, 成果物に欠陥がないかどうかを検証する。
イ：プログラムの内部構造とは無関係に, プログラムが仕様どおりに機能するかどうかを検証する。
ウ：プログラムの内部構造に着目し, プログラムが仕様どおりに動作するかどうかを検証する。
エ：明確で厳密な意味を定義することができる言語を用いてソフトウェアの仕様を記述して, 満たすべき性質と仕様とが整合しているかどうかを論理的に検証する。（正解）
解説
ソフトウェアの品質を確保するための検証に形式手法を用いる【午前2 解説】
要点まとめ
- 結論：形式手法は仕様を厳密な言語で記述し、論理的に整合性を検証する方法です。
- 根拠：形式手法は数学的・論理的な記述を用いて、仕様と満たすべき性質の整合性を証明します。
- 差がつくポイント：形式手法はプログラムの動作検証ではなく、仕様の正確性や一貫性を論理的に検証する点が特徴です。
正解の理由
選択肢エは「明確で厳密な意味を定義することができる言語を用いてソフトウェアの仕様を記述し、満たすべき性質と仕様の整合性を論理的に検証する」と述べています。これは形式手法の本質を正確に表現しており、仕様の誤りや矛盾を数学的に検証することでソフトウェアの品質を高める方法です。形式手法はプログラムの実装ではなく、仕様レベルでの検証に特化しています。
よくある誤解
形式手法はプログラムの動作をテストする手法ではなく、仕様の正確性を数学的に証明する技術です。動作検証やレビューとは異なります。
解法ステップ
- 問題文の「形式手法」をキーワードに注目する。
- 形式手法は「仕様の厳密な記述」と「論理的検証」が特徴であることを思い出す。
- 選択肢の説明を「仕様の記述方法」と「検証対象（仕様か実装か）」で比較する。
- 仕様の論理的整合性を検証する説明がある選択肢を選ぶ。
- それが選択肢エであることを確認する。
選択肢別の誤答解説
- ア：複数人で成果物の欠陥を検証するのは「レビュー」や「ウォークスルー」であり、形式手法ではない。
- イ：プログラムの外部仕様に基づく検証は「ブラックボックステスト」であり、形式手法とは異なる。
- ウ：プログラムの内部構造に着目するのは「ホワイトボックステスト」であり、形式手法の説明ではない。
- エ：仕様を厳密な言語で記述し、論理的に検証する形式手法の正しい説明。
補足コラム
形式手法はソフトウェアの安全性や信頼性が特に重要な分野（航空宇宙、医療機器、鉄道制御など）で活用されます。数学的証明により仕様の矛盾や欠陥を早期に発見できるため、後工程のコスト削減にも寄与します。ただし、導入コストや専門知識が必要なため、すべての開発に適用されるわけではありません。
FAQ
Q: 形式手法とテストの違いは何ですか？
A: 形式手法は仕様の論理的整合性を数学的に証明する方法で、テストは実装の動作を実際に確認する手法です。
A: 形式手法は仕様の論理的整合性を数学的に証明する方法で、テストは実装の動作を実際に確認する手法です。
Q: 形式手法で使われる言語にはどんなものがありますか？
A: Z言語、VDM、Bメソッドなどがあり、仕様を厳密に記述するための形式的記述言語です。
A: Z言語、VDM、Bメソッドなどがあり、仕様を厳密に記述するための形式的記述言語です。
関連キーワード: 形式手法, ソフトウェア検証, 仕様記述, ブラックボックステスト, ホワイトボックステスト, ソフトウェア品質保証