This NSF Cyber-Physical Systems (CPS) Frontier project "Verified Human Interfaces, Control, and Learning for Semi-Autonomous Systems (VeHICaL)" is developing the foundations of verified co-design of interfaces and control for human cyber-physical systems (h-CPS) --- cyber-physical systems that operate in concert with human operators. VeHICaL aims to bring a formal approach to designing both interfaces and control for h-CPS, with provable guarantees. The VeHICaL project is grounded in a novel problem formulation that elucidates the unique requirements on h-CPS including not only traditional correctness properties on autonomous controllers but also quantitative requirements on the logic governing switching or sharing of control between human operator and autonomous controller, the user interface, privacy properties, etc. The project is making contributions along four thrusts: (1) formalisms for modeling h-CPS; (2) computational techniques for learning, verification, and control of h-CPS; (3) design and validation of sensor and human-machine interfaces, and (4) empirical evaluation in the domain of semi-autonomous vehicles. The VeHICaL approach is bringing a conceptual shift of focus away from separately addressing the design of control systems and human-machine interaction and towards the joint co-design of human interfaces and control using common modeling formalisms and requirements on the entire system. This co-design approach is making novel intellectual contributions to the areas of formal methods, control theory, sensing and perception, cognitive science, and human-machine interfaces. Cyber-physical systems deployed in societal-scale applications almost always interact with humans. The foundational work being pursued in the VeHICaL project is being validated in two application domains: semi-autonomous ground vehicles that interact with human drivers, and semi-autonomous aerial vehicles (drones) that interact with human operators. A principled approach to h-CPS design --- one that obtains provable guarantees on system behavior with humans in the loop --- can have an enormous positive impact on the emerging national ``smart'' infrastructure. In addition, this project is pursuing a substantial educational and outreach program including: (i) integrating research into undergraduate and graduate coursework, especially capstone projects; (ii) extensive online course content leveraging existing work by the PIs; (iii) a strong undergraduate research program, and (iv) outreach and summer programs for school children with a focus on reaching under-represented groups.

Software-Defined Control (SDC) is a revolutionary methodology for controlling manufacturing systems that uses a global view of the entire manufacturing system, including all of the physical components (machines, robots, and parts to be processed) as well as the cyber components (logic controllers, RFID readers, and networks). As manufacturing systems become more complex and more connected, they become more susceptible to small faults that could cascade into major failures or even cyber-attacks that enter the plant, such as, through the internet. In this project, models of both the cyber and physical components will be used to predict the expected behavior of the manufacturing system. Since the components of the manufacturing system are tightly coupled in both time and space, such a temporal-physical coupling, together with high-fidelity models of the system, allows any fault or attack that changes the behavior of the system to be detected and classified. Once detected and identified, the system will compute new routes for the physical parts through the plant, thus avoiding the affected locations. These new routes will be directly downloaded to the low-level controllers that communicate with the machines and robots, and will keep production operating (albeit at a reduced level), even in the face of an otherwise catastrophic fault. These algorithms will be inspired by the successful approach of Software-Defined Networking. Anomaly detection methods will be developed that can ascertain the difference between the expected (modeled) behavior of the system and the observed behavior (from sensors). Anomalies will be detected both at short time-scales, using high-fidelity models, and longer time-scales, using machine learning and statistical-based methods. The detection and classification of anomalies, whether they be random faults or cyber-attacks, will represent a significant contribution, and enable the re-programming of the control systems (through re-routing the parts) to continue production. The manufacturing industry represents a significant fraction of the US GDP, and each manufacturing plant represents a large capital investment. The ability to keep these plants running in the face of inevitable faults and even malicious attacks can improve productivity -- keeping costs low for both manufacturers and consumers. Importantly, these same algorithms can be used to redefine the production routes (and machine programs) when a new part is introduced, or the desired production volume is changed, to maximize profitability for the manufacturing operation.

Recent years have seen an explosion in the use of cellular and wifi networks to deploy fleets of semi-autonomous physical systems, including unmanned aerial vehicles (UAVs), self-driving vehicles, and weather stations to perform tasks such as package delivery, crop harvesting, and weather prediction. The use of cellular and wifi networks has dramatically decreased the cost, energy, and maintenance associated with these forms of embedded technology, but has also added new challenges in the form of delay, packet drops, and loss of signal. Because of these new challenges, and because of our limited understanding of how unreliable communication affects performance, the current protocols for regulating physical systems over wireless networks are slow, inefficient, and potentially unstable. In this project we develop a new computational framework for designing provably fast, efficient and safe protocols for the control of fleets of semi-autonomous physical systems. The systems considered in this project are dynamic, defined by coupled ordinary differential equations, and connected by feedback to a controller, with a feedback interconnection which has multiple static delays, multiple time-varying delays, or is sampled at discrete times. For these systems, we would like to design optimal and robust feedback controllers assuming a limited number of sensor measurements are available. Specifically, we seek to design a class of algorithms which are computationally efficient, which scale to large numbers of subsystems, and which, given models of the dynamics, communication links, and uncertainty, will return a controller which is provably stable, robust to model uncertainty, and provably optimal in the relevant metric of performance. To accomplish this task, we leverage a new duality result which allows the problem of controller synthesis for infinite-dimensional systems to be convexified. This result allows the problem of optimal and robust dynamic output-feedback controller synthesis to be reformulated as feasibility of a set of convex linear operator inequalities. We then use semidefinite programming to parametrize the set of feasible operators and thereby test feasibility of the inequalities with little to no conservatism. In a similar manner, estimator design and optimal controller synthesis are recast as semidefinite programming problems and used to solve the problems of sampled-data and systems with input delay. The algorithms will be scalable to at least 20 states and the controllers will be field-tested on a fleet of wheeled robotic vehicles.

Coordinated cyber-physical attacks (CCPA) have been touted as a serious threat for several years, where "coordinated" means that attackers have complete knowledge of the physical plant and status, and sometimes can even create physical defects, to assist cyber attacks, and vice versa. In recent years, these attacks have crept from theory to reality, with attacks on vehicles, electrical grids, and industrial plants, which have the potential to cause destruction and even death outside of the digital world. CCPA raise a unique challenge with respect to cyber-physical systems (CPS) safety. Historically, technologies to defend cyber attacks and physical attacks are developed separately under different assumptions and models. For instance, cyber security technologies often require the complete profile of the physical dynamics and the observation of the system state, which may not be available when physical defects exist. Similarly, existing system control techniques may efficiently compensate for the physical damage, but under the assumption that the control software and the sensor data are not compromised. There is a lack of unified approaches against CCPA. With this observation, this project focuses on the development of unified models with coherent set of assumptions, supported by integrated technologies, upon which CCPA can be defended much more effectively. To establish theoretical foundations and engineering principles for resilient CPS architectures, this project will investigate unified models and platforms that represent the scientific understanding of resilient CPS against CCPA. Engineering of CPS will be addressed through the development and integration of complexity-reduced software architectures, along with their design principles, which lead to verifiable and certifiable architectures with higher level of system resilience. Technology of CPS will be addressed through the design of new attack detection, isolation, and recovery tools as well as timing and control techniques to ensure appropriate responses to CCPA. The proposed inherently interdisciplinary research will ensure predictable performance for resilient CPS, by leveraging the disciplinary advances in (i) the design and evaluation of robust fault-tolerant control systems yielding significantly enhanced levels of safety in highly unpredictable environments; (ii) the design and implementation of complexity reduction architecture yielding a significant reduction in the verification time from hours to seconds; (iii) the development of multi-rate sampled-data control and robust reachability-based attack detection techniques ensuring that the sensor data is reliable; and (iv) the development of cyber-physical co-adaptation that optimizes control performance and computation task scheduling to guarantee system safety and efficient recovery from CCPA. The target application of this project is unmanned aerial vehicles (UAVs). The research results will be evaluated in three different testbeds: UAV testbed, generic transportation model (GTM) aircraft, and power system virtual testbed (VTB). The technological advancement from this project will provide solutions for the safety and reliability issues faced by today's CPS and deliver dependable CPS that are applicable without sacrificing functionality or accessibility in complex and potentially hostile networked environment. The results of this project will be communicated in archival journal publications, conference venues and various workshops and lectures, and will be integrated at different academic levels.

Coordinated cyber-physical attacks (CCPA) have been touted as a serious threat for several years, where "coordinated" means that attackers have complete knowledge of the physical plant and status, and sometimes can even create physical defects, to assist cyber attacks, and vice versa. In recent years, these attacks have crept from theory to reality, with attacks on vehicles, electrical grids, and industrial plants, which have the potential to cause destruction and even death outside of the digital world. CCPA raise a unique challenge with respect to cyber-physical systems (CPS) safety. Historically, technologies to defend cyber attacks and physical attacks are developed separately under different assumptions and models. For instance, cyber security technologies often require the complete profile of the physical dynamics and the observation of the system state, which may not be available when physical defects exist. Similarly, existing system control techniques may efficiently compensate for the physical damage, but under the assumption that the control software and the sensor data are not compromised. There is a lack of unified approaches against CCPA. With this observation, this project focuses on the development of unified models with coherent set of assumptions, supported by integrated technologies, upon which CCPA can be defended much more effectively. To establish theoretical foundations and engineering principles for resilient CPS architectures, this project will investigate unified models and platforms that represent the scientific understanding of resilient CPS against CCPA. Engineering of CPS will be addressed through the development and integration of complexity-reduced software architectures, along with their design principles, which lead to verifiable and certifiable architectures with higher level of system resilience. Technology of CPS will be addressed through the design of new attack detection, isolation, and recovery tools as well as timing and control techniques to ensure appropriate responses to CCPA. The proposed inherently interdisciplinary research will ensure predictable performance for resilient CPS, by leveraging the disciplinary advances in (i) the design and evaluation of robust fault-tolerant control systems yielding significantly enhanced levels of safety in highly unpredictable environments; (ii) the design and implementation of complexity reduction architecture yielding a significant reduction in the verification time from hours to seconds; (iii) the development of multi-rate sampled-data control and robust reachability-based attack detection techniques ensuring that the sensor data is reliable; and (iv) the development of cyber-physical co-adaptation that optimizes control performance and computation task scheduling to guarantee system safety and efficient recovery from CCPA. The target application of this project is unmanned aerial vehicles (UAVs). The research results will be evaluated in three different testbeds: UAV testbed, generic transportation model (GTM) aircraft, and power system virtual testbed (VTB). The technological advancement from this project will provide solutions for the safety and reliability issues faced by today's CPS and deliver dependable CPS that are applicable without sacrificing functionality or accessibility in complex and potentially hostile networked environment. The results of this project will be communicated in archival journal publications, conference venues and various workshops and lectures, and will be integrated at different academic levels.