Computer systems are increasingly coming to be relied upon to augment or replace human operators in controlling mechanical devices in contexts such as transportation systems, chemical plants, and medical devices, where safety and correctness are critical. A central problem is how to verify that such partially automated or fully autonomous cyber-physical systems (CPS) are worthy of our trust. One promising approach involves synthesis of the computer implementation codes from formal specifications, by software tools. This project contributes to this "correct-by-construction" approach, by developing scalable, automated methods for the synthesis of control protocols with provable correctness guarantees, based on insights from models of human behavior. It targets: (i) the gap between the capabilities of today's hardly autonomous, unmanned systems and the levels of capability at which they can make an impact on our use of monetary, labor, and time resources; and (ii) the lack of computational, automated, scalable tools suitable for the specification, synthesis and verification of such autonomous systems. The research is based on study of modular reinforcement learning-based models of human behavior derived through experiments designed to elicit information on how humans control complex interactive systems in dynamic environments, including automobile driving. Architectural insights and stochastic models from this study are incorporated with a specification language based on linear temporal logic, to guide the synthesis of adaptive autonomous controllers. Motion planning and other dynamic decision-making are by algorithms based on computational engines that represent the underlying physics, with provision for run-time adaptation to account for changing operational and environmental conditions. Tools implementing this methodology are validated through experimentation in a virtual testing facility in the context of autonomous driving in urban environments and multi-vehicle autonomous navigation of micro-air vehicles in dynamic environments. Education and outreach activities include involvement of undergraduate and graduate students in the research, integration of the research into courses, demonstrations for K-12 students, and recruitment of research participants from under-represented demographic groups. Data, code, and teaching materials developed by the project are disseminated publicly on the Web.

This work examines how to get safety and security in Internet of Things (IoT) systems where multiple devices (things), each designed in isolation from others, are brought together to form a networked system, controlled via one or more software applications ("apps"). "Things" in an IoT environment can include simple devices such as switches, lightbulbs, smart locks, thermostats, and safety alarms as well as complex systems such as appliances, smartphones, and cars. Software IoT "apps" can monitor and control multiple devices in homes, cars, cities, and businesses, providing significant benefits such as energy efficiency, security, safety, and user convenience. Unfortunately, programmable IoT systems also introduce new risks, including enabling remote control by hackers of devices in smart homes, cars, and cities, via buggy IoT apps. Testing IoT apps to remove bugs is currently challenging due to a variety of physical devices with which such apps may interact, including devices that were not even available during app development. The proposed work will help develop techniques for testing IoT apps efficiently and for enforcing safety and security constraints on their run-time behavior. More specifically, the proposed work is centered around three technical thrusts: 1) creating virtual device models to help efficiently test IoT apps systematically without knowing the precise details of physical devices that the apps will control in advance; 2) automating test development for an IoT app to check safety and security specifications against a flexible set of devices; and 3) providing support for enforcement of specifications at run-time for security and safety assertions. The work includes extensive experimentation and evaluation using diverse devices and will represent a significant advance in hardening this important spaces

Scaling the Internet of Things (IoT) to billions and possibly trillions of "things" requires transformative advances in the science, technology, and engineering of cyber-physical systems (CPS), with none more pressing or challenging than the power problem. Consider that if every device in a 1 trillion IoT network had a battery that lasted for a full five years, over 500 million batteries would need to be changed every day. Clearly, a battery-powered IoT is not feasible at this scale due to both human resource logistics and environmental concerns. There is a need for a battery-less approach that dependably meets functionality requirements using energy harvested from the physical world. This project brings together experts in materials, devices, circuits, and systems to pursue a holistic approach to self-powered wireless devices deployed in real-world environments and IoT systems and applications. In addition, educational and outreach activities will help develop the workforce for this relatively new field with the holistic, materials-to-systems perspective that will be necessary to lead innovation in this space.A critical challenge that this project addresses is that both optimal device operation and energy harvester efficiency are heavily dependent on physical world dynamics, and thus, self-powered devices that are statically configured or that just respond to instantaneous conditions are unlikely to provide the dependability required for many IoT systems and applications. To address this fundamental and critically enabling challenge, data collections will be performed to study the physical world dynamics that impact device operation and harvester efficiency, such as ambient conditions, electromagnetic interference, and human behavior. This scientific study will lead to the development of dynamic models that will, in turn, be used to develop algorithms to dynamically configure devices and harvesters based not only on past and current conditions but also on predictions of future conditions. These algorithms will then be used to dynamically configure technological innovations in ultra-low power device operation and ultra-high efficiency energy harvesting to engineer and operate dependable self-powered things for the IoT.

By 2050, 70% of the world's population is projected to live and work in cities, with buildings as major constituents. Buildings' energy consumption contributes to more than 70% of electricity use, with people spending more than 90% of their time in buildings. Future cities with innovative, optimized building designs and operations have the potential to play a pivotal role in reducing energy consumption, curbing greenhouse gas emissions, and maintaining stable electric-grid operations. Buildings are physically connected to the electric power grid, thus it would be beneficial to understand the coupling of decisions and operations of the two. However, at a community level, there is no holistic framework that buildings and power grids can simultaneously utilize to optimize their performance. The challenge related to establishing such a framework is that building control systems are neither connected to, nor integrated with the power grid, and consequently a unified, global optimal energy control strategy at a smart community level cannot be achieved. Hence, the fundamental knowledge gaps are (a) the lack of a holistic, multi-time scale mathematical framework that couples the decisions of buildings stakeholders and grid stakeholders, and (b) the lack of a computationally-tractable solution methodology amenable to implementation on a large number of connected power grid-nodes and buildings. In this project, a novel mathematical framework that fills the aforementioned knowledge gaps will be investigated, and the following hypothesis will be tested: Connected buildings, people, and grids will achieve significant energy savings and stable operation within a smart city. The envisioned smart city framework will furnish individual buildings and power grid devices with custom demand response signals. The hypothesis will be tested against classical demand response (DR) strategies where (i) the integration of building and power-grid dynamics is lacking and (ii) the DR schemes that buildings implement are independent and individual. By engaging in efficient, decentralized community-scale optimization, energy savings will be demonstrated for participating buildings and enhanced stable operation for the grid are projected, hence empowering smart energy communities. To ensure the potential for broad adoption of the proposed framework, this project will be regularly informed with inputs and feedback from Southern California Edison (SCE). In order to test the hypothesis, the following research products will be developed: (1) An innovative method to model a cluster of buildings--with people's behavior embedded in the cluster's dynamics--and their controls so that they can be integrated with grid operation and services; (2) a novel optimization framework to solve complex control problems for large-scale coupled systems; and (3) a methodology to assess the impacts of connected buildings in terms of (a) the grid's operational stability and safety and (b) buildings' optimized energy consumption. To test the proposed framework, a large-scale simulation of a distribution primary feeder with over 1000 buildings will be conducted within SCE?s Johanna and Santiago substations in Central Orange County.