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 的法定使命，并通过使用基金会的智力优势和更广泛的评估进行评估，认为值得支持。影响审查标准。