专题：model_checking

本文提出基于模型的验证方法，用于检查MongoDB分布式事务协议与WiredTiger存储引擎接口的一致性。通过TLA+建模和路径驱动测试，实现了自动化验证，具有较高的技术深度和实际应用价值。