Loading...
Please wait, while we are loading the content...
Similar Documents
Formal verification of an automotive engine controller in cutoff mode (1998).
| Content Provider | CiteSeerX |
|---|---|
| Author | Villa, Tiziano Wong-Toi, Howard Balluchi, Andrea Preußig, Jörg Sangiovanni-Vincentelli, Alberto L. Alberto, Yosinori Watanabe Preußig |
| 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. 1 Introduction 1.1 Verification of embedded systems Embedded systems are informally defined as a collection of programmable parts surrounded by ASICs and other standard components that interact continuously with an environment through sensors and actuators. Embedded systems often are used in life-critical situations, where reliability and safety are more important criteria than performance. The closed-loop system---which involves a discrete controller and its analog environment---has behaviors that are inherently hybrid, i.e., ... |
| File Format | |
| Publisher Date | 1998-01-01 |
| Access Restriction | Open |
| Subject Keyword | Cutoff Mode Formal Verification Automotive Engine Controller Analog Environment Discrete Controller Programmable Part Hybrid Controller Important Criterion Fuel Injection Life-critical Situation Closed-loop System Model Checker Hytech Engine Control Hybrid Automaton Performance Property Embedded System Standard Component |
| Content Type | Text |
