[SERVER-43595] Literature review for TLA+ trace checker paper Created: 24/Sep/19  Updated: 29/Oct/23  Resolved: 25/Nov/19

Status: Closed
Project: Core Server
Component/s: Replication
Affects Version/s: None
Fix Version/s: 4.3.3

Type: New Feature Priority: Major - P3
Reporter: A. Jesse Jiryu Davis Assignee: A. Jesse Jiryu Davis
Resolution: Fixed Votes: 0
Labels: None
Remaining Estimate: Not Specified
Time Spent: Not Specified
Original Estimate: Not Specified

Issue Links:
Depends
is depended on by SERVER-43598 TLA+ Trace Checker paper: "Related Wo... Closed
is depended on by SERVER-44850 Second round of literature review for... Closed
Backwards Compatibility: Fully Compatible
Sprint: Repl 2019-10-07, Repl 2019-10-21, Repl 2019-11-04, Repl 2019-11-18, Repl 2019-12-02
Participants:

 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.


 Comments   
Comment by A. Jesse Jiryu Davis [ 22/Nov/19 ]

One more paper to go, added late: "Using Formal Specifications to Monitor and Guide Simulation: Verifying the Cache Coherence Engine of the Alpha 21364 Microprocessor"

Comment by A. Jesse Jiryu Davis [ 07/Oct/19 ]

Once this is done, draft a "Related Work" section and send to experts we know for review to see what we've missed. Then this ticket can be closed.

Generated at Thu Feb 08 05:03:34 UTC 2024 using Jira 9.7.1#970001-sha1:2222b88b221c4928ef0de3161136cc90c8356a66.