论文标题
实践中极端建模
eXtreme Modelling in Practice
论文作者
论文摘要
形式建模是开发复杂系统的强大工具。在MongoDB，我们使用TLA+对几个系统的多个方面进行建模和验证。确保规范及其实施之间的一致性可以为任何规范增加价值；它可以避免转录错误，防止错误，因为大型组织会迅速开发指定的代码，甚至保持同一规范的多个实现。在本文中，我们探索基于模型的测试，作为确保规范实现符合度的工具。我们尝试了两项案例研究：MongoDB Server的复制协议和基于模型的测试案例生成（MBTCG）中的基于模型的跟踪检查（MBTC）中的MongoDB Realm Sync的操作转换算法。我们发现MBTC对于测试服务器符合高度抽象的规范是不切实际的。但是，MBTCG在领域同步方面非常成功。我们分析了为什么一种技术成功而另一种技术失败，并建议未来的实施者在基于模型的测试中进行类似的尝试。
Formal modelling is a powerful tool for developing complex systems. At MongoDB, we use TLA+ to model and verify multiple aspects of several systems. Ensuring conformance between a specification and its implementation can add value to any specification; it can avoid transcription errors, prevent bugs as a large organization rapidly develops the specified code, and even keep multiple implementations of the same specification in sync. In this paper, we explore model-based testing as a tool for ensuring specification-implementation conformance. We attempted two case studies: model-based trace-checking (MBTC) in the MongoDB Server's replication protocol and model-based test-case generation (MBTCG) in MongoDB Realm Sync's operational transformation algorithm. We found MBTC to be impractical for testing that the Server conformed to a highly abstract specification. MBTCG was highly successful for Realm Sync, however. We analyze why one technique succeeded and the other failed, and advise future implementers making similar attempts at model-based testing.
