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.

Securing critical networked cyber-physical systems (NCPSs) such as the power grid or transportation systems has emerged as a major national and global priority. The networked nature of such systems renders them vulnerable to a range of attacks both in cyber and physical domains as corroborated by recent threats such as the Stuxnet worm. Developing security mechanisms for such NCPSs significantly differs from traditional networked systems due to interdependence between cyber and physical subsystems (with attacks originating from either subsystem), possible cooperation between attackers or defenders, and the presence of human decision makers in the loop. The main goal of this research is to develop the necessary science and engineering tools for designing NCPS security solutions that are applicable to a broad range of application domains. This project will develop a multidisciplinary framework that weaves together principles from cybersecurity, control theory, networking and criminology. The framework will include novel security mechanisms for NCPSs founded on solid control-theoretic and related notions, analytical tools that allow incorporation of bounded human rationality in NCPS security, and experiments with real-world attack scenarios. A newly built cross-institutional NCPS simulator will be used to evaluate the proposed mechanisms in realistic environments. This research transcends specific cyber-physical systems domains and provides the necessary tools to building secure and trustworthy NCPSs. The broader impacts include a new infrastructure for NCPS research and education, training of students, new courses, and outreach events focused on under-represented student groups.

Securing critical networked cyber-physical systems (NCPSs) such as the power grid or transportation systems has emerged as a major national and global priority. The networked nature of such systems renders them vulnerable to a range of attacks both in cyber and physical domains as corroborated by recent threats such as the Stuxnet worm. Developing security mechanisms for such NCPSs significantly differs from traditional networked systems due to interdependence between cyber and physical subsystems (with attacks originating from either subsystem), possible cooperation between attackers or defenders, and the presence of human decision makers in the loop. The main goal of this research is to develop the necessary science and engineering tools for designing NCPS security solutions that are applicable to a broad range of application domains. This project will develop a multidisciplinary framework that weaves together principles from cybersecurity, control theory, networking and criminology. The framework will include novel security mechanisms for NCPSs founded on solid control-theoretic and related notions, analytical tools that allow incorporation of bounded human rationality in NCPS security, and experiments with real-world attack scenarios. A newly built cross-institutional NCPS simulator will be used to evaluate the proposed mechanisms in realistic environments. This research transcends specific cyber-physical systems domains and provides the necessary tools to building secure and trustworthy NCPSs. The broader impacts include a new infrastructure for NCPS research and education, training of students, new courses, and outreach events focused on under-represented student groups.

The project focuses on swarming cyber-physical systems (swarming CPS) consisting of a collection of mobile networked agents, each of which has sensing, computing, communication, and locomotion capabilities, and that have a wide range of civilian and military applications. Different from conventional static CPS, swarming CPS rely on mobile computing entities, e.g., robots, which collaboratively interact with phenomena of interest at different physical locations. This unique feature calls for novel sensing-motion co-design solutions to accomplish a variety of increasingly complex missions. Towards this, the overall research objective of this project is to establish and demonstrate a generic motion-sensing co-design procedure that will significantly reduce the complexity of the mission design for swarming CPS, and greatly facilitate the development of effective, efficient and adaptive control and sensing strategies under various environment uncertainties. This project aims to offer comprehensive scientific understanding of the dynamic nature of swarming CPS, contribute to generic engineering principles for designing collaborative control and sensing algorithms, and advance the enabling technologies of practically applying CPS in the challenging environment. The research solutions of this project aim to bring significant advance in the environmental sustainability, homeland security, and human well-being. The project provides unique interdisciplinary training opportunities for graduate and undergraduate students through both research work and related courses that the PIs will develop and offer. The project significantly advances the state of the art in cooperative control and sensing and provide an enabling technology for swarming CPS through highly interrelated thrusts: (1) a generic sensing and motion co-design procedure, which reveals the fundamental interplay between the sensing dynamics and motion dynamics of swarming CPS, will be proposed to facilitate the development of effective and efficient control and sensing strategies; (2) by following such co-design procedure, provable correct, computation efficient, and communication light control and sensing strategies will be developed for swarming CPS with constrained resources to accomplish specific missions, e.g., locating pollutants, in an unknown field, while navigating through uncertain spaces; (3) to provide an enabling mobile platform to verify the proposed strategies, innovative small, highly 3D maneuverable, noiseless, energy-efficient, and robust robotic fish fully actuated by smart material will be designed to meet the maneuvering requirements of the proposed algorithms; (4) novel Magnetic Induction (MI)-based underwater communication and localization solutions will be developed, which allows robotic fish to timely and reliably exchange messages, while simultaneously providing accurate inter-fish localization in the harsh 3D underwater environment; and (5) the proposed sensing-motion co-design strategies will be verified and demonstrated using a school of wirelessly interconnected robotic fish in both lab-based experiments and field experiments.

Enhanced Structural Health Monitoring of Civil Infrastructure Systems by Observing and Controlling Loads using a Cyber-Physical System Framework The economic prosperity of the nation is dependent on vast networks of civil infrastructure systems. Unfortunately, large fractions of these infrastructure systems are rapidly approaching the end of their intended design lives. The national network of highway bridges is especially vulnerable to age-based deterioration as revealed by recent catastrophic bridge collapses in the United States. Two major bottlenecks currently exist that severely limit the effectiveness of existing bridge health management methods. First, the causal relationship between repeated truck loading and long-term structural deterioration is not well understood. Second, current management methods are reliant on visual inspections which only provide qualitative information regarding bridge health and introduce subjectivity in post-inspection decision making. This project aims to resolve these major bottlenecks by advancing a cyber-physical system (CPS) designed to monitor the health of highway bridges, control the loads imposed on bridges by heavy trucks, and provide visual inspectors with quantitative information for data-driven bridge health assessments. The CPS framework created will have enormous impact on the national economy by enhancing public safety while dramatically improving the cost-effectiveness of infrastructure management methods. The project will also create publically available graduate-level course curricula focused on CPS technology and engages inner-city middle-school students from underrepresented groups to prepare them to pursue careers in the science, technology, engineering, and mathematics (STEM) fields. The overarching goal of the research project is to create a scalable and robust CPS framework for the observation and control of mobile agents that asynchronously and transiently interact with a stationary physical system. While this class of problem is found throughout many engineering disciplines, the project focuses on the health management of highway bridges. The mobile agents relevant to bridge health are the trucks that load and introduce long-term damage in the bridge and inspectors who visually inspect the bridge. The task of devising a robust CPS framework will be challenged by the highly transient nature of the agents involved. Specifically, the compressed time of interaction between the truck and bridge results in tight time constraints on observation, quantification and control of the truck's loading. The project will rely on ad-hoc wireless communications to seamlessly integrate sensors embedded in the mobile agents (trucks and inspectors) with wireless sensors installed on the bridge and with servers dedicated to cloud-based analytics located on the Internet. The project will design the CPS framework to quantify in real-time truck loads based on sensor data streaming into the CPS framework. A distributed computing architecture will be created for the CPS framework to automate the decomposition of computational tasks in order to dramatically improve the speed and efficiency of the framework's data processing capabilities. Finally, the CPS framework will establish ad-hoc feedback control of the mobile agents in order to control mobile agent-stationary system interactions. In particular, feedback control of an instrumented truck allows the CPS framework to control the loads imposed on the bridge for improved health assessments. The CPS framework will be further extended to control visual inspection processes by providing inspectors with recommend inspection actions based on rigorous analysis of collected sensor data. The intellectual significance of the CPS framework is that it observes and controls truck loads on highway bridges for the first time while creating an entirely new data-driven paradigm for more accurate health assessment of infrastructure systems.

Advances in technology mean that computer-controlled physical devices that currently still require human operators, such as automobiles, trains, airplanes, and medical treatment systems, could operate entirely autonomously and make rational decisions on their own. Autonomous cars and drones are a concrete and highly publicized face of this dream. Before this dream can be realized we must address the need for safety - the guaranteed absence of undesirable behaviors emerging from autonomy. Highly publicized technology accidents such as rocket launch failures, uncontrolled exposure to radiation during treatment, aircraft automation failures and unintended automotive accelerations serve as warnings of what can happen if safety is not adequately addressed in the design of such cyber-physical systems. One approach for safety analysis is the use of software tools that apply formal logic to prove the absence of undesired behavior in the control software of a system. In prior work, this approach this been proven to work for simple controller software that is generated automatically by tools from abstract models like Simulink diagrams. However, autonomous decision making requires more complex software that is able to solve optimization problems in real time. Formal verification of control software that includes such optimization algorithms remains an unmet challenge. The project SORTIES (Semantics of Optimization for Real Time Intelligent Embedded Systems) draws upon expertise in optimization theory, control theory, and computer science to address this challenge. Beginning with the convergence properties of convex optimization algorithms, SORTIES examines how these properties can be automatically expressed as inductive invariants for the software implementation of the algorithms, and then incorporates these properties inside the source code itself as formal annotations which convey the underlying reasoning to the software engineer and to existing computer-aided verification tools. The SORTIES goal is an open-source-semantics-carrying autocoder, which takes an optimization algorithm and its convergence properties as input, and produces annotated, verifiable code as output. The demonstration of the tool on several examples, such as a Mars lander, an aircraft avionics system, and a jet engine controller, shows that the evidence of quality produced by annotations is fully compatible with its application to truly functional products. Project research is integrated with education through training of "tri-lingual" professionals, who are equally conversant in system operation, program analysis, and the theory of control and optimization.

The project focuses on swarming cyber-physical systems (swarming CPS) consisting of a collection of mobile networked agents, each of which has sensing, computing, communication, and locomotion capabilities, and that have a wide range of civilian and military applications. Different from conventional static CPS, swarming CPS rely on mobile computing entities, e.g., robots, which collaboratively interact with phenomena of interest at different physical locations. This unique feature calls for novel sensing-motion co-design solutions to accomplish a variety of increasingly complex missions. Towards this, the overall research objective of this project is to establish and demonstrate a generic motion-sensing co-design procedure that will significantly reduce the complexity of the mission design for swarming CPS, and greatly facilitate the development of effective, efficient and adaptive control and sensing strategies under various environment uncertainties. This project aims to offer comprehensive scientific understanding of the dynamic nature of swarming CPS, contribute to generic engineering principles for designing collaborative control and sensing algorithms, and advance the enabling technologies of practically applying CPS in the challenging environment. The research solutions of this project aim to bring significant advance in the environmental sustainability, homeland security, and human well-being. The project provides unique interdisciplinary training opportunities for graduate and undergraduate students through both research work and related courses that the PIs will develop and offer. The project significantly advances the state of the art in cooperative control and sensing and provide an enabling technology for swarming CPS through highly interrelated thrusts: (1) a generic sensing and motion co-design procedure, which reveals the fundamental interplay between the sensing dynamics and motion dynamics of swarming CPS, will be proposed to facilitate the development of effective and efficient control and sensing strategies; (2) by following such co-design procedure, provable correct, computation efficient, and communication light control and sensing strategies will be developed for swarming CPS with constrained resources to accomplish specific missions, e.g., locating pollutants, in an unknown field, while navigating through uncertain spaces; (3) to provide an enabling mobile platform to verify the proposed strategies, innovative small, highly 3D maneuverable, noiseless, energy-efficient, and robust robotic fish fully actuated by smart material will be designed to meet the maneuvering requirements of the proposed algorithms; (4) novel Magnetic Induction (MI)-based underwater communication and localization solutions will be developed, which allows robotic fish to timely and reliably exchange messages, while simultaneously providing accurate inter-fish localization in the harsh 3D underwater environment; and (5) the proposed sensing-motion co-design strategies will be verified and demonstrated using a school of wirelessly interconnected robotic fish in both lab-based experiments and field experiments.

Recent developments in nanotechnology and synthetic biology have enabled a new direction in biological engineering: synthesis of collective behaviors and spatio-temporal patterns in multi-cellular bacterial and mammalian systems. This will have a dramatic impact in such areas as amorphous computing, nano-fabrication, and, in particular, tissue engineering, where patterns can be used to differentiate stem cells into tissues and organs. While recent technologies such as tissue- and organoid on-a-chip have the potential to produce a paradigm shift in tissue engineering and drug development, the synthesis of user-specified, emergent behaviors in cell populations is a key step to unlock this potential and remains a challenging, unsolved problem. This project brings together synthetic biology and micron-scale mobile robotics to define the basis of a next-generation cyber-physical system (CPS) called biological CPS (bioCPS). Synthetic gene circuits for decision making and local communication among the cells are automatically synthesized using a Bio-Design Automation (BDA) workflow. A Robot Assistant for Communication, Sensing, and Control in Cellular Networks (RA), which is designed and built as part of this project, is used to generate desired patterns in networks of engineered cells. In RA, the engineered cells interact with a set of micro-robots that implement control, sensing, and long-range communication strategies needed to achieve the desired global behavior. The micro-robots include both living and non-living matter (engineered cells attached to inorganic substrates that can be controlled using externally applied fields). This technology is applied to test the formation of various patterns in living cells. The project has a rich education and outreach plan, which includes nationwide activities for CPS education of high-school students, lab tours and competitions for high-school and undergraduate students, workshops, seminars, and courses for graduate students, as well as specific initiatives for under-represented groups. Central to the project is the development of theory and computational tools that will significantly advance that state of the art in CPS at large. A novel, formal methods approach is proposed for synthesis of emergent, global behaviors in large collections of locally interacting agents. In particular, a new logic whose formulas can be efficiently learned from quad-tree representations of partitioned images is developed. The quantitative semantics of the logic maps the synthesis of local control and communication protocols to an optimization problem. The project contributes to the nascent area of temporal logic inference by developing a machine learning method to learn temporal logic classifiers from large amounts of data. Novel abstraction and verification techniques for stochastic dynamical systems are defined and used to verify the correctness of the gene circuits in the BDA workflow.

The project focuses on swarming cyber-physical systems (swarming CPS) consisting of a collection of mobile networked agents, each of which has sensing, computing, communication, and locomotion capabilities, and that have a wide range of civilian and military applications. Different from conventional static CPS, swarming CPS rely on mobile computing entities, e.g., robots, which collaboratively interact with phenomena of interest at different physical locations. This unique feature calls for novel sensing-motion co-design solutions to accomplish a variety of increasingly complex missions. Towards this, the overall research objective of this project is to establish and demonstrate a generic motion-sensing co-design procedure that will significantly reduce the complexity of the mission design for swarming CPS, and greatly facilitate the development of effective, efficient and adaptive control and sensing strategies under various environment uncertainties. This project aims to offer comprehensive scientific understanding of the dynamic nature of swarming CPS, contribute to generic engineering principles for designing collaborative control and sensing algorithms, and advance the enabling technologies of practically applying CPS in the challenging environment. The research solutions of this project aim to bring significant advance in the environmental sustainability, homeland security, and human well-being. The project provides unique interdisciplinary training opportunities for graduate and undergraduate students through both research work and related courses that the PIs will develop and offer. The project significantly advances the state of the art in cooperative control and sensing and provide an enabling technology for swarming CPS through highly interrelated thrusts: (1) a generic sensing and motion co-design procedure, which reveals the fundamental interplay between the sensing dynamics and motion dynamics of swarming CPS, will be proposed to facilitate the development of effective and efficient control and sensing strategies; (2) by following such co-design procedure, provable correct, computation efficient, and communication light control and sensing strategies will be developed for swarming CPS with constrained resources to accomplish specific missions, e.g., locating pollutants, in an unknown field, while navigating through uncertain spaces; (3) to provide an enabling mobile platform to verify the proposed strategies, innovative small, highly 3D maneuverable, noiseless, energy-efficient, and robust robotic fish fully actuated by smart material will be designed to meet the maneuvering requirements of the proposed algorithms; (4) novel Magnetic Induction (MI)-based underwater communication and localization solutions will be developed, which allows robotic fish to timely and reliably exchange messages, while simultaneously providing accurate inter-fish localization in the harsh 3D underwater environment; and (5) the proposed sensing-motion co-design strategies will be verified and demonstrated using a school of wirelessly interconnected robotic fish in both lab-based experiments and field experiments.

In the next few decades, autonomous vehicles will become an integral part of the traffic flow on highways. However, they will constitute only a small fraction of all vehicles on the road. This research develops technologies to employ autonomous vehicles already in the stream to improve traffic flow of human-controlled vehicles. The goal is to mitigate undesirable jamming, traffic waves, and to ultimately reduce the fuel consumption. Contemporary control of traffic flow, such as ramp metering and variable speed limits, is largely limited to local and highly aggregate approaches. This research represents a step towards global control of traffic using a few autonomous vehicles, and it provides the mathematical, computational, and engineering structure to address and employ these new connections. Even if autonomous vehicles can provide only a small percentage reduction in fuel consumption, this will have a tremendous economic and environmental impact due to the heavy dependence of the transportation system on non-renewable fuels. The project is highly collaborative and interdisciplinary, involving personnel from different disciplines in engineering and mathematics. It includes the training of PhD students and a postdoctoral researcher, and outreach activities to disseminate traffic research to the broader public. This project develops new models, computational methods, software tools, and engineering solutions to employ autonomous vehicles to detect and mitigate traffic events that adversely affect fuel consumption and congestion. The approach is to combine the data measured by autonomous vehicles in the traffic flow, as well as other traffic data, with appropriate macroscopic traffic models to detect and predict congestion trends and events. Based on this information, the loop is closed by carefully following prescribed velocity controllers that are demonstrated to reduce congestion. These controllers require detection and response times that are beyond the limit of a human's ability. The choice of the best control strategy is determined via optimization approaches applied to the multiscale traffic model and suitable fuel consumption estimation. The communication between the autonomous vehicles, combined with the computational and control tasks on each individual vehicle, require a cyber-physical approach to the problem. This research considers new types of traffic models (micro-macro models, network approaches for higher-order models), new control algorithms for traffic flow regulation, and new sensing and control paradigms that are enabled by a small number of controllable systems available in a flow.