CAREER: Programming Abstractions and Formal Reasoning for IoT Application Development

物联网（IoT）包括提供计算、通信和与物理世界接口的网络设备系统。物联网系统越来越多地出现在广泛的应用领域，包括医疗保健、制造业、农业和家庭自动化。随着物联网系统变得越来越大、越来越复杂，开发物联网应用变得越来越困难。一种常见的方法是将数据从传感设备移动到中心位置（如云）进行处理。这种集中式方法充分利用了网络边缘的小型物联网设备，并且由于数据的大量移动可能会使网络不堪重负。另一种选择是将更多的计算放在边缘，即在生成数据的小型设备上或附近，可以更有效地利用基础设施。然而，它受到系统复杂性的限制，因为编程任务是一项艰巨的任务，需要在嵌入式编程、网络协议和分布式计算方面具有深厚的专业知识。本项目力求使后一种分散办法成为可能。该项目的新颖之处在于编程技术，它可以更容易地创建高效可靠的丰富物联网应用程序。该项目的影响是(i)创建软件工具，将在几个具有经济和社会意义的领域推进物联网应用开发；（ii）为广大受众开发物联网编程的教育资源。该项目开发(i)新的高级编程抽象和语言，使物联网程序员能够表达复杂的多设备应用逻辑，（ii）用于建立应用程序尊重正确性属性和资源消耗界限的形式化推理技术，以及（iii）管理应用程序可靠部署和有效执行的运行时系统。尽管物联网系统中存在许多不确定性来源，但编程抽象为观测确定性提供了有价值的保证。为了支持对正确性属性和资源边界的形式化推理，该项目探索了不变注释、领域特定类型和轻量级静态分析技术之间的协同作用。运行时系统确保应用程序在可用基础设施的适当资源约束下可靠地执行。该项目还为本科生和研究生开发教材，以及针对非专业物联网爱好者的软件工具和学习资源。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

The Internet of Things (IoT) encompasses systems of networked devices that provide computation, communication, and an interface with the physical world. IoT systems are finding increasing presence in a wide range of application domains, including healthcare, manufacturing, agriculture, and home automation. As IoT systems become larger and more complex, it is becoming increasingly difficult to develop IoT applications. One common approach is to move data from the sensing devices to a central location, such as the cloud, for processing. This centralized approach under-utilizes the small IoT devices at the edge of the network and can overwhelm the network due to the large movement of data. The alternative of placing more computation on the edge, that is, on or close to the small devices that generate the data, makes more efficient use of the infrastructure. It is, however, limited by the complexity of the system, as the programming task is a daunting undertaking that requires deep expertise in embedded programming, network protocols and distributed computing. This project seeks to enable the latter decentralized approach. The project's novelties are programming techniques that make it easier to create rich IoT applications that are efficient and reliable. The project's impacts are (i) the creation of software tools that will advance IoT application development in several domains of economic and societal significance and (ii) the development of educational resources on IoT programming for a broad audience.This project develops (i) new high-level programming abstractions and languages that enable IoT programmers to express complex multi-device application logic, (ii) formal reasoning techniques for establishing that an application respects correctness properties and bounds on resource consumption, and (iii) a runtime system that manages the reliable deployment and efficient execution of applications. The programming abstractions provide the valuable guarantee of observational determinism, despite the many sources of uncertainty that exist in IoT systems. In order to enable formal reasoning for correctness properties and resource bounds, the project explores the synergy among invariant annotations, domain-specific types, and lightweight static analysis techniques. The runtime system ensures that applications execute reliably and within appropriate resource constraints on the available infrastructure. The project also develops educational material for undergraduate and graduate students, as well as software tools and learning resources that target non-expert IoT enthusiasts.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.