一句话：提出带周期递归的定时进程演算与基于速率的会话类型，保证 IoT 消息传递的速率正确性，并在 Rust 中实现原型。
许多嵌入式与 IoT 系统需周期性重复计算与通信，若进程以不同速率收发消息会导致语义错误。本文建立基于速率的会话类型框架：引入带周期递归的定时进程演算，以建模无限重复行为；在二元会话类型中定义基于速率的会话类型，并提出 rate compatibility 兼容关系。该关系通过类型扩展合成并检查公共超周期类型，使不同周期的进程可安全通信。作者证明类型保持与 rate error freedom，并给出通过计算超周期进行类型检查的可判定方法。最后将类型系统嵌入 Rust 原生类型系统实现原型，并应用于 Android 传感器、可穿戴设备与声音处理等案例。
We develop a session types based framework for implementing and validating rate-based message passing systems in Internet of Things (IoT) domains. To model the indefinite repetition present in many embedded and IoT systems, we introduce a timed process calculus with a periodic recursion primitive. This allows us to model rate-based computations and communications inherent to these application domains. We introduce a definition of rate based session types in a binary session types setting and a new compatibility relationship, which we call rate compatibility. Programs which type check enjoy the standard session types guarantees as well as rate error freedom --- meaning processes which exchanges messages do so at the same rate. Rate compatibility is defined through a new notion of type expansion, a relation that allows communication between processes of differing periods by synthesizing and checking a common superperiod type. We prove type preservation and rate error freedom for our system, and show a decidable method for type checking based on computing superperiods for a collection of processes. We implement a prototype of our type system including rate compatibility via an embedding into the native type system of Rust. We apply this framework to a range of examples from our target domain such as Android software sensors, wearable devices, and sound processing.
@article{paperbot1884,
title = {Validating IoT Devices with Rate-Based Session Types},
author = {Grant Iraci and Cheng-En Chuang and Raymond Hu and Lukasz Ziarek},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {OOPSLA2},
year = {2023},
doi = {10.1145/3622854}
}