UML Statechart Fault Tree Generation By Model Checking

The safety analysis of workflows requires a key creative step where safety engineers imagine what undesirable events can occur under which conditions. We present a framework for the automated generation of fault trees from UML models extended with probabilistic non-deterministic branching. We present an algorithm that allows for exhaustive generation of possible error states that could arise during model execution, where the generated error states allow for both fail-stop behaviour and continued system execution.

By employing stochastic model checking we calculate the probabilities of reaching each non-error state of the system. Each generated error state is assigned a variable indicating its individual probability of occurrence. Our method can determine the probability of combined faults occurring, while accounting for the basic probabilistic structure of the system being modelled enabling a comprehensive fault tree to be generated, where expected mean values of reward structures can be calculated at points of failure.