# 軽量形式手法 軽量形式手法とは、完全な形式検証(full formal verification)の健全性を追求する代わりに、自動化・使いやすさ・システムと仕様が継続的に変化する中で正しさを保ち続ける能力を優先する、実用的な検証アプローチを指す。ShardStore の事例では、実装と同じ言語(Rust)で書かれた実行可能な参照モデルを、property-based テストと stateless model checking で実装と照合することで実現される。正しさの特性(逐次クラッシュなし・逐次クラッシュあり・並行クラッシュなし)を分解し、それぞれに最も適した検証ツールを割り当てる点が特徴である(Source: [[@2021__SOSP__Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3]])。 ## 横断的知見 - (まだ単一ソースのみ。他ソースとの突き合わせが可能になり次第、知見を積み増す。) ## 未解決の問い - 並行クラッシュ実行(並行性とクラッシュの組み合わせ)を検証する有効な自動化手法は何か。ShardStore の事例では未確立のまま残されている。 - 実装と同じ言語で参照モデルを書くアプローチは、Rust 以外の言語(例: Go・Java 製の分散ストレージシステム)でも同程度の保守コスト削減効果を持つか。 - リソース枯渇(disk space・メモリ)系の障害を、テスト環境固有のオーバーヘッドと実バグを区別しながら自動検証する手法は確立できるか。 - 軽量形式手法によって検出される不具合の分布(機能的正しさ/クラッシュ整合性/並行性)は、他の本番ストレージシステムでも同様の比率になるか。 ## 関連 - ソース: [[@2021__SOSP__Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3]] - エンティティ: [[ShardStore]] / [[James Bornholt]] / [[Amazon Web Services]] ## 出典 - [[@2021__SOSP__Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3]]