Systematic evaluation of fault trees using real-time model checker UPPAAL

Sungdeok Cha, Hanseong Son, Junbeom Yoo, Eunkyung Jee, Poong Hyun Seong

Research output: Contribution to journalArticlepeer-review

12 Citations (Scopus)


Fault tree analysis, the most widely used safety analysis technique in industry, is often applied manually. Although techniques such as cutset analysis or probabilistic analysis can be applied on the fault tree to derive further insights, they are inadequate in locating flaws when failure modes in fault tree nodes are incorrectly identified or when causal relationships among failure modes are inaccurately specified. In this paper, we demonstrate that model checking technique is a powerful tool that can formally validate the accuracy of fault trees. We used a real-time model checker UPPAAL because the system we used as the case study, nuclear power emergency shutdown software named Wolsong SDS2, has real-time requirements. By translating functional requirements written in SCR-style tabular notation into timed automata, two types of properties were verified: (1) if failure mode described in a fault tree node is consistent with the system's behavioral model; and (2) whether or not a fault tree node has been accurately decomposed. A group of domain engineers with detailed technical knowledge of Wolsong SDS2 and safety analysis techniques developed fault tree used in the case study. However, model checking technique detected subtle ambiguities present in the fault tree.

Original languageEnglish
Pages (from-to)11-20
Number of pages10
JournalReliability Engineering and System Safety
Issue number1
Publication statusPublished - 2003 Oct
Externally publishedYes


  • Fault tree analysis
  • Formal methods
  • Model checking
  • Software engineering

ASJC Scopus subject areas

  • Safety, Risk, Reliability and Quality
  • Industrial and Manufacturing Engineering


Dive into the research topics of 'Systematic evaluation of fault trees using real-time model checker UPPAAL'. Together they form a unique fingerprint.

Cite this