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.
翻译:正式建模是开发复杂系统的有力工具。 在MongoDB, 我们使用 TLA+ 来建模和验证多个系统的多个方面。 确保规格及其执行的一致可以增加任何规格的价值; 它可以避免抄录错误, 防止作为大型组织错误的错误迅速开发指定代码, 甚至保持同一规格的多重执行同步。 在本文中, 我们探索基于模型的测试作为确保规格与执行相符的工具。 我们尝试了两个案例研究: 在MongoDB服务器的复制协议中基于模型的微量检查(MBTC)和在MOngoDB Realm Sync的操作变异算法中基于模型的立体生成(MBTCG ) 。 我们发现MBTC在测试服务器是否符合非常抽象的规格时不切实际。 但是, MBTCG 在 Realm Sync 中非常成功。 我们分析了一种技术为什么成功, 而另一种技术失败了, 我们建议未来的实施者在模型测试中进行类似的尝试 。