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

物联网（IoT）和实时系统已经在社会中变得无处不在，从方便的小工具到救生工具。 管理这些系统的程序的正确性是至关重要的。 不幸的是，用于构建此类系统的编程语言缺乏内置的验证方法。 到目前为止，研究主要集中在形式化方法，推导出程序的抽象模型，然后进行验证。 这种方法固有地受到程序和模型之间的脱节的影响：模型可能不准确，并且与不断发展的程序不同步。 该项目的创新之处在于通过使用会话类型将物联网和实时系统的验证与其开发相集成。 该项目提供了一种新的编程语言和类型系统，可以验证物联网和实时系统。 此类系统由许多通过消息进行通信的进程组成，验证需要确保进程遵守预期的通信协议。 为了验证通信协议，该项目开发了适用于物联网和实时系统领域的新会话类型。 该项目的影响是会话类型理论的进步，以解决这个新的应用领域和博士的培训和发展所带来的挑战。周期性、速率、延迟和一般时间的概念虽然对于物联网和实时系统是常见的，但在会话类型理论中缺乏。 该项目开发了一个新的会话类型理论能够表达这些概念。 这一发展迫使人们对通信兼容性的定义进行了根本性的重新考虑（也称为“兼容性”）。会话二元性）。时间的引入要求考虑产出和投入分别被生产和消耗的速率。 研究人员从直觉线性会话类型和会话类型pi演算之间建立的Curry-Howard对应开始。 在此基础上，研究人员整合了时间感知通信的各个方面，包括：固有的周期性，同步通信，异步通信，延迟，偶发事件和基于事件的交互过程。 该项目将产生一个形式化的证明和Rust中的实现。元理论的结果将包括声明和证明新的时间正确性属性，使用的逻辑关系方法。这个奖项反映了NSF的法定使命，并已被认为是值得通过评估使用基金会的智力价值和更广泛的影响审查标准的支持。

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.