Validating IoT Devices with Rate-Based Session Types

Explore a groundbreaking session types framework for implementing and validating rate-based message passing systems in Internet of Things (IoT) domains through this 18-minute conference talk from OOPSLA2 2023. Delve into the introduction of a timed process calculus with a periodic recursion primitive, designed to model the indefinite repetition common in embedded and IoT systems. Discover the concept of rate-based session types in a binary session types setting and learn about the new compatibility relationship called rate compatibility. Understand how type-checked programs enjoy standard session types guarantees and rate error freedom, ensuring processes exchange messages at the same rate. Examine the novel type expansion relation that enables communication between processes with different periods by synthesizing and checking a common superperiod type. Gain insights into the proven type preservation and rate error freedom of the system, as well as the decidable method for type checking based on computing superperiods for multiple processes. Explore the practical implementation of this framework through its embedding into Rust's native type system and its application to real-world examples such as Android software sensors, wearable devices, and sound processing.