一句话：提出端到端形式化验证框架 VeriRT，弥合实时分布式系统高层计时抽象规约与底层汇编实现之间的形式鸿沟，并在 Coq 中机器化验证。
安全攸关系统常被设计为实时分布式系统，但在实现层面为其应用形式化验证一直面临显著的技术挑战，核心难点在于高层抽象计时规约与底层实现之间存在形式上的鸿沟。本文提出 VeriRT——一个端到端的实时分布式系统形式化验证框架。该框架建立了构造形式化计时操作语义的理论基础：将传统操作语义与底层计时假设相结合，并给出针对抽象规约推理系统计时行为的原则，从而支持从抽象计时规约到低层实现的 refinement 推理。框架复用 CompCert 的正确性证明，保证实时分布式系统汇编实现层面的正确性。作者在两个贴近实际的实时系统上开展了案例研究。所有结果均在 Coq 中形式化。
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 real-time distributed systems at the implementation level has faced significant technical challenges. In this paper, we present VeriRT , an end-to-end formal verification framework that closes the formal gap between high-level abstract timed specifications and low-level implementations for real-time distributed systems.Within the framework, we establish a theoretical foundation for constructing formal timed operational semantics by integrating conventional operational semantics and low-level timing assumptions, along with principles for reasoning about their timed behaviors against abstract specifications. We leverage CompCert’s correctness proofs to guarantee the correctness of the assembly implementation of real-time distributed systems. We provide two case studies on realistic real-time systems. All the results are formalized in Coq.
@article{paperbot3232,
title = {VeriRT: An End-to-End Verification Framework for Real-Time Distributed Systems},
author = {Yoonseung Kim and Sung-Hwan Lee and Yonghyun Kim and Chung-Kil Hur},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {POPL},
year = {2025},
doi = {10.1145/3704897}
}