Compositional Synthesis of Temporal Fault Trees from State Machines

Dependability analysis of a dynamic system which is embedded with several complex interrelated components raises two main problems. First, it is difficult to represent in a single coherent and complete picture how the system and its constituent parts behave in conditions of failure. Second, the analysis can be unmanageable due to a considerable number of failure events which increases with the number of components involved. To remedy this problem, in this paper we outline a scalable analysis approach that converts failure behavioural models - state machines (SMs) - to temporal fault trees (TFTs), which can then be analysed using Pandora (a recent technique for introducing temporal logic to fault trees). The improved scalability of the approach stems from a compositional synthesis of the TFTs (generated from the individual component SMs) for Pandora analysis. We show, by using a Generic Triple Redundant (GTR) system, how the approach enables a more accurate and full analysis of an increasingly complex system.