「形式手法」「フォーマルメソッド」(formal methods)という言葉は,数理論理学等を基盤として品質の高いソフトウェアを効率よくための科学的・系統的アプローチの総称です.この言葉の絶対的な定義があるわけではありませんが,大まかには以下のようにまとめることができます.
形式手法においては,数理論理学等に基づき,システムの注目する側面を正確に,曖昧さのないモデルで表現する.これによりシステムへに関する理解を明確にするとともに,システムの満たす性質について科学的・系統的な分析や検証を行う.その結果,曖昧な理解や誤りを早期に発見し手戻りを防いだり,分析・検証により品質を高めたりすることができる.
以下ではもう少し詳細に,形式手法の考え方とその利点や限界,また利用可能なツールや産業界での適用に関する現状を説明します.