VeriRT: An End-to-End Verification Framework for Real-Time Distributed Systems

• DOI: 10.1145/3704897
• Publication Date: 2025-01-09T10:48:42Z
• Authors: Yoonseung Kim; Sung-Hwan Lee; Yonghyun Kim; Chung-Kil Hur
• Keywords: End-to-end principle; End of history; Dead end

Safety-critical systems are often designed as real-time distributed systems. Despite the need for strong guarantees of safety and reliability in these systems, applying formal verification methods to at implementation level has faced significant technical challenges. In this paper, we present VeriRT, an end-to-end framework that closes gap between high-level abstract timed specifications low-level implementations Within framework, establish a theoretical foundation constructing operational semantics by integrating conventional timing assumptions, along with principles reasoning about their behaviors against specifications. We leverage CompCert’s correctness proofs guarantee assembly provide two case studies on realistic All results formalized Coq.