Rate-Based Session Types for IoT Systems

We develop a session types 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. Our framework is used to implement a heart rate sensor application that runs on a commercially available smartwatch.

• Publication year

  2025

• Venue

  ACM Transactions on Programming Languages and Systems

• Publication date

  2025-07-24

• Fields of study

  Not labeled

• Identifiers
  DOI 10.1145/3754449
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Fearless Asynchronous Communications with Timed Multiparty Session Protocols

  2024cited by this paper
• Validating IoT Devices with Rate-Based Session Types

  2023cited by this paper
• Stay Safe under Panic: Affine Rust Programming with Multiparty Session Types

  2022cited by this paper
• Deadlock-free asynchronous message reordering in rust with multiparty session types

  2021cited by this paper
• Virtual Sensors

  2021cited by this paper
• Duality of Session Types: The Final Cut

  2020cited by this paper
• Ferrite: A Judgmental Embedding of Session Types in Rust

  2020cited by this paper
• Collaborative Sensing with Interactive Learning using Dynamic Intelligent Virtual Sensors

  2019cited by this paper
• Less is more: multiparty session types revisited

  2019cited by this paper
• Digital Twin in Industry: State-of-the-Art

  2019cited by this paper
• Fast, Furious and Insecure: Passive Keyless Entry and Start Systems in Modern Supercars

  2019cited by this paper
• TinyML: Machine Learning with TensorFlow Lite on Arduino and Ultra-Low-Power Microcontrollers

  2019cited by this paper
• Parallel complexity analysis with temporal session types

  2018cited by this paper
• Software-Defined Radio for Engineers

  2018cited by this paper
• A Survey on Internet of Things: Architecture, Enabling Technologies, Security and Privacy, and Applications

  2017cited by this paper
• Manifest sharing with session types

  2017cited by this paper
• A virtual layer of measure based on soft sensors

  2016cited by this paper
• Session types for Rust

  2015cited by this paper
• Sensor Cloud: A Cloud of Virtual Sensors

  2014cited by this paper
• Timed Multiparty Session Types

  2014cited by this paper
• Global progress for dynamically interleaved multiparty sessions

  2014cited by this paper
• Propositions as sessions

  2012cited by this paper
• Real-time estimation of biomass and specific growth rate in physiologically variable recombinant fed-batch processes

  2012cited by this paper
• Session Types as Intuitionistic Linear Propositions

  2010cited by this paper
• Multiparty asynchronous session types

  2008cited by this paper
• Wireless sensor network survey

  2008cited by this paper
• Language Primitives and Type Discipline for Structured Communication-Based Programming Revisited: Two Systems for Higher-Order Session Communication

  2007influential reference
• Typing the Behavior of Software Components using Session Types

  2006cited by this paper
• Subtyping for session types in the pi calculus

  2005influential reference
• The MIT Press

  2005cited by this paper
• Typing the Behavior of Objects and Component Using Session Types

  2003cited by this paper
• WCET analysis of probabilistic hard real-time systems

  2002cited by this paper
• LANGUAGE PRIMITIVES AND TYPE DISCIPLINE FOR STRUCTURED COMMUNICATION-BASED PROGRAMMING

  1998influential reference
• 袖珍操作系统-QNX/Neutrino

  1998cited by this paper
• Multi-Sensor Fusion: Fundamentals and Applications With Software

  1997cited by this paper
• Types for Dyadic Interaction

  1993cited by this paper
• Scheduling Algorithms for Multiprogramming in a Hard-Real-Time Environment

  1989influential reference

• No citing papers are available for this paper.