Features

The dftlib library provides Python support for fault tree analysis, especially dynamic fault trees (DFT).

Import/Export

The library supports the import and export of (dynamic) fault trees from the following formats.

Galileo format

The Galileo format was originally introduced by the Galileo DFT tool. The original format is described in the Galileo manual and an extension version is described on the FFORT website. A collection of fault trees in the Galileo format is available in the FFORT collection.

JSON format

The library support a custom JSON format describing the DFT elements. The JSON format is compatible with the DFT visualization, the Storm model checker and the SAFEST tool.

Text format

The library also supports a simple text format of the following form:

AND(OR(A,B),C)

All three formats can be imported and exported with dftlib. Furthermore, export in anonymized form is also possible. This export anonymizes event names such that publication without confidential information is possible.

LaTeX generation

dftlib supports exporting fault trees as tikz code for LaTeX. When using the JSON format, the layouting information from the JSON format is preserved in the layout of the tikz code. The tikz export uses the DFT symbols defined in dft-tikz.tex. An example template is provided in resources/latex.

Fault tree simplification

The fault tree structure can be simplified through graph rewriting. The simplifications rules are in parts based on Junges et al. ‘Fault trees on a diet: automated reduction by graph rewriting’.

Analysis

The (dynamic) fault trees can be analysed with the Storm model checker as described here. The easiest approach is using the stormpy Python bindings for Storm. The steps for fault tree analysis are described in the stormpy documentation.

dftlib also supports analysis of DFT via encoding in satisfiability modulo theories (SMT).