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.

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.

This INSPIRE award is partially funded by the Cyber-Physical Systems Program in the Division of Computer and Network Systems in the Directorate for Computer and Information Science and Engineering, the Information and Intelligent Systems Program in the Division of Information and Intelligent Systems in the Directorate for Computer and Information Science and Engineering, the Computer Systems Research Program in the Division of Computer and Network Systems in the Directorate for Computer and Information Science and Engineering, and the Software and Hardware Foundations Program in the Division of Computing and Communications Foundations in the Directorate for Computer and Information Science and Engineering. Sound plays a vital role in the ocean ecosystem as many organisms rely on acoustics for navigation, communication, detecting predators, and finding food. Therefore, the 3D underwater soundscape, i.e., the combination of sounds present in the immersive underwater environment, is of extreme importance to understand and protect underwater ecosystems. This project is creating a transformative distributed ocean observing system for studying the underwater soundscape at revolutionary spatial (~100 meters) and temporal (~100 seconds) resolutions that is also able to simultaneously resolve small-scale ocean current flow. These breakthroughs are achieved using a distributed collective of small hydrophone-equipped subsurface floats, which utilize group management techniques and sensor fusion to understand the ocean soundscape in a Lagrangian manner. The ability to record soundscapes provides a novel sensing technology to understand the effects of sound on marine ecosystems and the role that sound plays for species development. Experiments off the coast of San Diego, CA, and a research campaign in the Cayman Islands provide concrete scientific studies that are tightly interwoven with the engineering research. Oceans are drivers of global climate, are home to some of the most important and diverse ecosystems, and represent a substantial contribution to the world's economy as a major source of food and employment. The technological and scientific advances in this project provide crucial tools to understand natural ocean resources, by studying soundscapes at spatio-temporal scales that were heretofore extremely burdensome and expensive to obtain.

This project establishes a new framework for the formal verification of cyber-physical systems. The framework combines the power of logical decision engines and scalable numerical methods to perform safety verification of general nonlinear hybrid systems. The key difficulty with formal verification of hybrid systems is that all scalable modern verification techniques rely heavily on the use of powerful decision procedures. For hybrid systems, one needs to reason about logic formulas over the real numbers with nonlinear functions, which has been regarded as an intractable problem. The project proposes new directions for tackling the core decision problems, with the combined power of logical and numerical algorithms. The research directly leads to the development of practical tools that will push the frontier of verification of realistic cyber-physical systems to a brand new level. This project aims at fundamental research of problems that stand at the core of the design, analysis, and implementation of reliable cyber-physical systems. It combines techniques from logic, numerical analysis, and automated reasoning, and will produce a unifying methodology that is powerful to address main challenges in this field. The techniques developed in this project will significantly enhance the complexity and reliability of the next generations of cyber-physical systems. Cyber-physical systems are ubiquitous in safety-critical applications as diverse as aerospace, automotive, civil infrastructure, energy, manufacturing, and healthcare. Malfunctioning cyber-physical systems can have catastrophic economic and societal consequences. This project will have a broad range of impact in these areas. This research aims to significantly enhance the management of complexity and reliability of the next generations of cyber-physical systems, and will broadly impact all the application areas.

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.

This project will develop architecture and supporting enabling technologies to avert imminent loss of life or property in fast changing environments. The selected application is resuscitation in an intensive care unit (ICU) because it is life critical, time critical, human-centric and includes complex devices and software. For example, heart attack can be obscured in a trauma patient hemorrhaging from a broken leg in the presence of a collapsed lung. The challenge lies in solving the overarching difficulties of safe execution while maintaining complex and dynamic workflows. The availability and skill levels of medical staff, patient conditions, and medical device configurations all change rapidly. The core contribution is design and verification of reduced complexity situation awareness architecture for Emergency Cyber Physical Human systems (ECPH), supported by enabling technologies such as workflow adaptation protocols, managing data uncertainty and safe device plug and play. The ECPH workflow adaptation protocols are not only a function of the tasks and environment at hand, but must also be aware of the capabilities and training of the medical staff. In addition, risk mitigation driven safety interlock protocols will keep the actions of medical staff and CPS in synchrony with dynamically selected workflows. This is a cooperative effort of UIUC engineering and the ICU department of Carle Foundation Hospital. An ECPH team operates to accomplish a mission under rapidly changing circumstances. The stressful, rushed, and often unfriendly environment of an ECPH system means that errors, uncertainty, and failures will arise. This research will offer safety and resilience in the face of such disruptions. Effective and immediate intervention enabled by an optimized ECPH system will dramatically reduce preventable errors. The societal impact of effective collaboration under high stress will be enormous in terms of human lives and health care costs. According to CDC in 2010, the estimated direct & indirect costs of heart attacks and strokes alone in the U.S. were $503.2 billion; a significant percent of such patients during emergency care suffer complications and harm which are preventable. This project will develop educational material for training the next generation of researchers and engineers. The technology to be developed will also be adapted to other similar ECPH environments such as fighting a raging building fire.

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.

1329875 (Hu). Despite their importance within the energy sector, buildings have not kept pace with technological improvements and particularly the introduction of intelligent features. A primary obstacle in enabling intelligent buildings is their highly distributed and diffuse nature. To address this challenge, a modular approach will be investigated for building design, construction, and operation that would completely transform the building industry. Buildings would be assembled from a set of pre-engineered intelligent modules and commissioned on site in a "plug-and-play" manner much like a "LEGO" set but with added capability of (a) allowing for easy configuration and re-configuration that can be integrated to provide delivery of thermal and visual comfort, ventilation; (b) providing optimized controls in terms of overall occupant satisfaction and energy efficiency and performance monitoring. The primary goal of the research is to develop and demonstrate innovative concepts for distributed intelligence along with a new paradigm for plug-and-play building control that is a necessary precursor in enabling this transformation. To accomplish these tasks, the investigators constitute a multidisciplinary team with expertise from three engineering disciplines, namely Civil (Architectural), Mechanical, Electrical and Computer Engineering. The intellectual merit of this research lies in developing a unified approach that advances the engineering of cyber-physical systems (CPS) for buildings by contributing to the following fields: (a) modeling and identification of building subsystems and integrated systems; (b) multi-agent system networks that enable distributed intelligent monitoring and control of multi-zone buildings; (c) optimal control algorithms for stochastic hybrid systems that can optimize the operation of buildings with mode changes under uncertainty. These contributions will be integrated in simulation and experimental platforms for multi-agent building system networks to validate the developed algorithms and to provide a new CPS-based technological solution to the control and optimization of modular buildings. An initial knowledge/technology base will be provided for scalable, adaptive, robust, and efficient engineering solutions for cyber-enabled building systems that will transform the current building operation practice, enabling the next generation of smart buildings with optimized comfort delivery and energy use. The broader impacts of this project are: (a) Theoretical development of modeling representations, algorithms, and simulation tools that will impact a number of scientific communities, including Civil/Architectural, Mechanical and Computer Engineering, Computer Science, and Operations Research. The proposed new principles for heterogeneous multi-agent system networks, distributed intelligence, and optimal hybrid control algorithms will have impacts in a diverse range of fields outside of building systems such as power systems, transportation systems, robotics, etc.; (b) Integration of the proposed modeling, simulation, and experimental platforms into new teaching modules and experiential learning activities that support the curriculum development in three engineering schools and Purdue?s first year engineering program; (c) Dissemination of research outcomes to the industry to open up a new horizon of business and economy that would enable the growth of green and intelligent buildings; (d) The creation of outreach and engagement initiatives that motivate K-12 teachers and students in STEM learning and research, broaden the participation of underrepresented groups in engineering, and motivate undergraduate students to participate in research related to emerging CPS topics.

Processors in cyber-physical systems are increasingly being used in applications where they must operate in harsh ambient conditions and a computational workload which can lead to high chip temperatures. Examples include cars, robots, aircraft and spacecraft. High operating temperatures accelerate the aging of the chips, thus increasing transient and permanent failure rates. Current ways to deal with this mostly turn off the processor core or drastically slow it down when some part of it is seen to exceed a given temperature threshold. However, this pass/fail approach ignores the fact that (a) processors experience accelerated aging due to high temperatures, even if these are below the threshold, and (b) while deadlines are a constraint for real-time tasks to keep the controlled plant in the allowed state space, the actual controller response times that will increase if the voltage or frequency is lowered (to cool down the chip) are what determine the controlled plant performance. Existing approaches also fail to exploit the tradeoff between controller reliability (affected by its temperature history) and the performance of the plant. This project addresses these issues. Load-shaping algorithms are being devised to manage thermal stresses while ensuring appropriate levels of control quality. Such actions include task migration, changing execution speed, selecting an alternative algorithm or software implementation of control functions, and terminating prematurely optional portions of iterative tasks. Validation platforms for this project include automobiles and unmanned aerial vehicles. These platforms have been chosen based on both their importance to society and the significant technical challenges they pose. With CPS becoming ever more important in our lives and businesses, this project which will make CPS controllers more reliable and/or economical has broad potential social and economic impacts. Collaboration with General Motors promotes transition of the new technology to industry. The project includes activities to introduce students to thermal control in computing, in courses spanning high-school, undergraduate and graduate curricula.