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.

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.

As self-driving cars are introduced into road networks, the overall safety and efficiency of the resulting traffic system must be established and guaranteed. Numerous critical software-related recalls of existing automotive systems indicate that current design practices are not yet up to this challenge. This project seeks to address this problem, by developing methods to analyze and coordinate networks of fully and partially self-driving vehicles that interact with conventional human-driven vehicles on roads. The outcomes of the research are expected to also contribute to the safety of other cyber-physical systems with scalable configurable hierarchical structures, by developing a mathematical framework and corresponding software tools that analyze the safety and reliability of a class of systems that combine physical, mechanical and biological components with purely computational ones. The project research spans four technical areas: autonomous and human-controlled collaborative driving; scheduling computations over heterogeneous distributed computing systems; security and trust in V2X (Vehicle-to-Vehicle and Vehicle-to-Infrastructure) networks; and Verification & Validation of V2X systems through semi-virtual environments and scenarios. The integrating aspect of this research is the development of a distributed system calculus for Cyber-Physical Systems (CPS) that enables modeling, simulation and analysis of collaborative vehicular systems. The development of a comprehensive framework to model, analyze and test reconfiguration, hierarchical control, security and trust differentiates this research from previous attempts to address the same problem. Educational and outreach activities include integration of project research in undergraduate and graduate courses, and a summer camp at Ohio State University for high-school students through the Women in Engineering program.

In the next few decades, autonomous vehicles will become an integral part of the traffic flow on highways. However, they will constitute only a small fraction of all vehicles on the road. This research develops technologies to employ autonomous vehicles already in the stream to improve traffic flow of human-controlled vehicles. The goal is to mitigate undesirable jamming, traffic waves, and to ultimately reduce the fuel consumption. Contemporary control of traffic flow, such as ramp metering and variable speed limits, is largely limited to local and highly aggregate approaches. This research represents a step towards global control of traffic using a few autonomous vehicles, and it provides the mathematical, computational, and engineering structure to address and employ these new connections. Even if autonomous vehicles can provide only a small percentage reduction in fuel consumption, this will have a tremendous economic and environmental impact due to the heavy dependence of the transportation system on non-renewable fuels. The project is highly collaborative and interdisciplinary, involving personnel from different disciplines in engineering and mathematics. It includes the training of PhD students and a postdoctoral researcher, and outreach activities to disseminate traffic research to the broader public. This project develops new models, computational methods, software tools, and engineering solutions to employ autonomous vehicles to detect and mitigate traffic events that adversely affect fuel consumption and congestion. The approach is to combine the data measured by autonomous vehicles in the traffic flow, as well as other traffic data, with appropriate macroscopic traffic models to detect and predict congestion trends and events. Based on this information, the loop is closed by carefully following prescribed velocity controllers that are demonstrated to reduce congestion. These controllers require detection and response times that are beyond the limit of a human's ability. The choice of the best control strategy is determined via optimization approaches applied to the multiscale traffic model and suitable fuel consumption estimation. The communication between the autonomous vehicles, combined with the computational and control tasks on each individual vehicle, require a cyber-physical approach to the problem. This research considers new types of traffic models (micro-macro models, network approaches for higher-order models), new control algorithms for traffic flow regulation, and new sensing and control paradigms that are enabled by a small number of controllable systems available in a flow.

This project addresses the foundational problem of knowledge within cyber-physical systems (CPS), i.e., systems that combine aspects such as communication, computation, and physics. A single system observes its environment through sensors and interacts through actuators. Neither is perfect. Thus, the CPS's internal view of the world is blurry and its actions are imprecise. CPS are still analyzed with methods that do not distinguish between truth in the world and an internal view thereof, resulting in a mismatch between the behavior of theoretical models and their real-world counterparts. How could they be trusted to perform safety-critical tasks? This project addresses this critical insufficiency by developing methods to reason about knowledge and learning in CPS. The project pursues the development of new logical principles for verifying knowledge-aware CPS. This project investigates how to make the mismatch between the world and the partial perception through sensors explicit and how to achieve provably correct control in theory as well as practice despite this mismatch. By investigating changing knowledge in a changing world, this project contributes to a fundamental feature without which CPS can never be truly safe and efficient at the same time. The project's broader significance and importance are a result of the widespread attention that CPS gain in many safety-critical areas, such as in aviation and automotive industries. One reason for safety gaps in such CPS is that formal verification techniques are still largely knowledge-agnostic, and verifiable solutions overly pessimistic. This project addresses these issues and provides tools that allow for incorporating knowledge about the environment's intentions into the models to derive provably correct, but justifiably optimistic, and thus efficient, behavior. By their logical nature, these techniques are applicable to a wide range of CPS and, thus, contribute significantly to numerous applications. Results obtained within this project will be demonstrated in CPS models and laboratory robot scenarios, and will be shared in courses and with industrial partners. The technical approach that this project pursues develops a new modeling language, logic, and proof calculus for verifying knowledge-aware CPS. The knowledge paradigm used allows CPS controllers to seamlessly acquire knowledge about the world but also about other agents in the system, i.e., other controllers. Knowledge is the key to interactions between different agents. This project investigates how an explicit model of world perception and agent intentions - and knowledge of these perceptions and intentions - allows CPS agents to act, based on more efficient, but still provably safe control in multi-agent scenarios. The methods will be implemented in the verification tool KeYmaera and demonstrated in formal verification on different case study applications such as car scenarios.

In the next few decades, autonomous vehicles will become an integral part of the traffic flow on highways. However, they will constitute only a small fraction of all vehicles on the road. This research develops technologies to employ autonomous vehicles already in the stream to improve traffic flow of human-controlled vehicles. The goal is to mitigate undesirable jamming, traffic waves, and to ultimately reduce the fuel consumption. Contemporary control of traffic flow, such as ramp metering and variable speed limits, is largely limited to local and highly aggregate approaches. This research represents a step towards global control of traffic using a few autonomous vehicles, and it provides the mathematical, computational, and engineering structure to address and employ these new connections. Even if autonomous vehicles can provide only a small percentage reduction in fuel consumption, this will have a tremendous economic and environmental impact due to the heavy dependence of the transportation system on non-renewable fuels. The project is highly collaborative and interdisciplinary, involving personnel from different disciplines in engineering and mathematics. It includes the training of PhD students and a postdoctoral researcher, and outreach activities to disseminate traffic research to the broader public. This project develops new models, computational methods, software tools, and engineering solutions to employ autonomous vehicles to detect and mitigate traffic events that adversely affect fuel consumption and congestion. The approach is to combine the data measured by autonomous vehicles in the traffic flow, as well as other traffic data, with appropriate macroscopic traffic models to detect and predict congestion trends and events. Based on this information, the loop is closed by carefully following prescribed velocity controllers that are demonstrated to reduce congestion. These controllers require detection and response times that are beyond the limit of a human's ability. The choice of the best control strategy is determined via optimization approaches applied to the multiscale traffic model and suitable fuel consumption estimation. The communication between the autonomous vehicles, combined with the computational and control tasks on each individual vehicle, require a cyber-physical approach to the problem. This research considers new types of traffic models (micro-macro models, network approaches for higher-order models), new control algorithms for traffic flow regulation, and new sensing and control paradigms that are enabled by a small number of controllable systems available in a flow.

In the next few decades, autonomous vehicles will become an integral part of the traffic flow on highways. However, they will constitute only a small fraction of all vehicles on the road. This research develops technologies to employ autonomous vehicles already in the stream to improve traffic flow of human-controlled vehicles. The goal is to mitigate undesirable jamming, traffic waves, and to ultimately reduce the fuel consumption. Contemporary control of traffic flow, such as ramp metering and variable speed limits, is largely limited to local and highly aggregate approaches. This research represents a step towards global control of traffic using a few autonomous vehicles, and it provides the mathematical, computational, and engineering structure to address and employ these new connections. Even if autonomous vehicles can provide only a small percentage reduction in fuel consumption, this will have a tremendous economic and environmental impact due to the heavy dependence of the transportation system on non-renewable fuels. The project is highly collaborative and interdisciplinary, involving personnel from different disciplines in engineering and mathematics. It includes the training of PhD students and a postdoctoral researcher, and outreach activities to disseminate traffic research to the broader public. This project develops new models, computational methods, software tools, and engineering solutions to employ autonomous vehicles to detect and mitigate traffic events that adversely affect fuel consumption and congestion. The approach is to combine the data measured by autonomous vehicles in the traffic flow, as well as other traffic data, with appropriate macroscopic traffic models to detect and predict congestion trends and events. Based on this information, the loop is closed by carefully following prescribed velocity controllers that are demonstrated to reduce congestion. These controllers require detection and response times that are beyond the limit of a human's ability. The choice of the best control strategy is determined via optimization approaches applied to the multiscale traffic model and suitable fuel consumption estimation. The communication between the autonomous vehicles, combined with the computational and control tasks on each individual vehicle, require a cyber-physical approach to the problem. This research considers new types of traffic models (micro-macro models, network approaches for higher-order models), new control algorithms for traffic flow regulation, and new sensing and control paradigms that are enabled by a small number of controllable systems available in a flow.

Traditionally, the design of urban transit services has been based on limited sampling data collected through surveys and censuses, which are often dated and incomplete. Lacking massive online feeds from multiple transit modes makes it hard to achieve real-time equilibrium in demand and supply relationship through cyber-control, which eventually manifests into multiple urban transportation issues: (i) lengthy last-mile transit due to non-supply, (ii) prolonged waiting due to undersupply, and (iii) excessive idle mileage due to oversupply. This project addresses these issues by focusing on two types of transportation systems in metropolitan areas: (i) public bike rental sharing systems and (ii) fleet-oriented ride sharing systems. The public bike rental sharing systems are used to allow commuters to rent bikes near public transit stations for the last mile of their trips. The fleet-oriented ride sharing systems schedule a fleet of participating vehicles for ride sharing among passengers in which shared ridership reduces individual fare paid by passengers, increases the profit of taxi drivers, and can improve the availability of service. The theory and practice of transportation sharing systems have typically focused on isolated individual transportation modes. The project will collect massive multi-modal online feeds from metropolitan information infrastructure to model dynamic behaviors of transportation systems, and then utilize massive micro-level trip information to apply fine-grained real-time control to handle rapid changes in dynamic metropolitan environments. General principles and design methodologies will be designed to build multi-modal, integrated urban transportation systems. These research discoveries will be applied toward commercial applications. Long-term deployment problem of bike stations will be addressed, especially in the low-income districts, to provide suggestions on the station deployment and assessment for specific deployment plans. The project also solves the short-term bike maintenance issue to balance the usage of shared bikes to prevent quick deterioration of rental bikes, and improve availability of bike rental services in real time. This project will also study fleet-oriented ride sharing systems that decide fares based on real-time supply/demand ratio to handle dynamic metropolitan scenarios. This project will support two Ph.D. students who will receive innovation and technology translation training through close interactions with municipal governments and small-business companies. Such partnerships expedite the adoption of cutting-edge technology, evaluate research solutions in operational environments, and obtain user feedback to trigger further innovations. The project will improve the efficiency of existing transportation systems under sharing economy and ultimately the work would noticeably improve the quality of every-day life in metropolitan areas across the United States.

Many safety-critical cyber-physical systems rely on advanced sensing capabilities to react to changing environmental conditions. One such domain is automotive systems. In this domain, a proliferation of advanced sensor technology is being fueled by an expanding range of autonomous capabilities (blind spot warnings, automatic lane-keeping, etc.). The limit of this expansion is full autonomy, which has been demonstrated in various one-off prototypes, but at the expensive of significant hardware over-provisioning that is not tenable for a consumer product. To enable features approaching full autonomy in a commercial vehicle, software infrastructure will be required that enables multiple sensor-processing streams to be multiplexed onto a common hardware platform at reasonable cost. This project is directed at the development of such infrastructure. The desired infrastructure will be developed by focusing on a particularly compelling challenge problem: enabling cost-effective driver-assist and autonomous-control automotive features that utilize vision-based sensing through cameras. This problem will be studied by (i) examining numerous multicore-based hardware configurations at various fixed price points based on realistic automotive use cases, and by (ii) characterizing the range of vision-based workloads that can be feasibly supported using the software infrastructure to be developed. The research to be conducted will be a collaboration involving academic researchers at UNC and engineers at General Motors Research. The collaborative nature of this effort increases the likelihood that the results obtained will have real impact in the U.S. automotive industry. Additionally, this project is expected to produce new open-source software and tools, new course content, public outreach through participation in UNC's demo program, and lectures and seminars by the investigators at national and international forums.

Despite many advances in vehicle automation, much remains to be done: the best autonomous vehicle today still lags behind human drivers, and connected vehicle (V2V) and infrastructure (V2I) standards are only just emerging. In order for such cyber-physical systems to fully realize their potential, they must be capable of exploiting one of the richest and most complex abilities of humans, which we take for granted: seeing and understanding the visual world. If automated vehicles had this ability, they could drive more intelligently, and share information about road and environment conditions, events, and anomalies to improve situational awareness and safety for other automated vehicles as well as human drivers. That is the goal of this project, to achieve a synergy between computer vision, machine learning and cyber-physical systems that leads to a safer, cheaper and smarter transportation sector, and which has potential applications to other sectors including agriculture, food quality control and environment monitoring. To achieve this goal, this project brings together expertise in computer vision, sensing, embedded computing, machine learning, big data analytics and sensor networks to develop an integrated edge-cloud architecture for (1) "anytime scene understanding" to unify diverse scene understanding methods in computer vision, and (2) "cooperative scene understanding" that leverages vehicle-to-vehicle and vehicle-to-infrastructure protocols to coordinate with multiple systems, while (3) emphasizing how security and privacy should be managed at scale without impacting overall quality-of-service. This architecture can be used for autonomous driving and driver-assist systems, and can be embedded within infrastructure (digital signs, traffic lights) to avoid traffic congestion, reduce risk of pile-ups and improve situational awareness. Validation and transition of the research to practice are through integration within City of Pittsburgh public works department vehicles, Carnegie Mellon University NAVLAB autonomous vehicles, and across the smart road infrastructure corridor under development in Pittsburgh. The project also includes activities to foster development of a new cyber-physical systems workforce, though involvement of students in the research, co-taught multi-disciplinary courses, and co-organized workshops.