Designing software with complex configurations
summary
Shows how TLA+ (with TLC) and Alloy/Alloy 6 model a spanning‑tree echo protocol and catch a subtle config bug: two specific directed networks cause a missing-parent case. TLC verifies complete graphs up to 5 nodes quickly but times out at 6 nodes (1h limit), while Alloy 6 checks all graphs up to 6 nodes in ~13 minutes and produces graphical counterexamples for validation. Emphasizes lightweight formal methods, explicit‑state vs symbolic analysis, and a practical fix that restores correctness.
AI-written summary · about
chapters (13)
- 0:00Software configuration design
- 2:09Formal methods for everyday software
- 3:34Complex software configurations
- 7:03Modeling echo protocol with TLA+
- 14:50TLA+ basics and syntax
- 18:00Validating TLA+ specs
- 24:28TLA+ limitations
- 24:51Alloy for structural design
- 27:01Alloy’s relational logic
- 32:19Extending Alloy for behavior
- 35:29Interactive Alloy 6 validation
- 37:35Finding protocol bugs with Alloy
- 39:00Final comparison
related talks
01h 13mWorkshop: TLA+ in action (Part 3)
01h 13mDesigning distributed systems with TLA+
24mTLA+: Your Secret Weapon Against Concurrency Hell
01h 12mWorkshop: TLA+ in action (Part 4)
01h 14mWorkshop: TLA+ in action (Part 1)
15mTLC: Temporal Logic of Distributed Components
01h 11mWorkshop: TLA+ in action (Part 2)
01h 12mDistributed systems showdown — TLA + vs real code