一句话：提出完全语义的逻辑关系，用于验证异构应用与硬件设备对定时消息传递协议的合规性，并配以 refinement 类型系统与 Rust 类型检查器。
许多消息传递系统不仅要求消息按特定顺序交换，还要求消息在特定时刻或时间窗口内发生，这在 IoT 与实时系统中尤为普遍。由于这类系统具有异构性——应用与硬件设备往往用不同语言实现——依赖统一高级类型语言的验证方法不再适用。本文提出一种逻辑关系，用来验证其「居民」（待验证的应用与硬件设备）是否遵守给定的定时协议。该逻辑关系完全语义化，不要求居民在语法上良类型，从而支持两种使用模式：(i) 给定类型系统后对任意良类型应用的一次性验证；(ii) 对特定应用或硬件设备（即 foreign code）的逐实例验证。为支持模式 (i)，作者设计了一个表达定时消息传递协议的 refinement 类型系统，并证明基本定理：任何良类型程序都居住于该逻辑关系之中。类型检查器已在 Rust 中实现，并用 SMT 求解器检查时间约束的可满足性。最后通过一个智能家居空气质量监测系统（由控制器应用与多种环境传感器组成）的小型案例研究展示了两种使用模式。
Many of today’s message-passing systems not only require messages to be exchanged in a certain order but also to happen at a certain time or within a certain time window . Such correctness conditions are particularly prominent in Internet of Things (IoT) and real-time systems applications, which interface with hardware devices that come with inherent timing constraints. Verifying compliance of such systems with the intended timed protocol is challenged by their heterogeneity —ruling out any verification method that relies on the system to be implemented in one common language, let alone in a high-level and typed programming language. To address this challenge, this paper contributes a logical relation to verify that its inhabitants (the applications and hardware devices to be proved correct) comply with the given timed protocol. To cater to the systems’ heterogeneity, the logical relation is entirely semantic , lifting the requirement that its inhabitants are syntactically well-typed. A semantic approach enables two modes of use of the logical relation for program verification: (i) once-and-for-all verification of an arbitrary well-typed application, given a type system, and (ii) per-instance verification of a specific application / hardware device ( a.k.a ., foreign code). To facilitate mode (i) , the paper develops a refinement type system for expressing timed message-passing protocols and proves that any well-typed program inhabits the logical relation (fundamental theorem). A type checker for the refinement type system has been implemented in Rust, using an SMT solver to check satisfiability of timing constraints. Then, the paper demonstrates both modes of use based on a small case study of a smart home system for monitoring air quality, consisting of a controller application and various environment sensors.
@article{YaoICBZ25,
title = {Semantic Logical Relations for Timed Message-Passing Protocols},
author = {Yue Yao and Grant Iraci and Cheng-En Chuang and Stephanie Balzer and Lukasz Ziarek},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {POPL},
year = {2025},
doi = {10.1145/3704895}
}