Formal Verification of an Autonomous Vehicle System
Speaker: Nok Wongpiromsarn (Caltech)

 

Abstract 
Due to the increase in complexity of hardware and software, traditional techniques for analyzing the system quality based on testing are not adequate to ensure the reliability of the system. In this talk, I will describe the framework for formal verification, an alternative approach to analyzing systems, and illustrate how to formally specify and verify certain properties of Alice, an autonomous vehicle developed by the California Institute of Technology for the 2007 DARPA Urban Challenge. Due to the complexity of the system, its components are specified separately. Two approaches to deriving system's properties from components' specifications will be presented by considering two case studies. In the first case study, the properties of the system are derived from its specification which is simply the conjunction of its components' specifications. The correctness of the implementation is proved using a model checker. In the second case study, the properties of the relevant components are first derived from their specifications. The system's properties are then obtained from the components' properties.