皆さんは「形式手法（フォーマルメソッド：Formal Methods）」という技術を聞いたことがあるでしょうか？形式手法とは、高信頼なシステムやソフトウェアを設計・開発する技術です。数学を利用してシステム・ソフトウェアの仕様を記述し、それを検証します。英語表記が複数形であることからも分かるように、形式手法は個々の手法・言語・ツールの総称であり、個々の手法は100種類以上存在します。
形式手法は、大きく2つに分類されます。「形式仕様記述」と「モデル検査（形式検証）」です。「形式仕様記述」は、数学を利用して画面（レイアウトは除く）や振舞い、データモデルを含むシステム・ソフトウェアの仕様を厳密に書き、証明ツールを利用して仕様が正しいかどうかを検証します。「モデル検査（形式検証）」は、状態の振舞いに特化して記述し、状態のあらゆる組合せに対してツールを利用した検査をします。例えば、"デッドロックは発生しない"というシステムが満たすべき性質を検査し、満たさない状態が発見されると反例を出力します。

形式手法のメリットは、厳密に記述することにより、要求や設計の矛盾、曖昧さ、抜け漏れ等の誤りに気付けることです。また、記述したものが正しいかどうかをツールで検証し、要求や設計の矛盾、曖昧さ、抜け漏れ等の誤りを発見することができることです。開発現場で通常実施されている「設計書のレビュー」と同じに聞こえるかもしれませんが、設計書のレビューでは、複雑な仕様による見つけにくい誤りや、レビューワのスキルに依存した未指摘の誤りが発生する可能性があります。形式手法を用いると自然言語の曖昧性を排除でき、ツールを併用することで属人性を排除した検証が可能となります。
形式手法のデメリットは、習得の難しさです。新種のプログラミング言語を習得するものと想像してもらえばいいかもしれません。

形式手法には大きく2つの利用方法があります。1つ目の利用方法は、最初の要求や仕様から厳密に形式手法で記述、検証を繰り返しながら仕様を詳細化していくことで、仕様に誤りを挿入させずに設計を進める方法です（Correct by Constructionと言われています）。しかし、形式手法を習得した人材が少ない状況では、習得にかかるコストとの兼ね合いになるため、この利用方法はまだ現実的ではありません。
2つ目の利用方法は、自然言語で書かれた設計書を形式手法で記述し直し、比較することで設計書の誤りを発見する方法です。高い信頼性を必要とする機能に絞って形式手法を適用し、複雑な仕様による見つけにくい誤りや、レビューワのスキルに依存した未指摘の誤りが見つけられるため、システム開発の品質向上に繋がります。
NTTデータでは、2つ目の利用方法で形式手法の活用を開始し、設計誤りの防止に努めています。