Title :
Formal verification of an automotive engine controller in cutoff mode
Author :
Villa, Tiziano ; Wong-Toi, Howard ; Balluchi, Andrea ; Preussig, J. ; Sangiovanni-Vincentelli, Alberto L. ; Watanabe, Yosinori
Author_Institution :
PARADES, Rome, Italy
Abstract :
We describe formal verification of convergence and performance properties of an engine control algorithm being developed for Magneti-Marelli. We study the cutoff mode, where the driver releases the accelerator and the controller regulates fuel injection to minimize the oscillations while decelerating. The engine and its controller are modeled with hybrid automata and the sliding action of the hybrid controller is formally verified with the model checker HYTECH
Keywords :
automata theory; control system analysis computing; convergence; formal verification; internal combustion engines; variable structure systems; HYTECH model checker; Magneti-Marelli; automotive engine controller; cutoff mode; formal verification; fuel injection; hybrid automata; hybrid controller; performance properties; sliding action; Automata; Automatic control; Automotive engineering; Embedded system; Engines; Formal verification; Fuels; Mathematical model; Sliding mode control; Torque control;
Conference_Titel :
Decision and Control, 1998. Proceedings of the 37th IEEE Conference on
Conference_Location :
Tampa, FL
Print_ISBN :
0-7803-4394-8
DOI :
10.1109/CDC.1998.761976
