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

選択肢

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

正解と解説

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

形式手法は、数学的に意味が厳密に定まる言語で仕様を記述し、その仕様が満たすべき性質と矛盾しないことを論理的に証明したりモデル検査で網羅的に確認したりする方法である。テストのように入力例を試すのではなく、記述された範囲について網羅的に正しさを示せる点が特徴で、安全性が強く求められる分野で用いられる。一方で記述と検証の負荷が大きいため、適用範囲を絞る運用が一般的である。

選択肢ごとの解説

• ア役割を決めて実施する公式なレビュー（インスペクション）の説明である。
• イブラックボックステストの説明であり、形式手法ではない。
• ウホワイトボックステストの説明であり、形式手法ではない。
• エ正解。厳密な意味をもつ言語で仕様を記述し、性質との整合を論理的に検証する。

この問題に出た用語

• ホワイトボックステスト（命令網羅・分岐網羅・条件網羅）
• 形式手法（形式仕様記述）
• テスト技法（ホワイトボックステスト・ブラックボックステスト）
• ブラックボックステスト

同じ分野の他の問題

• 図のような階層構造で設計された組込みシステムがある。このシステムの開発プロジェクトにおいて,デバイスドライバ層の単体テス…2025年度 秋期 午前Ⅱ 問22
• JavaScriptなどのスクリプト言語を使って,Webブラウザに組み込まれているサーバとの非同期通信機能を利用する技術…2025年度 秋期 午前Ⅱ 問18
• アジャイル開発手法の一つであるスクラムを適用したソフトウェア開発プロジェクトにおいて、KPT手法を用いてレトロスペクティ…2025年度 春期 午前Ⅱ 問23
• アジャイル開発のプロジェクトで、ソースコードの品質を向上させるために、バグ、コードの重複、脆弱性につながるコードを自動で…2025年度 春期 午前Ⅱ 問22
• エクストリームプログラミング(XP:Extreme Programming)における“テスト駆動開発”の特徴はどれか。2024年度 秋期 午前Ⅱ 問23