Formal static fault tree analysis

Fault tree analysis (FTA) is a traditional informal reliability and safety analysis technique. FTA is basically a combinational model in which standard Boolean logic constructs, such as AND and OR gates, are used to decompose the fault events. Several dynamic constructs, such as Functional Dependency (FDEP) and Priority AND (PAND) gates, are also proposed to handle dynamic behaviors of system failure mechanisms. In this article, we focus on some paradoxes and constraints of the traditional FDEP and PAND gates, and present our static solutions to these dynamic gates. The proposed static fault tree model is formalized with Maude, an executable algebraic formal specification language. Two example fault tolerant parallel processor (FTPP) configurations are used to demonstrate our static fault tree model.