Computing Ordered Minimal Critical Sets

Fault Tree Analysis is widely used in industry for safety analysis purposes. Correct manual construction of fault trees is difficult, therefore automatic techniques like DCCA have been developed. Nevertheless the resulting minimal critical sets do not contain any information about possible temporal ordering of the failures. On the other hand, in safety critical application, systems are often equipped with backup facilities. This means that a failure in the main system has no longer consequences after the backup system has started to work. In this situation an analysis that does not incorporate temporal ordering of failures would be too pessimistic. In these cases information about temporal ordering of failures like temporal fault tree gates can greatly enhance the accuracy of the results of a safety analysis. We present a method to automatically deduce temporal ordering information for failures directly from system models and critical failure combinations resulting from FTA or DCCA, based on temporal logic and model checking.