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

Volume

4

fYear

1998

fDate

16-18 Dec 1998

Firstpage

4271

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Decision and Control, 1998. Proceedings of the 37th IEEE Conference on

Conference_Location

Tampa, FL

ISSN

0191-2216

Print_ISBN

0-7803-4394-8

Type

conf

DOI

10.1109/CDC.1998.761976

Filename

761976