VeriRT: An End-To-End Verification Framework for Real-Time Distributed Systems
summary
VeriRT provides an end-to-end framework that links abstract timed specs to assembly by (1) embedding low-level timing assumptions into operational semantics, (2) validating those assumptions via WCET analysis or testing, and (3) reusing CompCert-backed assembly correctness (extension of CompCert 3.9) to propagate guarantees. The framework formalizes timed operational semantics, produces a special NB event to rule out timing violations, and verifies two systems — Parsware middleware and Cristian’s clock sync — with Coq-formalized case studies.
AI-written summary · about
chapters (9)
- 0:00VeriRT framework
- 1:11Real-time distributed challenges
- 3:59Timing behavior modeling
- 7:41Timing and computation reasoning
- 11:15Nondeterminism handling
- 13:03VeriRT architecture
- 15:13Case studies: Parsware & clock sync
- 17:43Summary
- 18:05Q&A
related talks
01h 30mImplementing, verifying and debugging distributed event-based systems
38mThe Verification of a Distributed System
19mBridging the Verifiability Gap: Why We Need More From Our Specs and How We Get It
15mModular Verification of Op-Based CRDTs in Separation Logic
48mThe Verification of a Distributed System
22mTowards Modelling and Verification of Coupler Behaviour in Climate Models
19mMostly Automated Verification of Liveness Properties for Distributed Protocols w...
22mKatara: Synthesizing CRDTs with Verified Lifting