UML Statechart Fault Tree Generation By Model Checking

Creating fault tolerant and efficient process work-flows poses a significant challenge. Individual faults, defined as an abnormal conditions or defects in a component, equipment, or sub-process, must be handled so that the system may continue to operate, and are typically addressed by implementing various domain specific safeguards. In complex systems, in-dividual faults may combine to give rise to system failure, defined as a state or condition of not meeting a desirable or intended objective. The safety analysis of such systems is labour-intensive and requires a key creative step where safety engineers imagine what undesirable events can occur under which conditions.
Fault Tree Analysis (FTA) attempts to analyse the failure of systems by composing logic diagrams of separate individual faults to determine the probabil-ity of larger compound faults occurring. FTA is a commonly used method to derive and analyse poten-tial failures and their impact on overall system relia-bility and safety. FTA has seen extensive refinement and widespread adoption and is today considered a proven and accepted reliability engineering tech-nique, often required for regulatory approval of sys-tems. However, fault trees are typically manually constructed and determining the probabilities of faults occurring in systems which exhibit stochastic behaviour in the course of their correct execution is difficult, time-consuming and error prone.
Typically a FTA is based on an informal descrip-tion of the underlying system, or requires modelling the system in an FTA specific language. This makes it difficult to check the consistency of the analysis, because it is possible that causes are noted in the tree which do not lead to the failure (incorrectness) or that some causes of failure are overlooked (incom-pleteness).
To avoid these deficiencies, our approach derives the fault tree directly from the formal system model, under the assumption that any state can fail.
We present a framework for the automated gener-ation of fault trees from models of real-world pro-cess workflows, expressed in a formalised subset of the popular Business Process Modelling and Nota-tion (BPMN) language. To capture uncertainty and unreliability in workflows, we extend this formalism with probabilistic non-deterministic branching.We present an algorithm that allows for exhaustive gen-eration of possible error states that could arise in ex-ecution of the model, where the generated error states allow for both fail-stop behaviour and contin-ued system execution.
By employing stochastic model checking we cal-culate the probabilities of reaching each non-error state of the system. Each generated error state is as-signed a variable indicating its individual probability of occurrence. Our method can determine the proba-bility of combined faults occurring, while accounting for the basic probabilistic structure of the system be-ing modelled. From these calculations, a comprehen-sive fault tree is generated. Further, we show that annotating the model with rewards (data) allows the expected mean values of reward structures to be cal-culated at points of failure..