Collaborative Research: SHF: Medium: Integrated Verification of IoT and Real-time Communication Protocols

Internet of things (IoT) and real-time systems have become pervasive in society, ranging from convenient gadgets to life saving tools. Correctness of the programs governing these systems is paramount. Unfortunately, programming languages used to build such systems lack built-in verification methodology. Research so far has focused on formal methods, deriving an abstract model of the program, which is then verified. This approach inherently suffers from a disconnect between the program and the model: the model may be inaccurate and get out of sync with the program, which evolves. The project's novelties are to integrate the verification of IoT and real-time systems with their development through the use of session types. The project contributes a new programming language and type system that enable verification of IoT and real-time systems. Such systems consist of many processes that communicate by messages, and verification entails ensuring that processes adhere to the intended protocol of communication. To verify communication protocols, the project develops new session types applicable to the domain of IoT and real-time systems. The project's impacts are the advancement of session type theory to address the challenges posed by this new application domain and the training and development of Ph.D. students. The notions of periodicity, rate, delays, and time in general, while common to IoT and real-time systems, are lacking in session type theory. The project develops a new session type theory capable of expressing these notions. The development forces a foundational reconsideration of the definition of communication compatibility (a.k.a. session duality). The introduction of time demands consideration of the rate at which outputs and inputs are produced and consumed, respectively. The investigators start with the Curry-Howard correspondence established between intuitionistic linear session types and the session-typed pi-calculus. Building on this foundation, the investigators integrate the various facets of time-aware communication including: inherent periodicity, synchronous communication, asynchronous communication, delays, sporadic events, and event-based interaction of a process. The project will produce a formalization with proofs and an implementation in Rust. Metatheoretic results will include statement and proof of novel temporal correctness properties, using the logical relations method. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.