Proof assistants are a programming technique for writing trustworthy software, in which the programmer writes not only the program code but also a mathematical proof of the code's correctness. An automated proof checker then either verifies that the code is correct or shows where the proof is wrong, thus empowering the programmer to fix incorrect assumptions. This project focuses on the goal of software assurance for autonomous vehicles (AVs), which are complex cyber-physical systems, such as multi-robot teams, that move in the world and interact with one another. Examples of these systems include self-driving cars, automated drones for inspection and surveillance, and rescue robots for disaster recovery. Programs that interact with the real world through sensors and actuators must make many assumptions about noisy sensors, physics, human users, and other circumstances that cannot be controlled by the program. The intellectual merits are three tools to implement and prove complex AVs correct for noisy, real-world operations. These tools equip AVs to handle increasing levels of complexity of interaction. This project will lead to advances in software assurance of many kinds of AVs and multi-CPS systems. The project's broader significance and importance are that all kinds of AVs in the future must be built to be safe for real-world deployment, even under adverse conditions. Interoperability of diverse AV systems will also be improved, which will aid in coordination, for example among first-responders. The project integrates three key tasks into the verification of cyber-physical systems with increasing levels of concurrent operation. First, the project investigates the application of transformers to AVs. A transformer is a mechanism to combine a complex program with a proof about a corresponding simpler program in order to yield a proof about the complex program. This method will empower engineers to design AVs that can interact with one another safely and correctly in the real world without proving by hand the correctness of the multi-CPS variant of the program that handles errors in sensing and actuation. In the second task, the project turns to the verification of certain core building blocks of mobile AVs, including the rapidly-exploring random trees (RRT) motion planner and the Kalman filter state estimator. The core challenge in this task is to prove properties about algorithms that use continuum probabilities and other real numbers, typically implemented as floats. Since floating-point errors present an obstacle to verification, the PIs instead leverage constructive reals, which are capable of computing a result to arbitrary precision. In the third task, the project seeks to define a type system as the basis for codifying and performing inference about capabilities of heterogeneous AVs. This representation of capabilities is flexible, extensible, and supports probabilistic inference, thus accounting for sensing and actuation errors. This task will enable close coordination, even among AVs that have never encountered one another before.

One of the challenges toward achieving the vision of smart cities is improving the state of the underground infrastructure. For example, large US cities have thousands of miles of aging water mains, resulting in hundreds of breaks every year, and a large percentage of water consumption that is unaccounted for. The goal of this project is to develop models and methods to generate, analyze, and share data on underground infrastructure systems, such as water, gas, electricity , and sewer networks. The interdisciplinary team of investigators from the University of Illinois at Chicago, Brown University, and Northwestern University will leverage partnerships with the cities of Chicago and Evanston, Illinois, to make the approach and findings relevant to their stakeholders. Research results will be incorporated in courses at the three institutions. Outreach efforts include events for K-12 students to develop awareness about underground infrastructure from a data and computational perspective. The results of the project will ultimately help municipalities maintain and renovate civil infrastructure in a more effective manner. Cities are cyber-physical systems on a grand scale, and developing a precise knowledge of their infrastructure is critical to building a foundation for the future smart city. This proposal takes an information centric approach based on the complex interaction among thematic data layers to developing, visualizing, querying, analyzing, and providing access to a comprehensive representation of the urban underground infrastructure starting from incomplete and imprecise data. Specifically, the project has the following main technical components: (1) Generation of accurate GIS-based representations of underground infrastructure systems from paper maps, CAD drawings, and other legacy data sources; (2) Visualization of multi-layer networks combining schematic overview diagrams with detailed geometric representations; (3) Query processing algorithms for integrating spatial, temporal, and network data about underground infrastructure systems; (4) Data analytics spanning heterogeneous geospatial data sources and incorporating uncertainty and constraints; (5) Selective access to stakeholders on a need-to-know basis and facilitating data sharing; and (6) Evaluation in collaboration with the cities of Chicago and Evanston.

Two current trends promise to revolutionize the safety, reliability, and energy-efficiency of future automotive transportation: (i) wireless connectivity of vehicles to each other, to smart infrastructure, and to other mobile devices, and (ii) autonomy, ranging from driver assistance to full self-driving autonomy. Connected autonomous vehicles (CAVs) are cyber-physical systems with increasingly complex software algorithms in control of a physical vehicle moving in uncertain real-world environments. Planned connectivity regulations and recent advances in vehicular autonomy by leading manufacturers imply that CAVs will be ubiquitous in the near future. Roads will be data-rich environments where a large number of wireless devices attached to vehicles, infrastructure, personal electronics, and wearable gadgets will transmit multimodal data. In this scenario, two serious challenges arise for CAVs: (1) Onboard computational limitations may imply a de facto upper bound on the number of data sources that can be accommodated by the autonomy algorithms, and may introduce the problem of appropriately choosing a smaller subset of the available data, and (2) Given the finite amount of radio frequency spectrum and the rapidly growing number of wireless applications and end-users, spectrum scarcity arises, for which current communication protocols do not suffice. We observe that these two challenges are in fact intricately related, and that it is beneficial to address them together. To this end, the goal of this project is to investigate bidirectional interactions between the technologies of autonomy and of wireless connectivity in cyber-physical systems. Using CAVs as a case study in cyber-physical systems, we propose to investigate how estimation and control algorithms affect - and are affected by - software-defined radio communications in spectrum-scarce, data-rich environments. The technical premise of this project is an emphasis on data-rich environments, where too much data can overwhelm autonomy algorithms, e.g. real-time short-horizon trajectory planners for vehicles. The proposed approach of selecting the data sources that are likely to be the "most informative" is a new aspect compared to planning algorithms in the literature. Furthermore, this selection is dynamic, in that it evolves with the trajectory plan. This selective connectivity also helps the wireless spectrum sensing algorithm to converge faster by limiting the spatial regions to sweep for potential connections. The proposed trajectory planning algorithm is based on the so-called method of lifted graphs, which promises to bridge the gap between fast geometric path planning algorithms and slower control-theoretic techniques that incorporate vehicle dynamical constraints. Beyond CAVs, the proposed technical approach can be applied to other cyber-physical systems where several non-cooperative agents communicate over wireless channels. The proposed trajectory planning approach is sufficiently general to allow the formulations and solutions of different application-specific planning problems.

The primary objective of this research is to develop a new computing paradigm for wirelessly powered Internet-of-things (IoT) based devices and enhance their computational capabilities by more than an order of magnitude. The proposed research brings new opportunities to emerging applications such as computational RFIDs (Radio Frequency Identifiers), bio-implantable devices, and structural/environmental monitoring. The results of this research will contribute to the development of smarter IoT devices that are beyond the boundaries of traditional cyber-physical systems. Thus, significant new opportunities are expected in healthcare, energy, structural and environmental monitoring with substantial benefits to science, industry, and society at large. The PIs will promote outreach activities with emphasis on high school students and underrepresented groups. Undergraduate involvement will be encouraged through not only traditional means, but also through involvement of the PIs in professional societies and REU opportunities. One of the significant barriers that slows down the global scalability of IoT devices is the energy cost. Despite a variety of already existing techniques for energy harvesting methods, the computing capability of most of the IoT devices is limited by the available power. This research embodies a novel vision on developing an efficient computing method and corresponding IoT hardware architecture tailored for wireless energy harvesting. Specifically, the existing charge-recycling theory is leveraged in a unique way and the harvested AC signal is used to directly power the IoT device. Remarkable benefits are expected from this approach, e.g., i) the power loss due to rectification and regulation are eliminated, ii) the computational unit within the IoT device operates an order of magnitude more efficiently since the electrical charge is recycled rather than dissipated to ground. This unprecedented increase in energy efficiency enhances the on-site IoT device intelligence, thereby allowing for local decision making mechanisms.

The security of every vehicle on the road is necessary to ensure the safety of every person on or near roadways, whether a motorist, bicyclist, or pedestrian. Features such as infotainment, telematics, and driver assistance greatly increase the complexity of vehicles: top-of-the-line cars contain over 200 computers and 100 million lines of software code. With rising complexity comes rising costs to ensure safety and security. This project investigates novel methods to improve vehicular security by detecting malicious cyber attacks against a moving automobile and responding to those attacks in a manner that ensures the safety of humans in close proximity to the vehicle. The objective of this project is to protect in-vehicle networks from remote cyber attacks. The method of protection is a distributed in-vehicle network intrusion detection system (IDS) using information flow tracking and sensor data provenance in the cyber domain with novel approaches to address the physical uncertainty and time constraints of an automotive control system. When an intrusion is detected, the IDS triggers a fail-operational mode change to provide graceful degradation of service and initiate recovery without compromising human safety. Specific research aims of this project are to explore the design space of fail-operational IDS for automotive in-vehicle networks, to evaluate security and resiliency of an automobile using a fail-operational IDS, and to generalize fundamentals of a fail-operational IDS to other cyber-physical systems.

The ultimate goal of the project is to help the electric grid become more reliable even when a large amount of electricity is generated from green, but intermittent - sources such as solar and wind. To deal with this intermittency, inexpensive source of energy storage are required. Instead of investing in batteries, this project seeks to obtain cheap storage by manipulating power demand in consumer loads through intelligent decision-making algorithms. By varying power demand up and down from what a load would nominally consume, the load can be made to behave like a battery, effectively creating a source of Virtual Energy Storage (VES). This kind of virtual storage is cheaper than batteries since it is a software-based solution; little additional hardware is needed. Another aspect of the project is to develop decision-making algorithms to cope with operational issues faced by the power distribution networks (that deliver electricity to neighborhoods) due to increasing use of intermittent solar power. There are several technical challenges in achieving this vision: of intelligently manipulating consumer loads and other devices to help the power grid operate reliably. This project aims to address two of these key challenges. One is the design of algorithms to coordinate the actions of a large number of loads without a central decision-maker. Distributed (as opposed to centralized) control will be necessary since the communication and computation burden of a centralized scheme is overwhelming. At the same time, distributed control algorithms need to deliver reliable performance with low communication bandwidth, and be cognizant of the privacy and security concerns inherent in such Cyber Physical Systems (CPS) with humans in the loop. The second challenge is that the demand manipulation at the loads has to be done in such a manner that consumers. Quality of Service (QoS) is maintained in tight, pre-negotiated bounds. A number of technical innovations undergird the proposed work. These innovations include (1) frequency decomposition to map consumer resources to grid?s needs, (2) randomized control algorithms to convert intractable combinatorial optimization problems to tractable convex problems, and (3) physical signaling through grid-frequency and voltage measurements to enable multi-agent coordination without explicit communication.

Inspired by the manner in which humans improvise in everyday life, this NSF project is creating a theory of algorithmic improvisation for cyber-physical systems design. It is developing a mathematical framework, supported by tools, to address the challenge of designing systems that adapt to uncertainty in their operating environment and to changing requirements. Moreover, this framework has broad relevance to many fields in computer science and engineering. Results from the proposed work are being incorporated into teaching, with a particularly strong impact on courses at UC Berkeley on cyber-physical systems and formal methods, and on undergraduate projects conducted under broader outreach programs at UC Berkeley. Additionally, through collaborations with industry partners, the project is improving the state of the art in verification and control in the cyber-physical systems industry. Uncertainty in the design process, in the behavior of sub-systems that evolve over time, and in the operating environment remains a challenge for CPS design. There is a need to design automatic controllers that improvise to handle challenging situations as a skilled human would. This project addresses this need with a foundation approach that is developing a theoretically-sound definition of algorithmic improvisation that is also grounded in practice. It is exploring the full range of variations of the problem definition, analyzing their computational complexity, and devising efficient algorithms where shown to be theoretically possible. Additionally, it is developing new applications to verification, in novel algorithms for simulation-driven verification and verification of machine learning components, and to control, using improvisation for randomized robot path planning and for controlled exploration in adaptive, learning-based control. Together, this tight combination of theoretical work and practical applications seeks to break new ground in the science of cyber-physical systems.

The security of every vehicle on the road is necessary to ensure the safety of every person on or near roadways, whether a motorist, bicyclist, or pedestrian. Features such as infotainment, telematics, and driver assistance greatly increase the complexity of vehicles: top-of-the-line cars contain over 200 computers and 100 million lines of software code. With rising complexity comes rising costs to ensure safety and security. This project investigates novel methods to improve vehicular security by detecting malicious cyber attacks against a moving automobile and responding to those attacks in a manner that ensures the safety of humans in close proximity to the vehicle. The objective of this project is to protect in-vehicle networks from remote cyber attacks. The method of protection is a distributed in-vehicle network intrusion detection system (IDS) using information flow tracking and sensor data provenance in the cyber domain with novel approaches to address the physical uncertainty and time constraints of an automotive control system. When an intrusion is detected, the IDS triggers a fail-operational mode change to provide graceful degradation of service and initiate recovery without compromising human safety. Specific research aims of this project are to explore the design space of fail-operational IDS for automotive in-vehicle networks, to evaluate security and resiliency of an automobile using a fail-operational IDS, and to generalize fundamentals of a fail-operational IDS to other cyber-physical systems.

The rapid decrease in the cost of solar modules is motivating significant increases in distributed solar generation from rooftops and solar farms. Since the electric grid was not designed to support large-scale decentralized, intermittent, and uncontrollable solar generation, there are strict caps set on the amount of solar energy that may connect to the grid. Unfortunately, due to rapid solar growth, users are now starting to hit these caps. In addition, setting strict caps is highly inefficient, and wastes much of the grid's potential to accept solar power. Instead, as in the Internet, all users should be able to freely connect solar modules to the grid and dynamically share its capacity to transmit solar power. The proposal includes hardware in the loop simulation activities that will demonstrate feasibility of the approach. To address the problem, this project will conduct fundamental research on the design of "smart" software-defined solar (SDS) systems that self-regulate the power they let "flow" into the grid. Similar to data transmission in the Internet, SDS systems dynamically regulate the solar energy that flows into the grid to maximize its available solar capacity, maintain a balanced supply and demand, and fairly share the available capacity among connected users. In particular, the project will develop new mechanisms for fairly controlling solar power flows, new protocols for rate-limiting solar flows into the grid, and new policies for leveraging batteries as energy buffers to regulate solar flows. To enable SDS, the project will design new mechanisms for fairly controlling solar output from inverters and charge controllers, new protocols for rate-limiting solar injection into the grid, and new policies for leveraging batteries as energy buffers to regulate solar output. Collectively, these mechanisms and policies will provide the technical foundation for a new class of "networking" protocols for solar energy.

Data-driven cyber-physical systems are ubiquitous in many sectors including manufacturing, automotive, transportation, utilities and health care. This project develops the theory, methods and tools necessary to answer the central question "how can we, in a data-rich world, design and operate cyber-physical systems differently?" The resulting data-driven techniques will transform the design and operation process into one in which data and models - and human designers and operators - continuously and fluently interact. This integrated view promises capabilities beyond its parts. Explicitly integrating data will lead to more efficient decision-making and help reduce the gap from model-based design to system deployment. Furthermore, it will blend design- and run-time tasks, and help develop cyber-physical systems not only for their initial deployment but also for their lifetime. While proposed theory, methods and tools will cut across the spectrum of cyber-physical systems, the project focuses on their implications in the emerging application of additive manufacturing. Even though a substantial amount of engineering time is spent, additive manufacturing processes often fail to produce acceptable geometric, material or electro-mechanical properties. Currently, there is no mechanism for predicting and correcting these systematic, repetitive errors nor to adapt the design process to encompass the peculiarities of this manufacturing style. A data-driven cyber-physical systems perspective has the potential to overcome these challenges in additive manufacturing. The project's education plan focuses on the already much needed transformation of the undergraduate and graduate curricula to train engineers and computer scientists who will create the next-generation of cyber-physical with a data-driven mindset. The team will reach out to K-12 students and educators through a range of activities, and to undergraduate students from underrepresented groups through year-long research projects. All educational material generated by the project will be shared publicly.