eXtreme Modelling in Practice
summary
Two case studies compare two conformance techniques applied with TLA+ and TLC. model-based trace checking against the MongoDB Server fails after ten weeks because consistent snapshotting is hard, the spec omits concurrent dual leaders so postprocessing lies, and marginal cost per spec is too high. model-based test-case generation on Realm succeeds: TLC outputs about 30,000 states which convert to ~5,000 Go unit tests, expose a real bug and yield 100% branch coverage. Wishlist: standard JSON/CSV trace and a Toolbox button.
AI-written summary · about
chapters (4)
- 0:00Introduction to methodology
- 2:26Model-based trace checking
- 16:03Test case generation
- 20:46Conclusion and lessons
related talks
24mTLA+: Your Secret Weapon Against Concurrency Hell
30mTackling Concurrency Bugs with TLA+
01h 12mDistributed systems showdown — TLA + vs real code
44mModel-Based Testing for the Zephyr RTOS
23m„Complete” In-Sprint Testing Using Collaborative Models
49mESSENTIALS - Canon Test-Driven Development
40mAdvanced Test Coverage Criteria: Specify and Measure, Cover and Unmask
08mExample-driven development: bridging tests and documentation