分野：テクノロジ系
中分類：システム開発技術
小分類：ソフトウェア構築

形式手法は、機械処理可能で数学的に厳密に定義づけられた言語でソフトウェアの要求事項と検証対象を記述し、ソフトウェアがユーザーの求める仕様を満たせているかどうかを論理的に検証する手法です。形式手法を支援するツールとして、VDM、B-method、Zなどがあります。

形式手法では形式仕様記述言語に基づいて整合性の検証が行われることから、人の目では見つけることが困難な誤りも検出することができ、検証した部分に不具合がないことの保証を得ることができます。形式手法は、設計を検証する「モデル検査」、要求からプログラム実装の過程を検証する「形式仕様記述」、プログラム実装を検証する「プログラム検証」に分類されます。

• インスペクションの説明です。事前に役割を決められた参加者が責任のある第三者(モデレーター)の下で成果物を確認する最も公式なレビュー技法です。
• ブラックボックステストの説明です。システムの内部構造を考慮せず、システムに与える入力とそれに対する出力だけに着目して、入力に対する仕様書通りになっているかを検証するテストです。
• ホワイトボックステストに関する説明です。プログラムやモジュールの単体テストとして実施されるテスト手法で内部構造に基づき仕様書通りに動作するかを検証するために実施されます。
• 正しい。形式手法によるソフトウェア検証の説明です。