CAREER: Programming Abstractions and Formal Reasoning for IoT Application Development

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

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.