CAREER: Programming Abstractions and Formal Reasoning for IoT Application Development

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.