Formal verification of an automotive engine controller in cutoff mode
Tiziano Villa, Howard Wong-Toi, Andrea Balluchi, Jörg Preußig, Alberto Luigi Sangiovanni-Vincentelli, Yasuhiro Watanabe · 2002
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.