HackerPapers

arXiv:2006.00915cs.SE

eXtreme Modelling in Practice

A. Jesse Jiryu Davis, Max Hirschhorn, Judah Schvimer

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.

arXiv comments
Journal reference
PVLDB (Proceedings of the VLDB Endowment), Vol. 13, No. 9, pp. 1346-1358 (2020)
DOI
doi:10.14778/3397230.3397233
Subjects
cs.SESoftware Engineering cs.LOLogic in Computer Science

On Hacker News

Linked by 2 identifiable commenters in 5 comments across 5 threads, from Sep 2022 to Jun 2025.

Comments linking this paper, per year.

Discussed in comments5 threads

  1. What works (and doesn't) selling formal methods 1 comment

    • With one client I have, we know the TLA+ model is accurate because we're extracting tests directly from the spec. It's kind of a riff on what MongoDB does in this paper: https://arxiv.org/abs/2006.00915

      hwayneView on HNParent context

  2. A Liveness Example in TLA+ 1 comment
  3. Quint 1 comment

    • In addition to what everybody else is saying about the value of having a spec at all, there's a lot of exciting developments now in using a spec to generate a test suite, which is way simpler than using a spec to generate production code. Example: https://arxiv.org/abs/2006.00915

      hwayneView on HNParent context

  4. FoundationDB: A Distributed Key-Value Store 1 comment

    • Yes, I managed to find it: "eXtreme Modeling in Practice" https://arxiv.org/pdf/2006.00915.pdf Unfortunately I got the product wrong; it was not Atlas, it was Realm Sync. All of the test-case generation stuff is in Section 5.

      aseippView on HNParent context

  5. Learn TLA+ 1 comment

    • The universal problem is "generating code from a formal spec" is extremely, maddeningly, pull-your-hair-outingly hard. A slightly easier thing, as you said, generating test cases, which is what the Mongo people have been advancing: https://arxiv.org/abs/2006.00915 (Another…

      hwayneView on HNParent context

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.