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 journalArticle

12 Citations (Scopus)

Abstract

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
Volume82
Issue number1
DOIs
Publication statusPublished - 2003 Oct 1
Externally publishedYes

Fingerprint

Fault Tree
Failure modes
Model checking
Real-time
Evaluation
Failure Mode
Fault tree analysis
Safety Analysis
Thyristors
Nuclear energy
Model Checking
Model
Vertex of a graph
Engineers
Defects
Fault Tree Analysis
Cutset
Probabilistic Analysis
Timed Automata
Requirements

Keywords

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

ASJC Scopus subject areas

  • Mechanical Engineering
  • Safety, Risk, Reliability and Quality

Cite this

Systematic evaluation of fault trees using real-time model checker UPPAAL. / Cha, Sungdeok; Son, Hanseong; Yoo, Junbeom; Jee, Eunkyung; Seong, Poong Hyun.

In: Reliability Engineering and System Safety, Vol. 82, No. 1, 01.10.2003, p. 11-20.

Research output: Contribution to journalArticle

Cha, Sungdeok ; Son, Hanseong ; Yoo, Junbeom ; Jee, Eunkyung ; Seong, Poong Hyun. / Systematic evaluation of fault trees using real-time model checker UPPAAL. In: Reliability Engineering and System Safety. 2003 ; Vol. 82, No. 1. pp. 11-20.
@article{15a874af738d40b4a3cc76e86c34e046,
title = "Systematic evaluation of fault trees using real-time model checker UPPAAL",
abstract = "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.",
keywords = "Fault tree analysis, Formal methods, Model checking, Software engineering",
author = "Sungdeok Cha and Hanseong Son and Junbeom Yoo and Eunkyung Jee and Seong, {Poong Hyun}",
year = "2003",
month = "10",
day = "1",
doi = "10.1016/S0951-8320(03)00059-0",
language = "English",
volume = "82",
pages = "11--20",
journal = "Reliability Engineering and System Safety",
issn = "0951-8320",
publisher = "Elsevier Limited",
number = "1",

}

TY - JOUR

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

AU - Cha, Sungdeok

AU - Son, Hanseong

AU - Yoo, Junbeom

AU - Jee, Eunkyung

AU - Seong, Poong Hyun

PY - 2003/10/1

Y1 - 2003/10/1

N2 - 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.

AB - 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.

KW - Fault tree analysis

KW - Formal methods

KW - Model checking

KW - Software engineering

UR - http://www.scopus.com/inward/record.url?scp=0041528508&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0041528508&partnerID=8YFLogxK

U2 - 10.1016/S0951-8320(03)00059-0

DO - 10.1016/S0951-8320(03)00059-0

M3 - Article

AN - SCOPUS:0041528508

VL - 82

SP - 11

EP - 20

JO - Reliability Engineering and System Safety

JF - Reliability Engineering and System Safety

SN - 0951-8320

IS - 1

ER -