Investigation of Formal Verification of the Autonomous Vehicle Control System by Specification Translation

The autonomous vehicle control system is a typical kind of hybrid system that combines continuous behaviors such as time, velocity, position, and discrete behavior such as pedal actions including acceleration, braking, and no-operation. Formal specification and verification techniques help us to verify desired properties of the given system. In this study, we investigate an approach that formal verification of the autonomous vehicle control system by specification translation in CafeOBJ and Maude algebraic language to take advantage of the theorem proving and model checking.