Jairam S., Lata K., Roy S., Bhat N.
Texas Instruments India Pvt Ltd., IN
Keywords: ACC, formal verification, Gyroscope, MEMS
A formal verification approach for MEMS based embedded systems is presented. The methodology is demonstrated on an adaptive cruise control (ACC) system for the motion control of a platoon of cars. The system consists of a MEMS based gyroscope for measuring speed. The ACC system and the MEMS component are first modeled as a hybrid system, and then validated using a discrete time domain dynamic simulation approach in the Simulink/Stateflow framework from Mathworks. For its validation using a formal approach, CHECKMATE [1] a public domain formal verification tool for hybrid systems is used. CHECKMATE accepts a restrictive hybrid automata model, known as polyhedral invariant hybrid automata (PIHA) [2]. This necessitates transformation of the general Simulink/Stateflow model into a restrictive Simulink/Stateflow model using a subset of its models/blocks acceptable by CHECKMATE to create the equivalent PIHA model. To integrate the MEMS gyroscope model under CHECKMATE compliance requirements, it becomes necessary to make changes to the CHECKMATE implementation code in MATLAB. In this paper we outline our experience and highlight several issues faced in using CHECKMATE to carry out a formal analysis. The key contributions of the paper are 1) Statement of realistic properties which enable formal analysis and ensure a fail-safe, or safety critical operation of the ACC system. 2) Simulation and validation of the MEMS based ACC model in Simulink/Stateflow using exact macro-models for both MEMS gyroscope and the ACC system [3]. 3) Techniques to model an open hybrid system in CHECKMATE (it accepts only closed hybrid systems for formal analysis). 4) Transformations in Simulink/Stateflow models of the ACC and MEMS gyroscope that are necessary to conform to the PIHA model. 5) Description of changes necessary in the CHECKMATE code in Matlab to integrate the complex MEMS based gyroscope model captured as a look-up-table (LUT). 6) Optimization of the ACC system parameters using formal runs in CHECKMATE to identify fail-safe regions of operation. 7) Selection of MEMS gyroscope topologies based on optimized ACC system parameters.
Journal: TechConnect Briefs
Volume: 3, Nanotechnology 2008: Microsystems, Photonics, Sensors, Fluidics, Modeling, and Simulation – Technical Proceedings of the 2008 NSTI Nanotechnology Conference and Trade Show, Volume 3
Published: June 1, 2008
Pages: 611 - 614
Industry sectors: Advanced Materials & Manufacturing | Sensors, MEMS, Electronics
Topic: Informatics, Modeling & Simulation
ISBN: 978-1-4200-8505-1