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

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

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.