形式手法（形式仕様記述）とは？けいしきしゅほう
形式手法（形式仕様記述）とは、仕様を数学に基づく形式仕様記述言語で厳密に書き、モデル検査や定理証明によって性質を機械的に確かめる手法。シラバスが挙げるVDM-SLやVDM++のように、システムの状態と、その状態が満たすべき不変条件・事前条件・事後条件を記述する形が代表で、自然言語の曖昧さを排除できる。
最終更新：2026-10-06
この語が出る過去問を解く →背景
自然言語で書かれた仕様は読み手によって解釈が割れ、レビューで全ての状態の組合せを見きることもできない。テストも有限のケースしか試せないため、稀な順序でしか現れない不具合は残ってしまう。人命や資産に直結する分野では「試した範囲では見つからなかった」では足りず、「その状態には到達しない」ことを示す必要がある。この要求に応えるために、仕様そのものを検証できる形で書く道具立てが用意された。
具体例
TLS 1.3の標準化では、仕様案に対する形式的な検証が並行して行われ、鍵交換や認証の性質が成り立つことが確かめられた。国内では、非接触ICカードFeliCa向けの組込みOSの仕様記述にVDM++が使われた事例が知られており、状態遷移が複雑で後戻りの費用が大きい領域ほど投入の価値が出る。
試験での引っ掛け
形式手法を使えばテストが不要になる、という理解は誤りで、保証されるのは記述した性質とモデル化した範囲に限られ、実装が仕様どおりに書かれているかは別に確かめる必要がある。習得の負担と記述量も大きいため、全体に一律で適用するものではなく、安全性や機密性の要となる部分に絞って使う。
関連用語
出た過去問
出典：令和6年度 春期 情報処理安全確保支援士試験 午前Ⅱ 問23（IPA）
ソフトウェアの品質を確保するための検証に形式手法を用いる。このとき行う検証方法の説明として、適切なものはどれか。
正解：明確で厳密な意味を定義することができる言語を用いてソフトウェアの仕様を記述して、満たすべき性質と仕様とが整合しているかどうかを論理的に検証する。
要点：形式手法は厳密な仕様記述と論理的な検証で正しさを示す
形式手法は、数学的に意味が厳密に定まる言語で仕様を記述し、その仕様が満たすべき性質と矛盾しないことを論理的に証明したりモデル検査で網羅的に確認したりする方法である。テストのように入力例を試すのではなく、記述された範囲について網羅的に正しさを示せる点が特徴で、安全性が強く求められる分野で用いられる。一方で記述と検証の負荷が大きいため、適用範囲を絞る運用が一般的である。
出典・参考
公式シラバスの4 開発技術 ＞ 1. 開発プロセス・手法 ＞ (3) 形式手法に掲載されている用語です。
解説は資格暗記が独自に作成しています。過去問の出典は各問題に記載のとおりです。