問23 形式手法による検証

情報処理​安全確保​支援士 令和6年度 春期 午前II、全25問のうちの問23。

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

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

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

正解はエです。

ふつうの文章で書いた仕様は、読む人によって意味がぶれることがあります。形式手法では、数学に基づいて意味が 1 つに決まる言語 (形式仕様記述言語) で仕様を書きます。そのうえで、「デッドロックが起きない」「残高が負にならない」のような満たすべき性質と仕様が食い違っていないかを、証明や、ありうる状態を道具で調べ尽くす方法 (モデル検査) で論理的に確かめます。正解はエです。

ほかの選択肢が違う理由

  • ア進行役や記録役などの役割を決めた複数人で欠陥を探すのは、インスペクションの説明です。
  • イ内部の作りを見ずに、仕様どおりに機能するかを入力と出力で確かめるのは、ブラックボックステストの説明です。
  • ウ内部の作りに着目して、命令や分岐を通しながら仕様どおりに動くかを確かめるのは、ホワイトボックステストの説明です。

仕組み

テストは、選んだ入力について正しく動くことしか示せません。形式手法は、条件を満たすすべての場合について性質が成り立つことを示せるのが強みです。

その代わり、厳密に書くための手間と知識が要ります。鉄道や航空、暗号のプロトコルのように、誤りが大きな事故につながる所で特に使われます。

この問に出る言葉