This project represents a cross-disciplinary collaborative research effort on developing rigorous, closed-loop approaches for designing, simulating, and verifying medical devices. The work will open fundamental new approaches for radically accelerating the pace of medical device innovation, especially in the sphere of cardiac-device design. Specific attention will be devoted to developing advanced formal methods-based approaches for analyzing controller designs for safety and effectiveness; and devising methods for expediting regulatory and other third-party reviews of device designs. The project team includes members with research backgrounds in computer science, electrical engineering, biophysics, and cardiology; the PIs will use a coordinated approach that balances theoretical, experimental and practical concerns to yield results that are intended to transform the practice of device design while also facilitating the translation of new cardiac therapies into practice. The proposed effort will lead to significant advances in the state of the art for system verification and cardiac therapies based on the use of formal methods and closed-loop control and verification. The animating vision for the work is to enable the development of a true in silico design methodology for medical devices that can be used to speed the development of new devices and to provide greater assurance that their behaviors match designers' intentions, and to pass regulatory muster more quickly so that they can be used on patients needing their care. The scientific work being proposed will serve this vision by providing mathematically robust techniques for analyzing and verifying the behavior of medical devices, for modeling and simulating heart dynamics, and for conducting closed-loop verification of proposed therapeutic approaches. The acceleration in medical device innovation achievable as a result of the proposed research will also have long-term and sustained societal benefits, as better diagnostic and therapeutic technologies enter into the practice of medicine more quickly. It will also yield a collection of tools and techniques that will be applicable in the design of other types of devices. Finally, it will contribute to the development of human resources and the further inclusion of under-represented groups via its extensive education and outreach programs, including intensive workshop experiences for undergraduates

This project represents a cross-disciplinary collaborative research effort on developing rigorous, closed-loop approaches for designing, simulating, and verifying medical devices. The work will open fundamental new approaches for radically accelerating the pace of medical device innovation, especially in the sphere of cardiac-device design. Specific attention will be devoted to developing advanced formal methods-based approaches for analyzing controller designs for safety and effectiveness; and devising methods for expediting regulatory and other third-party reviews of device designs. The project team includes members with research backgrounds in computer science, electrical engineering, biophysics, and cardiology; the PIs will use a coordinated approach that balances theoretical, experimental and practical concerns to yield results that are intended to transform the practice of device design while also facilitating the translation of new cardiac therapies into practice. The proposed effort will lead to significant advances in the state of the art for system verification and cardiac therapies based on the use of formal methods and closed-loop control and verification. The animating vision for the work is to enable the development of a true in silico design methodology for medical devices that can be used to speed the development of new devices and to provide greater assurance that their behaviors match designers' intentions, and to pass regulatory muster more quickly so that they can be used on patients needing their care. The scientific work being proposed will serve this vision by providing mathematically robust techniques for analyzing and verifying the behavior of medical devices, for modeling and simulating heart dynamics, and for conducting closed-loop verification of proposed therapeutic approaches. The acceleration in medical device innovation achievable as a result of the proposed research will also have long-term and sustained societal benefits, as better diagnostic and therapeutic technologies enter into the practice of medicine more quickly. It will also yield a collection of tools and techniques that will be applicable in the design of other types of devices. Finally, it will contribute to the development of human resources and the further inclusion of under-represented groups via its extensive education and outreach programs, including intensive workshop experiences for undergraduates.

Title: CPS: Breakthrough: Development of Novel Architectures for Control and Diagnosis of Safety-Critical Complex Cyber-Physical Systems This project is developing novel architectures for control and diagnosis of complex cyber-physical systems subject to stringent performance requirements in terms of safety, resilience, and adaptivity. These ever-increasing demands necessitate the use of formal model-based approaches to synthesize provably-correct feedback controllers. The intellectual merit of this research lies in a novel combination of techniques from the fields of dynamical systems, discrete event systems, reactive synthesis, and graph theory, together with new advancements in terms of abstraction techniques, computationally efficient synthesis of control and diagnosis strategies that support distributed implementations, and synthesis of acquisition of information and communication strategies. The project's broader significance and importance are demonstrated by the expected improvement of the safety, resilience, and performance of complex cyber-physical systems in critical infrastructures as well as the efficiency with which they are designed and certified. The original approach being developed is based on the combination of multi-resolution abstraction graphs for building discrete models of the underlying cyber-physical system with reactive synthesis techniques that exploit a representation of the solution space in terms of a finite structure called a decentralized bipartite transition system. The concepts of abstraction graph and decentralized bipartite transition system are novel and open new avenues of investigation with significant potential to the formal synthesis of safe, resilient, and adaptive controllers. This methodology naturally results in a set of decentralized and asynchronous controllers and diagnosers, which ensures greater resilience and adaptivity. Overall, this research will significantly impact the Science of Cyber-Physical Systems and the Engineering of Cyber-Physical Systems.

Driven by both civilian and military applications, such as coordinated surveillance, search and rescue, underwater or space exploration, manipulation in hazardous environments, and rapid emergency response, cooperative actions by teams of robots has emerged as an important research area. However, the coordination strategies for such robot teams are still developed to a great extent by trial-and-error processes. Hence, the strategies cannot guarantee mission success. This award supports fundamental research to provide a provably correct formal design theory of multi-robot systems that guarantees mission success. Furthermore, results from the research can be extended to the design of more general cyber-physical systems (CPSs) consisting of distributed and coordinated subsystems, such as the national power grid, ground/air traffic networks, and manufacturing systems. These CPSs are critical components of the national civil infrastructure that must operate reliably to ensure public safety. The multidisciplinary approach taken will help broaden participation of underrepresented groups in research and positively impact engineering education. Focusing on multi-robot teams, the goal of the research is to build foundations for a provably correct formal design theory for CPSs. This design theory will guarantee a given global performance of multi-robot teams through designing local coordination rules and control laws. The basic idea is to decompose the team mission into individual subtasks such that the design can be reduced to a local synthesis problem for individual robots. Multidisciplinary approaches combining hybrid systems, supervisory control, regular inference and model checking will be utilized to achieve this goal. The developed theory will enable robots in the team to cooperatively learn their individual roles in a mission, and then automatically synthesize local supervisors to fulfill their subtasks. A salient feature of this method lies on its ability to handle environmental uncertainties and unmodeled dynamics, as there is no need for an explicit model of the transition dynamics of each agent/robot and their interactions with the environment. In addition, the design is online and reactive, enabling the robot team to adapt to changing environments and dynamic tasking. The derived theory will be implemented as software tools and will be demonstrated through real robotic systems consisting of unmanned ground and aerial vehicles in unstructured urban/rural areas.

Driven by both civilian and military applications, such as coordinated surveillance, search and rescue, underwater or space exploration, manipulation in hazardous environments, and rapid emergency response, cooperative actions by teams of robots has emerged as an important research area. However, the coordination strategies for such robot teams are still developed to a great extent by trial-and-error processes. Hence, the strategies cannot guarantee mission success. This award supports fundamental research to provide a provably correct formal design theory of multi-robot systems that guarantees mission success. Furthermore, results from the research can be extended to the design of more general cyber-physical systems (CPSs) consisting of distributed and coordinated subsystems, such as the national power grid, ground/air traffic networks, and manufacturing systems. These CPSs are critical components of the national civil infrastructure that must operate reliably to ensure public safety. The multidisciplinary approach taken will help broaden participation of underrepresented groups in research and positively impact engineering education. Focusing on multi-robot teams, the goal of the research is to build foundations for a provably correct formal design theory for CPSs. This design theory will guarantee a given global performance of multi-robot teams through designing local coordination rules and control laws. The basic idea is to decompose the team mission into individual subtasks such that the design can be reduced to a local synthesis problem for individual robots. Multidisciplinary approaches combining hybrid systems, supervisory control, regular inference and model checking will be utilized to achieve this goal. The developed theory will enable robots in the team to cooperatively learn their individual roles in a mission, and then automatically synthesize local supervisors to fulfill their subtasks. A salient feature of this method lies on its ability to handle environmental uncertainties and unmodeled dynamics, as there is no need for an explicit model of the transition dynamics of each agent/robot and their interactions with the environment. In addition, the design is online and reactive, enabling the robot team to adapt to changing environments and dynamic tasking. The derived theory will be implemented as software tools and will be demonstrated through real robotic systems consisting of unmanned ground and aerial vehicles in unstructured urban/rural areas.

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.

Large battery systems with 100s/1000s cells are being used to power various physical platforms. For example, automobiles are transitioning from conventional powertrains to (plug-in) hybrid and electric vehicles (EVs). To achieve the desired efficiency of EVs, significant improvements are needed in the architecture and algorithms of battery management. This project will develop a new comprehensive battery management architecture, called Smart Battery Management System (SBMS). The research is expected to bridge the wide gap existing between cyber-physical system (CPS) research and electrification industry communities, provide environment-friendly solutions, increase the awareness of CPS, and develop skilled human resources. This project will incorporate and enhance a battery management system (BMS) by including battery state-of-charge (SoC) and state-of-health (SoH) algorithms as well as power management strategies on both pack and cell levels. Specifically, it consists of five main research tasks: (i) design a dynamically reconfigurable energy storage system to tolerate harsh internal and external stresses; (ii) develop cell-level thermal management algorithms; (iii) develop efficient, dependable charge and discharge scheduling algorithms in hybrid energy storage systems; (iv) develop a comprehensive, diagnostic/prognostic (P/D) algorithm with system parameters adjusted for making optimal decisions; and (v) build a testbed and evaluate the proposed architecture and algorithms on the testbed. This research will advance the state-of-the-art in the management of large-scale energy storage systems, extending their life and operation-time significantly, which is key to a wide range of battery-powered physical platforms. That is, SBMS will enable batteries to withstand excessive stresses and power physical platforms for a much longer time, all at low costs. SBMS will also serve as a basic framework for various aspects of CPS research, integrating (cyber) dynamic control and P/D mechanisms, and (physical) energy storage system dynamics.

This project will design next-generation defense mechanisms to protect critical infrastructures, such as power grids, large industrial plants, and water distribution systems. These critical infrastructures are complex primarily due to the integration of cyber and physical components, the presence of high-order behaviors and functions, and an intricate and large interconnection pattern. Malicious attackers can exploit the complexity of the infrastructure, and compromise a system's functionality through cyber attacks (that is hacking into the computation and communication systems) and/or physical attacks (tampering with the actuators, sensors and the control system). This work will develop mathematical models of critical infrastructures and attacks, develop intelligent control-theoretic security mechanisms, and validate the findings on an industry-accredited simulation platform. This project will directly impact national security and economic competitiveness, and the results will be available and useful to utility companies. To accompany the scientific advances, the investigators will also engage in educational efforts to bring this research to the classroom at UCR, and will disseminate their results via scientific publications. The work will also create several opportunities for undergraduate and graduate students to engage in research at UCR, one of the nation's most ethnically diverse research-intensive institutions. This study encompasses theoretical, computational, and experimental research at UCR aimed at characterizing vulnerabilities of complex cyber-physical systems, with a focus on electric power networks, and control-theoretic defense mechanisms to ensure protection and graceful performance degradation against accidental faults and malicious attacks. This project proposes a transformative approach to cyber-physical security, which builds on a unified control-theoretic framework to model cyber-physical systems, attacks, and defense strategies. This project will undertake three main research initiatives ranging from fundamental scientific and engineering research to analysis using industry-accepted simulation tools: (1) modeling and analysis of cyber-physical attacks, and their impact on system stability and performance; (2) design of monitors to reveal and distinguish between accidental and malignant contingencies; and (3) synthesis of adaptive defense strategies for stochastic and highly dynamic cyber-physical systems. Results will first be characterized from a pure control-theoretic perspective with focus on stochastic, switching, and dynamic cyber-physical systems, so as to highlight fundamental research challenges, and then specialized for the case of smart grid, so as to clarify the implementation of monitors, attacks, and defense strategies. The findings and strategies will be validated for the case of power networks by using the RTDS simulation system, which is an industry-accredited tool for real-time tests of dynamic behavior, faults, attacks, monitoring systems, and defensive strategies.

The goal of this project is to demonstrate new cyber-physical architectures that allow the sharing of closed-loop sensor networks among multiple applications through the dynamic allocation of sensing, networking, and computing resources. The sharing of sensor network infrastructures makes the provision of data more cost efficient and leads to virtual private sensor network (VPSN) architectures that can dramatically increase the number of sensor networks available for public use. These cyber infrastructures support a paradigm, called Sensing as a Service, in which users can obtain sensing and computational resources to generate the required data for their sensing applications. The challenge in sharing closed-loop sensor networks is that one application's actuation request might interfere with another's request. To address this challenge the VPSN architectures are comprised of three components: 1) a sensor virtualization layer that ensures that users obtain timely access to sensor data when requested and isolates their requests from others' through the creation of appropriate scheduling algorithms; 2) a computation virtualization layer that enables the allocation of computational resources for real-time data intensive applications which is closely tied to the sensor virtualization layer; 3) a virtualization toolkit that supports application developers in their efforts to build applications for virtualized, closed-loop sensor networks. The sharing of closed-loop sensor networks leads to substantial savings on infrastructure and maintenance costs. The proposed VPSN architectures enable users to create their own applications without having detailed knowledge of sensing technologies and allows them to focus on the development of applications. VPSNs will contribute to the creation of a nationwide, shared sensing cyber infrastructure, which will provide critical information for public safety and security. VPSNs will also help to revolutionize the way undergraduate and graduate students from many disciplines perform research. Students will be shielded from some of the complexities of sensor networks and allowed to focus on their core research. To prepare students from the Electrical and Computer Engineering (ECE) department at the University of Massachusetts to perform this kind of research, new classes in the area of Integrative Systems Engineering and Sensor Network Virtualization will be offered.