Verification of a MEMS based adaptive cruise control system using simulation and semi-formal approaches

In this paper we present a verification approach for a MEMS based hybrid system. The hybrid system is an adaptive cruise controller (ACC) involving a MEMS based gyroscope for speed measurement, for the motion control of a platoon of cars. A transformation based approach to obtain a continuous time solution of the states of the hybrid system is presented. This is then integrated into the Simulink/Stateflow (SS) tool framework from MathWorks Inc., where the validation of the ACC is carried out using simulation on the differential equation based and analytical function based continuous time domain dynamic behavior. We also show how this approach and the framework is amenable to verification using formal and semi-formal approaches.