HyRev: A Tool for the Automatic Generation of Real-Time Routines for Enabling Fail-Safe Control in a Class of Safety-Critical Embedded Systems Using Backwards Reachability Analysis

A fail-safe embedded system is a system that will transit to a safe state in the event of a system failure. In these situations the system will typically switch from the normal, now faulty, operational mode to an emergency control mode which will ensure the safety of the system. The switch will have a hard real-time constraint if the results of a temporal failure are catastrophic in nature. Many industry-critical systems fall into this category, such as industrial plants and vehicles. We show how hybrid automata can be used to model a failing system and how backwards reachability analysis of this model and a given model of the emergency control can be used to prove the conditions under which safety switching will always succeed in ensuring fail-safe behavior. To show the feasibility of the technique we present the prototype tool HyRev. The tool takes a description of the emergency control system and the catastrophic bad states of the system as input and produces a safety check routine with a well-defined worst-case execution time as output, which can then be run on the embedded system.