MongoDBにおけるエクストリームモデリング：実践的なコンプライアンスチェック

MongoDBのエンジニアは、TLA+仕様と2つのコンプライアンスチェック手法（トレースチェックとテストケース生成）を用いて、製品の実装が仕様に準拠しているかどうかを検証する実験を行いました。MongoDBサーバーで行われたトレースチェック実験は、Raftコンセンサスプロトコルの実装の検証を目指し、MongoDBモバイルSDKで行われたテストケース生成実験は、オペレーショナルトランスフォーメーションアルゴリズムの実装の検証を目指しました。その結果、トレースチェックは、マルチスレッドプログラムの状態のスナップショット取得の困難さと、仕様と実装の食い違いのために失敗しましたが、テストケース生成はアルゴリズムのバグを正常に発見し、100％のブランチカバレッジを達成しました。この記事では、得られた教訓をまとめ、この分野における最近の進歩を紹介し、TLA+の主流採用における継続的なコンプライアンスチェックの重要性を強調しています。