SPLASH 2023
Sun 22 - Fri 27 October 2023 Cascais, Portugal
Fri 27 Oct 2023 17:12 - 17:30 at Room I - distribution & networking 2 Chair(s): Elisa Gonzalez Boix

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.

Fri 27 Oct

Displayed time zone: Lisbon change

16:00 - 17:30
distribution & networking 2OOPSLA at Room I
Chair(s): Elisa Gonzalez Boix Vrije Universiteit Brussel
16:00
18m
Talk
Hybrid Multiparty Session Types: Compositionality for Protocol Specification through Endpoint Projection
OOPSLA
Lorenzo Gheri University of Liverpool, Nobuko Yoshida University of Oxford
DOI
16:18
18m
Talk
Mechanizing Session-Types using a Structural View: Enforcing Linearity without Linearity
OOPSLA
Chuta Sano McGill University, Ryan Kavanagh McGill University, Brigitte Pientka McGill University
DOI
16:36
18m
Talk
Message Chains for Distributed System Verification
OOPSLA
Federico Mora University of California at Berkeley, Ankush Desai Amazon Web Services, Elizabeth Polgreen University of Edinburgh, Sanjit A. Seshia University of California at Berkeley
DOI
16:54
18m
Talk
Randomized Testing of Byzantine Fault Tolerant AlgorithmsDistinguished Paper
OOPSLA
Levin N. Winter Delft University of Technology, Florena Buse Delft University of Technology, Daan de Graaf Delft University of Technology, Klaus von Gleissenthall Vrije Universiteit Amsterdam, Burcu Kulahcioglu Ozkan Delft University of Technology
DOI
17:12
18m
Talk
Validating IoT Devices with Rate-Based Session Types
OOPSLA
Grant Iraci University at Buffalo, Cheng-En Chuang University at Buffalo, Raymond Hu Queen Mary University of London, Lukasz Ziarek University at Buffalo
DOI