Abstract: Many electronic devices contain a micro-controller that interacts with a physical environment. The use of such control systems is widespread, for instance, they are employed in cars, robotic systems, and medical devices. For many of these applications, correctness of the control software, the low-level software controlling the physical system, is crucial. In this talk, I will present a technique for the systematic validation of such control software that combines software model checking techniques with continuous system simulation. When compared to testing, the presented approach allows controlling certain aspects, such as task scheduling and sensor errors, that cannot be controlled during testing; when compared to simulation, instead of a single trace, multiple traces are generated in a systematic way to cover exhaustively a set of possibilities. The result is a method for checking properties of a control system that generates a spectrum of simulation traces. The presented method allows expressing properties of the software, e.g., absence of null-pointer dereferences, as well as properties of the physical system the software is controlling, e.g., that a robot will never get too far from a given path.

This is joint work with Edmund M. Clarke and Sebastian Scherer.

This talk is in partial fulfillment of the speaking requirement.

Flavio Lerda received an M.S. in Software Engineering from Politecnico di Torino, Italy in 2000 and has spent two years as a visiting scientist in the Automated Software Engineering Group at NASA Ames Research Center. Currently, he is a PhD student in the Computer Science Department at Carnegie Mellon University. His research interests include Model Checking for Software and he is working on this subject with his advisor Edmund M. Clarke.