The Dynamic Fault Tree Rare Event Simulator

Carlos E. Budde*, Enno Ruijters, Mariëlle Stoelinga

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingChapterAcademicpeer-review

2 Citations (Scopus)
59 Downloads (Pure)


The dynamic-fault-tree rare event simulator, DFTRES, is a statistical model checker for dynamic fault trees (DFTs), supporting the analysis of highly dependable systems, e.g. with unavailability or unreliability under 10^(-30). To efficiently estimate such low probabilities, we apply the Path-ZVA algorithm to implement Importance Sampling with minimal user input. Calculation speed is further improved by selective automata composition and bisimulation reduction. DFTRES reads DFTs in the Galileo or JANI textual formats. The tool is written in Java 11 with multi-platform support, and it is released under the GPLv3. In this paper we describe the architecture, setup, and input language of DFTRES, and showcase its accurate estimation of dependability metrics of (resilient) repairable DFTs from the FFORT benchmark suite.

Original languageEnglish
Title of host publicationQuantitative Evaluation of Systems
Subtitle of host publication17th International Conference, QEST 2020, Vienna, Austria, August 31 – September 3, 2020, Proceedings
EditorsMarco Gribaudo, David N. Jansen, Anne Remke
Place of PublicationCham
Number of pages6
ISBN (Electronic)978-3-030-59854-9
ISBN (Print)978-3-030-59853-2
Publication statusPublished - 2020
Event17th International Conference on Quantitative Evaluation Systems, QEST 2020 - Online event, Vienna, Austria
Duration: 31 Aug 20203 Sept 2020
Conference number: 17

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349
NameTheoretical Computer Science and General Issues


Conference17th International Conference on Quantitative Evaluation Systems, QEST 2020
Abbreviated titleQEST 2020


  • 22/2 OA procedure


Dive into the research topics of 'The Dynamic Fault Tree Rare Event Simulator'. Together they form a unique fingerprint.

Cite this