The tool provides a drag-&-drop interface to model systems graphically, specify and verify measures of interest, plot results, and do step-by-step simulation of models. Advanced users can use features like specifying custom properties, characterizing complex system behaviours (states using Boolean equations) and quantifying their probabilities.

Complex systems usually have dynamic behaviour because of e.g. spare components, failure sequence among components, functional dependencies, etc. The analysis of such systems is usually quite complex which is usually based on simulation or generalization techniques. Unlike others we implement formal verification techniques e.g. probabilistic model-checking, and thus provide exact results on measures of interest. For systems having large state space, we provide an iterative analysis approach providing upper and lower bounds on the exact values of measures as discussed below.

In order to compute exact results for measures, first the full state space is constructed, and then analyzed. However, many states in the state space only marginally contribute to the result. If one is interested in an approximation of the MTTF (or the reliability), these states are of minor interest. SAFEST provides an approach that generates the state-space on-the-fly, and then compute an upper and a lower bound to the exact results on a partially unfolded system, which might be much smaller as compared to the fully unfolded system. The approximation is sound ensuring the exact result lies between these two bounds.

SAFEST automates model-based risk assessment (MBRA) in parallel with model-based systems engineering (MBSE). By annotating safety aspects (e.g. redundancy, functional dependencies, failure ordering, etc.) in SysML 2.0 models, aur algorithm automatically extract relevant DFTs out of them. This reduces a lot of effort required in building DFTS manually from SysML 2.0 models.

SAFEST provides a graphical interface to plot and compare measures of interest e.g. reliability of different sub-systems, which is helpful in deciding maintenance schedules.

The idea is to interactively visualize the impact of a sequence of events in a model. For example, in DFTs the user selects one of the basic events (BE) that should fail first. Based on this, the status of other DFT elements is redetermined and then visualized (failed, operational, fail-safe, claiming in SPAREs, etc.). Afterwards, another BE is selected to fail and so forth. The main benefit of this feature is the understandaing of the behaviour of dynamic gates of DFTs, thus helping in building realistic models of systems.

Model parameters can be provided in the form of constants, real expressions, and failure distributions. Failure distributions can be specified manually or evaluated from data sets that are generated during system operations. Furthermore, weighted failure distributions are also supported, allowing combining two or more failure distributions into one failure distribution. For example, combining failure distributions from international reliability standards with empirical distributions (calculated from field data) allows for having more meaningful distributions for system analysis in production.

The Backend Computational Engine SAFEST is powered by [Storm] -- a state-of-the-art probabilistic model checker. Storm is a tool for the analysis of systems involving random or probabilistic phenomena. Given an input model and a quantitative specification, it can determine whether the input model conforms to the specification. It has been designed with performance and modularity in mind. SAFEST interacts with the DFT module of Storm -- storm-dft -- using a Python binding [stormpy] and utilizes the rich features of [diftlib] library.

The SAFEST tool has been validated against multiple models given on the Quantitative Verification Benchmark Set as well as on FFORT fault tree forest websites. The Quantitative Verification Benchmark Set is a collection of probabilistic models to serve as a benchmark set for the benefit of algorithm and tool developers. Whereas, FFORT is a collection of fault trees gathered from scientific literature and open industrial reports by University of Twente, the Netherlands.