eXtreme Modelling in Practice

TL;DR

This paper evaluates model-based testing techniques in practice within MongoDB, demonstrating success with test-case generation but challenges with trace-checking for complex specifications.

Contribution

It provides practical insights into applying model-based testing methods to real-world systems, highlighting successes and limitations.

Findings

Model-based trace-checking was impractical for complex specifications.

Model-based test-case generation was highly successful for Realm Sync.

Analysis of why one technique succeeded and the other failed.

Abstract

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.