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.

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.

Modern medical devices increasingly incorporate connectivity mechanisms that offer the potential to integrate devices via network/middleware technology into larger systems of cooperating devices. Initial integration efforts in the industry are focused on streaming device data into electronic health records and integrating information from multiple devices into single customizable displays. This proposal provides a research foundation for engineering and verification of these safety critical systems through creating an open source Medical Device Coordination Framework (MDCF) which includes: 1)middleware for integrating medical devices and electronic health records, and 2) a model-based development environment that implements medical device coordination applications (apps for short), enabling a systems of systems paradigm for medical devices. The project has substantial broader impact via tools and techniques for verifying the integration of medical systems that are compatible with the Integrated Clinical Environment standard. In addition, the proposer includes extensive interaction with FDA specialists who are looking to transition these methods into their validation and verification processes for their regulatory mission.

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.

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.

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.

Trustworthy operation of next-generation complex power grid critical infrastructures requires mathematical and practical verification solutions to guarantee the correct infrastructural functionalities. This project develops the foundations of theoretical modeling, synthesis and real-world deployment of a formal and scalable controller code verifier for programmable logic controllers (PLCs) in cyber-physical settings. PLCs are widely used for control automation in industrial control systems. A PLC is typically connected to an engineering workstation where engineers develop the control logic to process the input values from sensors and issue control commands to actuators. The project focuses on protecting infrastructures against malicious control injection attacks on PLCs, such as Stuxnet, that inject malicious code on the device to drive the underlying physical platform to an unsafe state. The broader impact of this proposal is highly significant. It offers potential for real-time security for critical infrastructure systems covering sectors such as energy and manufacturing. The project's intellectual merit is in providing a mathematical and practical verification framework for cyber-physical systems through integration of offline formal methods, online monitoring solutions, and power systems analysis. Offline formal methods do not scale for large-scale platforms due to their exhaustive safety analysis of all possible system states, while online monitoring often reports findings too late for preventative action. This project takes a hybrid approach that dynamically predicts the possible next security incidents and reports to operators before an unsafe state is encountered, allowing time for response. The broader impact of this project is in providing practical mathematical analysis capabilities for general cyber-physical safety-critical infrastructure with potential direct impact on our national security. The research outcomes are integrated into education modules for graduate, undergraduate, and K-12 classrooms.

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.