Non-Intrusive System-Level Fault Tolerance for an Electronic Throttle Controller

This paper describes the methodology used to add nonintrusive system-level fault tolerance to an electronic throttle controller. The original model of the throttle controller is a hybrid system created at a major automotive company. We use Gurkh as a framework within which we translate the hybrid model into a set of timed automata and perform analysis using formal methods. The first step of the translation process is to transform the hybrid model and its static schedule into Gurkh’s preemptive tasking paradigm. Using the UPPAAL tool, we then check the correctness of the resulting set of timed-automata by formally verifying reachability and timing properties. We also propose a method for quantifying the quality of the translation by estimating the amount of jitter thence introduced. The final step is the implementation of a Monitoring Chip based on the formal system model. The chip provides non-intrusive "out-of-path" and timing error detection which in turn allows for fault tolerance at a system level.