Formal Design of Semi-Autonomous Cyberphysical Transportation Systems

The goal of this research is to develop fundamental theory, efficient algorithms, and realistic experiments for the analysis and design of safety-critical cyber-physical transportation systems with human operators. The research focuses on preventing crashes between automobiles at road intersections, since these account for about 40% of overall vehicle crashes. Specifically, the main objective of this work is to design provably safe driver-assist systems that understand driver's intentions and provide warnings/overrides to prevent collisions. In order to pursue this goal, hybrid automata models for the driver-vehicles-intersection system, incorporating driver behavior and performance as an integral part, are derived from human-factors experiments. A partial order of these hybrid automata models is constructed, according to confidence levels on the model parameters. The driver-assist design problem is then formulated as a set of partially ordered hybrid differential games with imperfect information, in which games are ordered according to parameter confidence levels. The resulting designs are validated experimentally in a driving simulator and in large-scale computer simulations. This research leverages the potential of embedded control and communication technologies to prevent crashes at traffic intersections, by enabling networks of smart vehicles to cooperate with each other, with the surrounding infrastructure, and with their drivers to make transportation safer, more enjoyable, and more efficient. The work is based on a collaboration among__researchers in formal methods, autonomous control, and human factors who are studying realistic and provably correct warning/override algorithms that can be readily transitioned to production vehicles.