Reasoning about temporal faults using an activation logic

Abstract

Faults modelling is essential to anticipate failures in critical systems. Traditionally, Static Fault Trees (SFTs) are employed to this end, but Temporal and Dynamic Fault Trees (TFTs and DFTs) are gaining evidence due to their enriched power to model and detect intricate propagation of faults that lead to a failure. SFTs structure can be abstracted to Boolean expressions. An algebra with an operator to express order is needed to abstract TFT and DFT structures. These expressions for SFT, TFT, and DFT are called structure expressions. Architectural modelling languages, such as Architecture and Analysis Design Language (AADL), have been used to model components and systems relations, including modelling of faults, errors, failures, and fault propagation. AADL tools can perform Static Fault Tree Analysis, for the faults modelled using AADL’s Error Model Annex. In previous work, we showed an Algebra of Temporal Faults to analyse the order of occurrence of faults extending Boolean algebra to perform analysis for Temporal and Dynamic fault trees. In this work, we show a parametrized logic to express nominal and erroneous behaviours, including faults modelling, provided an algebra and a set of operational modes. We show how to use this logic together with the Algebra of Temporal Faults to analyse the occurrence of faults as well as their order and propagation. The logic created in this work is intended to help analysts to consider all possible situations in complex expressions with order-related operators, avoiding to miss some subtle (but relevant) combination.