Towards formal verification of adaptive cruise controller using SpaceEx

摘要

A formal mathematical model of an Adaptive Cruise Controller (ACC) in SpaceEx is presented with a view to formally verify it to ensure its safety critical behavior. SpaceEx (an academic open source tool) is a hybrid systems modeling and verification platform which employs efficient implementation of reachability and safety verification algorithms which are scalable under certain assumptions, to circumvent the difficult problem of formal verification of hybrid systems. In this paper, application of SpaceEx in the comprehensive verification of an Adaptive Cruise Controller for automobiles is presented.