# 形式手法 形式手法(formal methods)とは、数学的に厳密な記法・モデルを用いてソフトウェアの挙動を仕様化し、その仕様に基づいて設計・実装の正しさを検証する技法の総称である。ソフトウェアライフサイクルの各段階——要件分析と仕様化・アーキテクチャ設計・詳細設計・コーディングとテスト・適合性テスト——それぞれに固有の形式手法トピックが存在し、代表的な記法として VDM・Z・B(モデルベース/抽象機械アプローチ)、Larch・ACT-ONE(代数的アプローチ)、SDL・Lotos・CCS/CSP(有限状態系の記述、通信プロトコル向け)が挙げられる。(Source: [[@1998__IEEECS__SWEBOK Straw Man - Appendix I Draft Classification of Knowledge on Formal Methods]]) ## 横断的知見 - **「仕様は書けるが検証・テスト生成の自動化は研究段階」という1998年時点の成熟度評価は、2021年のAmazon S3 ShardStoreの実務では部分的に反転している**: SWEBOK Straw Man Appendix I(1998)は、形式仕様に基づくテストケース自動導出(ブラックボックス単体テスト)や仕様からのコード自動合成を Research(研究段階)に分類し、実務で広く使われる段階には達していないと評価した。一方 ShardStore(2021)では、実装と同じ言語(Rust)で書いた実行可能な参照モデルに対する property-based テストと stateless model checking を、完全な形式検証の代替として本番システムの検証パイプラインに組み込んでいる。これは1998年に Research 段階とされたテストケース自動導出・仕様と実装の照合という方向性が、20年余りを経て(完全な数学的証明ではなく)実装言語ベースの軽量な形で実務に定着した例と解釈できる。ただし ShardStore も並行クラッシュ実行の検証は未解決として残しており、Appendix I が Advanced に分類した「証明義務の生成・解消による内部無矛盾性の検証」に相当する完全な形式証明は、2021年時点でも本番運用の主流ではない。(Source: [[@1998__IEEECS__SWEBOK Straw Man - Appendix I Draft Classification of Knowledge on Formal Methods]], [[@2021__SOSP__Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3]]) ## 未解決の問い - Appendix I の分類(Generally Accepted / Advanced / Research / Specialized)を2020年代の形式手法の実務動向(TLA+ の産業利用、決定論的シミュレーションテストなど)に当てはめ直すと、各トピックはどこまで区分が動いたか。 - Appendix I が Specialized とした通信プロトコル・ハードウェア設計向けのモデル検査は、ソフトウェア全般に対してどこまで汎化したか。 - 完全な形式証明(Advanced に分類された証明義務の生成・解消)が2020年代でも本番システムで主流化していない理由は、ツールの成熟度不足か、コスト対効果の問題か、それとも軽量形式手法で代替可能なためか。 ## 関連 - source: [[@1998__IEEECS__SWEBOK Straw Man - Appendix I Draft Classification of Knowledge on Formal Methods]] / [[@2021__SOSP__Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3]] - concept: [[軽量形式手法]] - entity: [[Guy Tremblay]] / [[ISO IEC 12207|ISO/IEC 12207]] - 書籍: [[SWEBOK Straw Man Version]] ## 出典 - Bourque, P. et al., *Guide to the Software Engineering Body of Knowledge – A Straw Man Version*, IEEE Computer Society, 1998, Appendix I. - [[@2021__SOSP__Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3]]