TLC: Temporal Logic of Distributed Components
summary
TLC is a temporal program logic that verifies both safety and liveness of layered distributed components and proves soundness against an operational semantics for stacks. It defines handlers that return (new state, outgoing requests, outgoing indications), a lowering transformation that pushes and restricts assertions for subcomponents, and a small set of inference rules that reduce global temporal invariants to handler checks. Authors mechanize proofs, claiming mechanized in Coq soundness, and apply TLC to stubborn links, perfect links, best-effort and uniform reliable broadcast, and epoch Paxos with worked examples (e.g., PL no-forge via three explicit steps).
AI-written summary · about
chapters (13)
- 0:00Intro
- 0:50Temporal Logic of Composable Components
- 1:38Layers of Components
- 1:53Component Implementation
- 3:40Semantics of Distributed Stacks
- 4:23Assertion Language
- 6:46Compositional Verification
- 8:02Lowering Specifications, Push
- 8:39Lowering Specifications, Restrict
- 9:24Program Logic
- 11:13Proof
- 12:14If a perfect link deliver event is issued then the issuing event is a stubborn link deliver event.
- 13:23Semantics and Soundness
related talks
01h 12mWorkshop: TLA+ in action (Part 4)
01h 13mDesigning distributed systems with TLA+
41mDesigning software with complex configurations
01h 11mWorkshop: TLA+ in action (Part 2)
01h 13mWorkshop: TLA+ in action (Part 3)
01h 14mWorkshop: TLA+ in action (Part 1)
18mSmart Casual Verification of the Confidential Consortium Framework
28mReasoning about Distributed Reconfigurable Systems