A safety-focused verification using software fault trees

Sungdeok Cha, Junbeom Yoo

Research output: Contribution to journalArticle

10 Citations (Scopus)

Abstract

When developing safety-critical software such as reactor protection systems (RPS) in nuclear power plants, a demonstration of software trust (e.g., safety) is not only absolutely essential but also usually mandated by government authorities. While automated generation of fault trees has become possible with increased use of formal specifications, industrial use of fault trees has been limited primarily to safety demonstrations that the system is free from behavior captured in the root node. In this paper, we propose to extend the use of automated fault tree for verification purposes. As a fault tree represents an abstract and partial behavioral model of software on credible causes leading to a hazard, it must still satisfy various properties (e.g., fairness, correctness). Verification of a fault tree is useful when developing safety-critical software because (1) it strengthens a safety-focused software development process; (2) it provides an opportunity to detect potentially critical errors early; and (3) it is less likely to experience a state explosion problem. This paper demonstrates how to convert a fault tree into a semantically equivalent logic formula so that they can be subject to formal verification using tools like Verification Interacting with Synthesis (VIS). We evaluated the feasibility of FTA's applicability as a verification tool on a prototype model of a nuclear power reactor protection system (RPS) software to be deployed in plants under construction in Korea.

Original languageEnglish
Pages (from-to)1272-1282
Number of pages11
JournalFuture Generation Computer Systems
Volume28
Issue number8
DOIs
Publication statusPublished - 2012 Oct

Keywords

  • Combinational equivalence checking
  • Safety analysis
  • Software fault tree
  • Software verification

ASJC Scopus subject areas

  • Software
  • Hardware and Architecture
  • Computer Networks and Communications

Fingerprint Dive into the research topics of 'A safety-focused verification using software fault trees'. Together they form a unique fingerprint.

  • Cite this