形式手法（形式仕様記述）とは？

形式手法（形式仕様記述）の意味

仕様を数学的な記法で厳密に書き、モデル検査や定理証明によって性質を機械的に検証する手法。自然言語の曖昧さを排除し、テストでは尽くせない状態の組合せまで網羅できるため、人命や資産に関わる分野で使われる。

形式手法（形式仕様記述）の具体例

鉄道の連動装置で、同時に相反する進路が開通しないという安全性質を形式的に記述し、モデル検査で全状態を探索する。テストでは再現困難な、複数の操作が特定の順序で重なる異常な組合せを設計段階で検出できる。

形式手法（形式仕様記述）は試験でどう引っ掛けられる？

形式手法は「テストが不要になる」手法ではなく、記述した性質とモデルの範囲でしか保証しない。実装が仕様どおりかは別途確かめる必要がある。また習得コストと記述量が大きく、全システムに適用するものではない。

形式手法（形式仕様記述）と関連する用語

• モデル駆動開発（MDA）
• 命題論理と述語論理
• システムの信頼性設計（フォールトトレラント・フェールセーフ）

形式手法（形式仕様記述）が出た過去問

• ソフトウェアの品質を確保するための検証に形式手法を用いる。このとき行う検証方法の説明として、適切なものはどれか。

  正解：明確で厳密な意味を定義することができる言語を用いてソフトウェアの仕様を記述して、満たすべき性質と仕様とが整合しているかどうかを論理的に検証する。

  要点：形式手法は厳密な仕様記述と論理的な検証で正しさを示す

  形式手法は、数学的に意味が厳密に定まる言語で仕様を記述し、その仕様が満たすべき性質と矛盾しないことを論理的に証明したりモデル検査で網羅的に確認したりする方法である。テストのように入力例を試すのではなく、記述された範囲について網羅的に正しさを示せる点が特徴で、安全性が強く求められる分野で用いられる。一方で記述と検証の負荷が大きいため、適用範囲を絞る運用が一般的である。

  出典：令和6年度 春期 情報処理安全確保支援士試験 am2 問23（IPA）