CAREER: Programming Abstractions and Formal Reasoning for IoT Application Development

职业：物联网应用程序开发的编程抽象和形式推理

• 批准号: 2340479
• 负责人: Konstantinos Mamouras
• 金额: $ 54.76万
• 依托单位: William Marsh Rice University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2024
• 资助国家: 美国
• 起止时间: 2024-02-01 至 2029-01-31
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2340479&HistoricalAwards=false
• 关键词: CAREER; Programming; Abstractions; Formal; Reasoning

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.

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