IT資格用語解説情報処理安全確保支援士試験・ソフトウェア開発手法
形式手法
更新日:
用語解説
形式手法は、数学に基づいて厳密な意味が定義された言語でソフトウェアの仕様を記述し、満たすべき性質と仕様とが整合しているかを論理的に検証する手法です。
■ 試験で押さえるポイント
形式仕様記述言語には、VDM、Z、Bメソッドなどがあります。
モデル検査は、状態遷移のモデルのすべての状態を自動で探索し、デッドロックが起きないことなどを確かめます。
自然言語の仕様にある曖昧さをなくせますが、記述と検証に専門の知識と手間がかかります。
検証の方法 | 確かめ方 |
|---|---|
形式手法 | 厳密な言語で書いた仕様が、満たすべき性質と整合するかを論理的に検証する |
インスペクション | 役割を決めた複数人で成果物を読み、欠陥を探す |
ブラックボックステスト | 内部構造を見ずに、仕様どおりに機能するかを確かめる |
ホワイトボックステスト | 内部構造に着目して、仕様どおりに動作するかを確かめる |
■ 過去問での着眼点
厳密な意味を定義できる言語で仕様を書き、性質との整合を検証するのが形式手法です。レビューやテストとは区別します。
例: 鉄道の信号制御の仕様を形式仕様記述言語で書き、2本の列車に同時に進行の信号が出ないことを証明します。