From timed automata to timed failure propagation graphs

Embedded real-time systems are increasingly applied in safety-critical environments like cars or aircrafts. Even though the system design might be free from flaws, hazardous situations may still be caused at run-time by random faults due to the wear of physical components. Hazard analysis is based on fault trees or failure propagation models. These models are created at least partly manually. They are usually independent from the software models which are used for checking safety and liveness properties to avoid systematic faults. This is particularly bad in cases, where the software model contains manually specified operations to deal with random faults which have been identified by hazard analysis. These operations include replacing the faulty components by reconfiguration. We propose to generate a failure propagation model automatically from the software model to check whether the results of hazard analysis have been properly accounted in the specification of reconfiguration operations. In contrast to other approaches, our approach considers the real-time properties of the system and adds explicit failure propagation times based on using timed automata for model specification.