Errors in cyber-physical systems can lead to disastrous consequences. Classic examples date back to the Therac-25 radiation incidents in 1987 and the Ariane 5 rocket crash in 1996. More recently, Toyota's unintended acceleration bug was caused by software errors, and certain cars were found vulnerable to attacks that can take over key parts of the control software, allowing attackers to even disable the brakes remotely. Pacemakers have also been found vulnerable to attacks that can cause deadly consequences for the patient. To reduce the chances of such errors happening, this project investigates the application of a technique called Foundational Verification to cyber-physical systems. In Foundational Verification, the system being developed is proved correct, in full formal detail, using a proof assistant. The main intellectual merit of the proposal is the attainment of previously unattainable levels of safety for cyber-physical systems because proofs in Foundational Verification are carried out in complete detail. To ensure that the techniques in this project are practical, they are evaluated within the context of a real flying quadcopter. The project's broader significance and importance is the improved correctness, safety and security of cyber-physical systems. In particular, this project lays the foundation for ushering in a new level of formal correctness for cyber-physical systems. Although the initial work focuses on quadcopters, the concepts, ideas, and research contributions have the potential for transformative impact on other kinds of systems, including power-grid software, cars, avionics and medical devices (from pacemakers and insulin pumps to defibrillators and radiation machines).

Strategic decision-making for physical-world infrastructures is rapidly transitioning toward a pervasively cyber-enabled paradigm, in which human stakeholders and automation leverage the cyber-infrastructure at large (including on-line data sources, cloud computing, and handheld devices). This changing paradigm is leading to tight coupling of the cyber- infrastructure with multiple physical- world infrastructures, including air transportation and electric power systems. These management-coupled cyber- and physical- infrastructures (MCCPIs) are subject to complex threats from natural and sentient adversaries, which can enact complex propagative impacts across networked physical-, cyber-, and human elements. We propose here to develop a modeling framework and tool suite for threat assessment for MCCPIs. The proposed modeling framework for MCCPIs has three aspects: 1) a tractable moment-linear modeling paradigm for the hybrid, stochastic, and multi-layer dynamics of MCCPIs; 2) models for sentient and natural adversaries, that capture their measurement and actuation capabilities in the cyber- and physical- worlds, intelligence, and trust-level; and 3) formal definitions for information security and vulnerability. The attendant tool suite will provide situational awareness of the propagative impacts of threats. Specifically, three functionalities termed Target, Feature, and Defend will be developed, which exploit topological characteristics of an MCCPI to evaluate and mitigate threat impacts. We will then pursue analyses that tie special infrastructure-network features to security/vulnerability. As a central case study, the framework and tools will be used for threat assessment and risk analysis of strategic air traffic management. Three canonical types of threats will be addressed: environmental-to-physical threats, cyber-physical co-threats, and human-in-the-loop threats. This case study will include development and deployment of software decision aids for managing man-made disturbances to the air traffic system.

The objective of this work is to generate new fundamental science that enables the operation of cyber-physical systems through complex environments. Predicting how a system will behave in the future requires more computing power if that system is complex. Navigating through environments with many obstacles could require significant computing time, which may delay the issue of decisions that have to be made by the on-board algorithms. Fortunately, systems do not always need the most accurate model to predict their behavior. This project develops new theory for deciding between the best model to use when making a decision in real time. The approach involves switching between different predictive models of the system, depending on the computational burden of the associated controller, and the accuracy that the predictive model provides. These tools will pave the way for more kinds of aircraft to navigate closely and safely with one another through the National Air Space (NAS), including Unmanned Air Systems (UAS). The results from this project will enable more accurate and faster trajectory synthesis for controllers with nonlinear plants, or nonlinear constraints that encode obstacles. The approach utilizes hybrid control to switch between models whose accuracy is normalized by their computational burden of predictive control methods. This synergistic approach enables computationally-aware cyber-physical systems (CPSs), in which model accuracy can be jointly considered with computational requirements. The project advances the knowledge on modeling, analysis, and design of CPSs that utilize predictive methods for trajectory synthesis under constraints in real-time cyber-physical systems. The results will include methods for the design of algorithms that adapt to the computational limitations of autonomous and semi-autonomous systems while satisfying stringent timing and safety requirements. With these methods come new tools to account for computational capabilities in real-time, and new hybrid feedback algorithms and prediction schemes that exploit computational capabilities to arrive at more accurate predictions within the time constraints. The algorithms will be modeled in terms of hybrid dynamical systems, to guarantee dynamical properties of interest. The problem space will draw from models of UAS in the NAS.

The objective of this work is to generate new fundamental science that enables the operation of cyber-physical systems through complex environments. Predicting how a system will behave in the future requires more computing power if that system is complex. Navigating through environments with many obstacles could require significant computing time, which may delay the issue of decisions that have to be made by the on-board algorithms. Fortunately, systems do not always need the most accurate model to predict their behavior. This project develops new theory for deciding between the best model to use when making a decision in real time. The approach involves switching between different predictive models of the system, depending on the computational burden of the associated controller, and the accuracy that the predictive model provides. These tools will pave the way for more kinds of aircraft to navigate closely and safely with one another through the National Air Space (NAS), including Unmanned Air Systems (UAS). The results from this project will enable more accurate and faster trajectory synthesis for controllers with nonlinear plants, or nonlinear constraints that encode obstacles. The approach utilizes hybrid control to switch between models whose accuracy is normalized by their computational burden of predictive control methods. This synergistic approach enables computationally-aware cyber-physical systems (CPSs), in which model accuracy can be jointly considered with computational requirements. The project advances the knowledge on modeling, analysis, and design of CPSs that utilize predictive methods for trajectory synthesis under constraints in real-time cyber-physical systems. 
 The results will include methods for the design of algorithms that adapt to the computational limitations of autonomous and semi-autonomous systems while satisfying stringent timing and safety requirements. With these methods come new tools to account for computational capabilities in real-time, and new hybrid feedback algorithms and prediction schemes that exploit computational capabilities to arrive at more accurate predictions within the time constraints. The algorithms will be modeled in terms of hybrid dynamical systems, to guarantee dynamical properties of interest. The problem space will draw from models of UAS in the NAS.

Strategic decision-making for physical-world infrastructures is rapidly transitioning toward a pervasively cyber-enabled paradigm, in which human stakeholders and automation leverage the cyber-infrastructure at large (including on-line data sources, cloud computing, and handheld devices). This changing paradigm is leading to tight coupling of the cyber- infrastructure with multiple physical- world infrastructures, including air transportation and electric power systems. These management-coupled cyber- and physical- infrastructures (MCCPIs) are subject to complex threats from natural and sentient adversaries, which can enact complex propagative impacts across networked physical-, cyber-, and human elements. We propose here to develop a modeling framework and tool suite for threat assessment for MCCPIs. The proposed modeling framework for MCCPIs has three aspects: 1) a tractable moment-linear modeling paradigm for the hybrid, stochastic, and multi-layer dynamics of MCCPIs; 2) models for sentient and natural adversaries, that capture their measurement and actuation capabilities in the cyber- and physical- worlds, intelligence, and trust-level; and 3) formal definitions for information security and vulnerability. The attendant tool suite will provide situational awareness of the propagative impacts of threats. Specifically, three functionalities termed Target, Feature, and Defend will be developed, which exploit topological characteristics of an MCCPI to evaluate and mitigate threat impacts. We will then pursue analyses that tie special infrastructure-network features to security/vulnerability. As a central case study, the framework and tools will be used for threat assessment and risk analysis of strategic air traffic management. Three canonical types of threats will be addressed: environmental-to-physical threats, cyber-physical co-threats, and human-in-the-loop threats. This case study will include development and deployment of software decision aids for managing man-made disturbances to the air traffic system.

During the last decade, we have witnessed a rapid penetration of autonomous systems technology into aerial, road, underwater, and sea vehicles. The autonomy assumed by these vehicles holds the potential to increase performance significantly, for instance, by reducing delays and increasing capacity, while enhancing safety, in a number of transportation systems. However, to exploit the full potential of these autonomy-enabled transportation systems, we must rethink transportation networks and control algorithms that coordinate autonomous vehicles operating on such networks. This project focuses on the design and operation of autonomy-enabled transportation networks that provide provable guarantees on achieving high performance and maintaining safety at all times. The foundational problems arising in this domain involve taking into account the physics governing the vehicles in order to coordinate them using cyber means. This research effort aims to advance the science of cyber-physical systems by following a unique and radical approach, drawing inspiration and techniques from non-equilibrium statistical mechanics and self-organizing systems, and blending this inspiration with the foundational tools of queueing theory, control theory, and optimization. This approach may allow orders of magnitude improvement in the servicing capabilities of various transportation networks for moving goods or people. The applications include the automation of warehouses, factory floors, sea ports, aircraft carrier decks, transportation networks involving driverless cars, drone-enabled delivery networks, air traffic management, and military logistics networks. The project also aims to start a new wave of classes and tutorials that will create trained engineers and a research community in the area of safe and efficient transportation networks enabled by autonomous cyber-physical systems.