Report on Verification of the MoBIES Vehicle-Vehicle Automotive OEP Problem

The DARPA MoBIES Automotive Vehicle-Vehicle Open Experimental Platform [14] defines a longitudinal controller for the leader car of a platoon moving in an Intelligent Vehicle Highway System (IVHS) autonomously. The challenge is to verify that cars using this longitudinal controller provide a safe (that is, collision-free) ride. This report presents the process of verifying this particular controller using our CHARON [2] toolkit. In particular, it involves modeling and simulation of the system in CHARON and verifying the controller using our predicate abstraction technique for hybrid systems [3].