Uploaded image for project: 'Core Server'
  1. Core Server
  2. SERVER-43595

Literature review for TLA+ trace checker paper

    XMLWordPrintableJSON

Details

    • Icon: New Feature New Feature
    • Resolution: Fixed
    • Icon: Major - P3 Major - P3
    • 4.3.3
    • None
    • Replication
    • None
    • Fully Compatible
    • Repl 2019-10-07, Repl 2019-10-21, Repl 2019-11-04, Repl 2019-11-18, Repl 2019-12-02

    Description

      Search for related papers, the papers they cite, the papers that cite them, etc.

      Read or skim selected papers and summarize them well enough for our paper's Related Work section: how do they differ from our approach, why can't we use their approach, how do we build upon them.

      Some important titles:

      • Model-Based Trace Checking
      • Trace Analysis for Conformance and Arbitration Testing
      • A General Approach to Trace-Checking in Distributed Computing Systems
      • Verifying Software Traces Against a Formal Specification with TLA+ and TLC - self-published by Ron Pressler
      • Concurrent development of model and implementation
      • A model-based trace testing approach for validation of formal co-simulation models

      Things we're looking for:

      • Techniques to verify that an implementation matches a formal model. In "How Amazon Web Services Uses Formal Methods" they wrote, 'On learning about TLA+, engineers usually ask, “How do we know that the executable code correctly implements the verified design?” The answer is we do not know.' OTOH there is the "Model-Based Trace Checking" paper, but not for TLA+, not for industrial software like MongoDB, and not deployed to CI.
      • Any estimates of the likelihood of mismatches due to "transcription bugs" in either direction: when implementing a spec or modeling an existing implementation. Any estimates of the cost of these bugs.
      • Techniques to measure how much of the formal spec's state space is covered by implementation tests.
      • Techniques to increase this coverage.

      Attachments

        Activity

          People

            jesse@mongodb.com A. Jesse Jiryu Davis
            jesse@mongodb.com A. Jesse Jiryu Davis
            Votes:
            0 Vote for this issue
            Watchers:
            2 Start watching this issue

            Dates

              Created:
              Updated:
              Resolved: