Title: Efficient Traffic Management: A Formal Methods Approach The objective of this project is to develop a formal methods approach to traffic management. Formal methods is an area of computer science that develops efficient techniques for proving the correct operation of systems, such as computer programs and digital circuits, and for designing systems that are correct by construction. This project extends this formalism to traffic networks where correctness specifications include eliminating congestion, ensuring that the freeway throughput remains over a minimum threshold, that queues are always eventually emptied, etc. The task is then to design signal timing and ramp metering strategies to meet such specifications. To accomplish this task, the project takes advantage of the inherent structure of existing, validated mathematical models of traffic flow and develops computationally efficient design techniques. The results are tested with real traffic data from the Interstate 210 travel corridor in Southern California. The educational component of the project includes course development on modeling and control of traffic networks, featuring in particular the formal methods approach of this project, and organizing workshops to train traffic engineers and operation practitioners on the use of software tools and methodologies of the project. To meet rich control objectives expressed using temporal logic, the project exploits the piecewise affine nature of existing, validated traffic models, and derives efficient finite state abstractions that form the basis of correct-by-construction control synthesis. To ensure scalability, the project further takes advantage of inherent monotonicity properties and decomposibility into sparsely connected subsystems. The first research task is to develop a design framework for signal timing and ramp metering strategies for signalized intersections and freeway traffic control. The second task is the coordinated control of freeway onramps and nearby signalized intersections to address situations such as a freeway demand surge after a sporting event, or an accident on the freeway when signal settings must be adjusted to favor a detour route. The third task is to pursue designs that exploit the statistics of demand for probabilistic correctness guarantees, as well as designs that incorporate optimality requirements, such as minimizing travel time. Validation of the results is pursued with high-fidelity simulation models calibrated using traffic data from the Interstate 210 travel corridor.

Title: Efficient Traffic Management: A Formal Methods Approach The objective of this project is to develop a formal methods approach to traffic management. Formal methods is an area of computer science that develops efficient techniques for proving the correct operation of systems, such as computer programs and digital circuits, and for designing systems that are correct by construction. This project extends this formalism to traffic networks where correctness specifications include eliminating congestion, ensuring that the freeway throughput remains over a minimum threshold, that queues are always eventually emptied, etc. The task is then to design signal timing and ramp metering strategies to meet such specifications. To accomplish this task, the project takes advantage of the inherent structure of existing, validated mathematical models of traffic flow and develops computationally efficient design techniques. The results are tested with real traffic data from the Interstate 210 travel corridor in Southern California. The educational component of the project includes course development on modeling and control of traffic networks, featuring in particular the formal methods approach of this project, and organizing workshops to train traffic engineers and operation practitioners on the use of software tools and methodologies of the project. To meet rich control objectives expressed using temporal logic, the project exploits the piecewise affine nature of existing, validated traffic models, and derives efficient finite state abstractions that form the basis of correct-by-construction control synthesis. To ensure scalability, the project further takes advantage of inherent monotonicity properties and decomposibility into sparsely connected subsystems. The first research task is to develop a design framework for signal timing and ramp metering strategies for signalized intersections and freeway traffic control. The second task is the coordinated control of freeway onramps and nearby signalized intersections to address situations such as a freeway demand surge after a sporting event, or an accident on the freeway when signal settings must be adjusted to favor a detour route. The third task is to pursue designs that exploit the statistics of demand for probabilistic correctness guarantees, as well as designs that incorporate optimality requirements, such as minimizing travel time. Validation of the results is pursued with high-fidelity simulation models calibrated using traffic data from the Interstate 210 travel corridor.

The goal of this project is to establish a theoretical and empirical foundation for secured and efficient energy resource management in the smart grid - a typical energy-based cyber-physical system and the future critical energy infrastructure for the nation. However, as a large distributed and complex system, the smart grid inherently operates under the presence of various uncertainties, which can be raised from natural disasters, malicious attacks, distributed renewable energy resources, plug-in electrical vehicles, habits of energy usage, and weather. These uncertainties make the development of a secured and efficient energy resource management system challenging. To address this challenging problem, a novel modeling framework and techniques to deal with these uncertainties will be developed. Threats and their impact on both system operations and end users will be studied and effective defensive schemes will be developed. The outcomes of this project will have broader impacts on the higher education system and national economy and will provide a scientific foundation for designing a secured and efficient energy-based critical infrastructure. The contributions of this project include: a theoretical framework, techniques, and toolkits for smart grid research and education. Specifically, a modeling framework for secured and efficient energy resource management will be developed to quantify uncertainties from both the cyber and physical power grids. Techniques based on statistical modeling, data mining, forecasting, and others will be developed to manage energy resources efficiently. Based on the developed framework, the space of attacks against system operations and end users from key function modules, attack venue, abilities of adversaries, and system knowledge will be studied systematically. Based on the deep understanding of attacks, novel schemes to prevent, detect, and attribute attacks will be developed. An integrated cyber and physical power grid simulation tool and testbed will be developed to evaluate the proposed modeling framework and techniques using realistic scenarios. This project will integrate research, education, and outreach. The outcomes of the project will be integrated into curriculum development and provide research and educational opportunities for both graduate and undergraduate students, including underrepresented minorities and CyberCorps: Scholarship for Service students.

This NSF-FDA Scholar-In-Residence award supports translational research in modeling to inform future medical device design and approval processes. It is supported by the NSF Cyber-Physical Systems program in the Division of Computer and Network Systems in the Directorate for Computer and Information Science and Engineering. Sudden cardiac death is the leading cause of fatalities in the industrialized world. One in five people in the United States is affected by some sort of heart disease and one third of all deaths are due to cardiac diseases with an economic impact of about $200 billion a year. Most of these deaths result from arrhythmias, particularly fibrillation, which is rapid, disorganized electrical activity. The classification of arrhythmias as either reentrant or focal is of clinical significance, yet is difficult to assess. The FDA is responsible for regulating the systems and algorithms that aim to make this important differentiation. Such differentiation is a complex task involving the analysis of complex spatio-temporal patterns of electrical activity. The objectives of this project are to identify the key features of fibrillation that models should represent, to compare how well (or poorly) existing models correspond to measured values of these features, and to develop models that better represent fibrillation. The project develops and extends cell and tissue models and explores the analysis of clinical, experimental and simulation data from the perspective of regulatory science at the FDA, including verification, validation, and uncertainty quantification (VVUQ). The project seeks to 1) validate and create new models that reproduce not only single-cell dynamics, but also experimental and clinically relevant physiological dynamics in tissue and 2) initiate a new developmental framework that the FDA can use not only to test cardiac electrophysiology devices but also to characterize and verify massive submissions of therapeutic compounds obtained by computer-aided drug design methods. The research is conducted in collaboration with the Center for Devices and Radiological Health at FDA, and is aimed at developing tools that can characterize and evaluate real-world performance of devices. This will help the FDA to better regulate and verify the safety and effectiveness of devices that are developed to treat and terminate cardiac arrhythmias. All results from this project will be made freely available to the research community and to the general public.

The objective of this project is to improve the performance of autonomous systems in dynamic environments, such as disaster recovery, by integrating perception, planning paradigms, learning, and databases. For the next generation of autonomous systems to be truly effective in terms of tangible performance improvements (e.g., long-term operations, complex and rapidly changing environments), a new level of intelligence must be attained. This project improves the state of robotic systems by enhancing their ability to coordinate activities (such as searching a disaster zone), recognize objects or people, account for uncertainty, and "most important" learn, so the system's performance is continuously improving. To do this, the project takes an interdisciplinary approach to developing techniques in core areas and at the interface of perception, planning, learning, and databases to achieve robustness. This project seeks to significantly improve the performance of cyber-physical systems for time-critical applications such as disaster monitoring, search and rescue, autonomous navigation, and security and surveillance. It enables the development of techniques and tools to augment all decision making processes and applications which are characterized by continuously changing operating conditions, missions and environments. The project contributes to education and a diverse engineering workforce by training students at the University of California, Riverside, one of the most diverse research institutions in US and an accredited Hispanic Serving Institution. Instruction and research opportunities cross traditional disciplinary boundaries, and the project serves as the basis for undergraduate capstone design projects and a new graduate course. The software and testbeds from this project will be shared with the cyber-physical system research community, industry, and end users. The project plans to present focused workshops/tutorials at major IEEE and ACM conferences. The results will be broadly disseminated through the project website. For further information see the project website at: http://vislab.ucr.edu/RESEARCH/DSLC/DSLC.php

This project investigates new reinforcement learning algorithms to enable long-term real-time autonomous learning by cyber-physical systems (CPS). The complexity of CPS makes hand-programming safe and efficient controllers for them difficult. For CPS to meet their potential, they need methods that enable them to learn and adapt to novel situations that they were not programmed for. Reinforcement learning (RL) is a paradigm for learning sequential decision making processes with potential for solving this problem. However, existing RL algorithms do not meet all of the requirements of learning in CPS. Efficacy of the new algorithms for CPS is evaluated in the context of smart buildings and autonomous vehicles. Cyber-physical systems (CPS) have the potential to revolutionize society by enabling smart buildings, transportation, medical technology, and electric grids. Success of this project could lead to a new generation of CPS that are capable of adapting to their situation and improving their performance autonomously over time. In addition to the traditional methods of dissemination, this project will develop and release open-source code implementing the new reinforcement learning algorithms. Education and outreach activities associated with the project include a Freshman Research Initiative course, participation in a UT Austin annual open house that draws in many underrepresented minorities to interest the public in computer science and science in general, and the department's annual summer school for high school girls called First Bytes.

Cyber-physical systems employed in transportation, security and manufacturing applications rely on a wide variety of sensors for prediction and control. In many of these systems, acquisition of information requires the deployment and activation of physical sensors, which can result in increased expense or delay. A fundamental aspect of these systems is that they must seek information intelligently in order to support their mission, and must determine the optimal tradeoffs as to the cost of physical measurements versus the improvement in information. A recent explosion in sensor and UAV technology has led to new capabilities for controlling the nature and mobility of sensing actions by changing excitation levels, position, orientation, sensitivity, and similar parameters. This has in turn created substantial challenges to develop cyber-physical systems that can effectively exploit the degrees of freedom in selecting where and how to sense the environment. These challenges include high-dimensionality of observations and the associated "curse of dimensionality", non-trivial relationships between the observations and the latent variables, poor understanding of models relating the nature of potential sensing actions and the corresponding value of the collected information, and lack of sufficient training data from which to learn these models. Intellectual Merit: The proposed research includes: (1) data-driven stochastic control theory for intelligent sensing in cyber-physical systems that incorporates costs/delays/risks and accounts for scenarios where models for sensing, decision-making, and prediction are unavailable or poorly understood. (2) Validation of control methods on a UAV sensor network in the real world domain of archaeological surveying. Broader Impacts: The proposed effort includes: (a) Outreach: planned efforts for encouraging participation of women and under-represented groups; (b) Societal impact: research will lead to novel concepts in environmental monitoring, traffic surveillance, and security applications. (c) Multi- disciplinary activities: Impacting existing knowledge in cyber-physical systems, sensor management, and statistical learning. Research findings will be disseminated through conferences presentations, departmental seminars, journal papers, workshops and special sessions at IEEE CDC and RSS; (d) Curriculum development through new graduate level courses and course projects.

Cyber-physical systems are found in nearly every area of daily life: transportation, energy, medical systems, and food production. Life and safety frequently depend upon their correct operation. This project develops a novel systematic framework and methods for understanding, designing, and controlling complex coupled cyber and physical systems based on large-scale computation. This is achieved by explicitly developing the connection between the abstraction, modeling and verification frameworks of physics-based models and those of discrete-transition systems. The approach is fundamentally new, based on the unification of two recent developments: (1) new probabilistic tools for simulating and analyzing high-fidelity physics-based models; and (2) statistical model checking methods. In addition to analytical research, the project produces methods and computational tools that can be used on a wide range of cyber-physical systems, particularly those that are safety and performance critical. There have been dramatic recent advances in probabilistic computational techniques for purely physics-based models, treating them computationally as Markov chains, and enabling efficient computation even for high-dimensional systems. Simultaneously with these purely physics-based model approaches, state-of-the-art methods for the verification of purely discrete-state systems have been developed based on stochastic computational tools also using Markov chains as the basis. This project connects these two independent branches to yield a radically new approach for complex, high-dimensional cyber-physical systems, based on the unifying concept of Markov models as an interface between the cyber and physical domains. An integral part of the project is a unified educational program aimed at addressing key bottlenecks in the recruitment and development of female and minority students into engineering and computer science. The educational program is developed around a new robotic vehicle with complex fluid-structure dynamics, that is used in: (i) a week-long residential summer camp for female high-school students on "Mechanics & Dynamics"; (ii)undergraduate research experiences for female and minority students to facilitate the transition to graduate education; and (iii) an experimental graduate course on verification of embedded systems.

Cyber-Physical Systems (CPS) encompass a large variety of systems including for example future energy systems (e.g. smart grid), homeland security and emergency response, smart medical technologies, smart cars and air transportation. One of the most important challenges in the design and deployment of Cyber-Physical Systems is how to formally guarantee that they are amenable to effective human control. This is a challenging problem not only because of the operational changes and increasing complexity of future CPS but also because of the nonlinear nature of the human-CPS system under realistic assumptions. Current state of the art has in general produced simplified models and has not fully considered realistic assumptions about system and environmental constraints or human cognitive abilities and limitations. To overcome current state of the art limitations, our overall research goal is to develop a theoretical framework for complex human-CPS that enables formal analysis and verification to ensure stability of the overall system operation as well as avoidance of unsafe operating states. To analyze a human-CPS involving a human operator(s) with bounded rationality three key questions are identified: (a) Are the inputs available to the operator sufficient to generate desirable behaviors for the CPS? (b) If so, how easy is it for the operator with her cognitive limitations to drive the system towards a desired behavior? (c) How can areas of poor system performance and determine appropriate mitigations be formally identified? The overall technical approach will be to (a) develop and appropriately leverage general cognitive models that incorporate human limitations and capabilities, (b) develop methods to abstract cognitive models to yield tractable analytical human models (c) develop innovative techniques to design the abstract interface between the human and underlying system to reflect mutual constraints, and (d) extend current state-of-the-art reachability and verification algorithms for analysis of abstract interfaces, iin which one of the systems in the feedback loop (i.e., the user) is mostly unknown, uncertain, highly variable or poorly modeled. The research will provide contributions with broad significance in the following areas: (1) fundamental principles and algorithms that would serve as a foundation for provably safe robust hybrid control systems for mixed human-CPS (2) methods for the development of analytical human models that incorporate cognitive abilities and limitations and their consequences in human control of CPS, (3) validated techniques for interface design that enables effective human situation awareness through an interface that ensures minimum information necessary for the human to safely control the CPS, (4) new reachability analysis techniques that are scalable and allow rapid determination of different levels of system safety. The research will help to identify problems (such as automation surprises, inadequate or excessive information contained in the user interface) in safety critical, high-risk, or expensive CPS before they are built, tested and deployed. The research will provide the formal foundations for understanding and developing human-CPS and will have a broad range of applications in the domains of healthcare, energy, air traffic control, transportation systems, homeland security and large-scale emergency response. The research will contribute to the advancement of under-represented students in STEM fields through educational innovation and outreach. The code, benchmarks and data will be released via the project website. Formal descriptions of models of human cognition are in general incompatible with formal models of the Cyber Physical System (CPS) the human operator(s) control. Therefore, it is difficult to determine in a rigorous way whether a CPS controlled by a human operator will be safe or stable and under which circumstances. The objective of this research is to develop an analytic framework of human-CPS systems that encompasses engineering compatible formal models of the human operator that preserve the basic architectural features of human cognition. In this project the team will develop methodologies for building such models as well as techniques for formal verification of the human-CPS system so that performance guarantees can be provided. They will validate models in a variety of domains ranging from air traffic control to large scale emergency response to the administration of anesthesia.

To ensure operational safety of complex cyber-physical systems such as automobiles, aircraft, and medical devices, new models, analyses, platforms, and development techniques are needed that can predict, possible interactions between features, detect them in the features' concrete implementations, and either eliminate or mitigate such interactions through precise modeling and enforcement of mixed-criticality cyber-physical system semantics. This project is taking a novel approach to reasoning about and managing feature interactions in cyber-physical systems, which encompasses interactions within software, interactions through the physical dynamics of the system, and interactions via shared computational resources. The proposed approach consists of three tightly coupled research thrusts: (1) a novel way of modeling features as automata equipped with both physical dynamics of the feature environment, and an assigned criticality level in each state of an automaton, (2) new automata-theoretic and control-theoretic analysis techniques, enabled by the modeling approach, and (3) new algorithms for adaptive sharing of computational resources between individual features that are guaranteed to satisfy the assumptions made during analysis, realized within a novel mixed-criticality cyber-physical platform architecture. The modeling approach will introduce a new model for mixed-criticality cyber-physical components and will support modern development standards, such as AUTOSAR in the automotive industry, for assigning criticality levels to features. Component interfaces in this model will capture control modes and the associated physical dynamics, operating modes and the associated resource requirements and criticality level, as well as relationships between control modes and operating modes. Analysis of features expressed in the proposed model will include detection of interactions and exploration of their effect on safety properties of the composite system. The broader impacts of the proposed work are twofold. One impact lies in the pervasive use of cyber-physical systems in our society. If the developed results are adopted in industry, it may help to promote improved safety of such systems. Results of the proposed research will be used in courses offered at both University of Pennsylvania and Washington University at the graduate and undergraduate levels. The project will also provide students with opportunities to get involved in cutting edge research within their fields of study.