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

物联网(IoT)和实时系统已经在社会上变得无处不在，从方便的小工具到拯救生命的工具。管理这些系统的程序的正确性至关重要。不幸的是，用于构建此类系统的编程语言缺乏内置的验证方法。到目前为止，研究集中在形式方法上，推导出程序的抽象模型，然后进行验证。这种方法固有地受到程序和模型之间的脱节的影响：模型可能不准确，并且与程序不同步，从而演变成程序。该项目的创新之处在于通过使用会话类型将物联网和实时系统的验证与开发相结合。该项目贡献了一种新的编程语言和类型系统，可以对物联网和实时系统进行验证。这类系统由许多通过消息进行通信的进程组成，验证需要确保进程遵守预定的通信协议。为了验证通信协议，该项目开发了适用于物联网和实时系统领域的新会话类型。该项目的影响是会话类型理论的进步，以应对这一新的应用领域带来的挑战，以及博士生的培养和发展。虽然周期、速率、延迟和一般时间的概念在物联网和实时系统中很常见，但会话类型理论中缺乏这些概念。该项目开发了一种新的会话类型理论，能够表达这些概念。这一发展迫使人们从根本上重新考虑通信兼容性的定义(又名会话二元性)。引入时间需要考虑产出和投入分别产生和消耗的速度。研究人员从建立在直觉型线性会话类型和会话类型圆周率演算之间的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.