Bridging the Verifiability Gap: Why We Need More From Our Specs and How We Get It
summary
ONOS goes from research to nationwide Comcast deployment while teams spend hours scanning gigabytes of logs to find elusive distributed bugs. The workflow adopts TLA+ and TLC to design and verify Raft extensions, leader election and distributed caches and then adds a test harness in Kubernetes and Helm that emits JSON traces to model-based trace checking and to a realtime pipeline via Kafka for model-based conformance monitoring. This catches client-centric invariant violations but struggles with infinite-stream trace retention, cross-process ordering and proving internal implementation steps.
AI-written summary · about
chapters (12)
- 0:00Intro
- 0:21Overview
- 3:26ONOS in Production
- 5:38A New ONOS
- 6:14A New Commitment to TLA+
- 7:14The Ideal Solution
- 7:56Why TLA+?
- 8:54Model-Based Trace Checking
- 9:18Test Framework
- 12:12Conformance Monitoring
- 14:50Challenges
- 16:41What We Learned Along the way
related talks
38mThe Verification of a Distributed System
48mThe Verification of a Distributed System
28mSee It to Believe It: Bringing Observability to Otherwise ...
22mTowards Modelling and Verification of Coupler Behaviour in Climate Models
01h 30mImplementing, verifying and debugging distributed event-based systems
20mSift: Using Refinement-guided Automation to Verify Complex Distributed Systems
01h 07m"Adding Observability to Distributed Systems"
40mAttesting Practically: Exploring the Glue Behind Secure Runtime Environments