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.

Many of the ideas that drive modern cloud computing, such as server virtualization, network slicing, and robust distributed storage, arose from the research community. But because today's clouds have particular, non-malleable implementations of these ideas "baked in," they are unsuitable as facilities in which to conduct research on future cloud architectures. This project creates CloudLab, a facility that will enable fundamental advances in cloud architecture. CloudLab will not be a cloud; CloudLab will be large-scale, distributed scientific infrastructure on top of which many different clouds can be built. It will support thousands of researchers and run hundreds of different, experimental clouds simultaneously. The Phase I CloudLab deployment will provide data centers at Clemson (with Dell equipment), Utah (HP), and Wisconsin (Cisco), with each industrial partner collaborating to explore next-generation ideas for cloud architectures CloudLab will be a place where researchers can try out ideas using any cloud software stack they can imagine. It will accomplish this by running at a layer below cloud infrastructure: it will provide isolated, bare-metal access to a set of resources that researchers can use to bring up their own clouds. These clouds may run instances of today's popular stacks, modest modifications to them, or something entirely new. CloudLab will not be tied to any particular particular cloud stack, and will support experimentation on multiple in parallel. The impact of cloud computing outside the field of computer science has been substantial: it has enabled a new generation of applications and services with direct impacts on society at large. CloudLab is positioned to have an immediate and substantial impact on the research community by providing access to the resources it needs to shape the future of clouds. Cloud architecture research, enabled by CloudLab, will empower a new generation of applications and services which will bring direct benefit to the public in areas of national priority such as medicine, smart grids, and natural disaster early warning and response.

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.

Designing software that can properly and safely interact with the physical world is an important cyber-physical systems design challenge. The proposed work includes the development of a novel approach to designing planning and control algorithms for high-performance cyber physical systems. The new approach was inspired by statistical mechanics and stochastic geometry. It will (i) identify behavior such as phase transitions in cyber-physical systems and (ii) capitalize this behavior in order to design practical algorithms with provable correctness and performance guarantees. The algorithms developed through this research effort hold the potential for immediate industrial impact, particularly in the development of real-time robotic systems. These algorithms may strengthen the rapidly developing U.S. robotics industry. The proposed research activity will also vitalize the PI?s educational plans. Undergraduate and graduate courses that make substantial contributions to the embedded systems education at MIT will be developed. The classes will focus on provably-correct controller synthesis for cyber-physical systems, which is currently not thought at MIT. Undergraduate students will be involved in research activities.