Dynamic model-based safety analysis: from state machines to temporal fault trees

Finite state transition models such as State Machines (SMs) have become a prevalent paradigm for the description of dynamic systems. Such models are well-suited to modelling the behaviour of complex systems, including in conditions of failure, and where the order in which failures and fault events occur can affect the overall outcome (e.g. total failure of the system). For the safety assessment though, the SM failure behavioural models need to be converted to analysis models like Generalised Stochastic Petri Nets (GSPNs), Markov Chains (MCs) or Fault Trees (FTs). This is particularly important if the transformed models are supported by safety analysis tools.This thesis, firstly, identifies a number of problems encountered in current safety analysis techniques based on SMs. One of the existing approaches consists of transforming the SMs to analysis-supported state-transition formalisms like GSPNs or MCs, which are very powerful in capturing the dynamic aspects and in the evaluation of safety measures. But in this approach, qualitative analysis is not encouraged; here the focus is primarily on probabilistic analysis. Qualitative analysis is particularly important when probabilistic data are not available (e.g., at early stages of design). In an alternative approach though, the generation of combinatorial, Boolean FTs has been applied to SM-based models. FTs are well-suited to qualitative analysis, but cannot capture the significance of the temporal order of events expressed by SMs. This makes the approach potentially error prone for the analysis of dynamic systems. In response, we propose a new SM-based safety analysis technique which converts SMs to Temporal Fault Trees (TFTs) using Pandora — a recent technique for introducing temporal logic to FTs. Pandora provides a set of temporal laws, which allow the significance of the SM temporal semantics to be preserved along the logical analysis, and thereby enabling a true qualitative analysis of a dynamic system. The thesis develops algorithms for conversion of SMs to TFTs. It also deals with the issue of scalability of the approach by proposing a form of compositional synthesis in which system large TFTs can be generated from individual component SMs using a process of composition. This has the dual benefits of allowing more accurate analysis of different sequences of faults, and also helping to reduce the cost of performing temporal analysis by producing smaller, more manageable TFTs via the compositionality.The thesis concludes that this approach can potentially address limitations of earlier work and thus help to improve the safety analysis of increasingly complex dynamic safety-critical systems