SPLAT! How to Avoid Bugs while Driving on the Highway
Sarah Loos, Carnegie Mellon University
A bug on your windshield does little damage, but a bug in the software that controls your engine, brakes or steering is catastrophic. Driver assistance technologies, like adaptive cruise control and automatic braking protocols, have the potential to increase the efficiency of crowded roads, but more compelling is their capacity for reducing the number of accidents and fatalities resulting from driver error. Yet, increased dependence on this next-generation technology is wise only when its reliability has been ensured and regulated. Our research strives to find automated methods for formal verification of these systems. We have discovered several fundamental principles which allow large-scale systems to be verified with modular, mechanized, and semi-automated methods. We used these methods to give the first mechanized formal verification of adaptive cruise control for a distributed highway system with an arbitrary number of cars. The major mismatches in advanced hybrid systems for traffic applications are caused by scalability issues, nonlinearities in dynamics, and lack of modeling features. For instance, traffic control systems require maneuvers with a large and evolving number of participants, depending on the local traffic situation. Verification does not yet scale to large systems like these. We are working to develop hierarchical modularity principles in order to exploit the static structure of the system, which would otherwise be too big to handle. Verification is increasingly useful when it handles models with a large degree of freedom. We are developing a parallel automated theorem-prover for hybrid systems which, when combined with previously described methods, could automatically verify complex systems, making a leap forward in CPS safety. Our methods can’t protect your windshield from insects as you cruise down the highway, but with continued research we can remove the dangerous software bugs in safety-critical systems that testing and model checking overlook.
Abstract Author(s): Sarah M. Loos, André Platzer