Formal modeling and verification of safety-critical software

Junbeom Yoo, Eunkyoung Jee, Sungdeok Cha

Research output: Contribution to journalArticle

33 Citations (Scopus)

Abstract

Rigorous quality demonstration is important when developing safety-critical software such as a reactor protection system (RPS) for a nuclear power plant. Although using formal methods such as formal modeling and verification is strongly recommended, domain experts often reject formal methods for four reasons: there are too many candidate techniques, the notations appear complex, the tools often work only in isolation, and output is often too difficult for domain experts to understand. A formal-methods-based process that supports development, verification and validation, and safety analysis can help domain experts overcome these obstacles. Nuclear engineers can also use CASE tools to apply formal methods without having to know details of the underlying formalism. The authors spent more than seven years working with nuclear engineers in developing RPS software and applying formal methods. The engineers and regulatory personnel found the process effective and easy to apply with the integrated tool support.

Original languageEnglish
Pages (from-to)42-49
Number of pages8
JournalIEEE Software
Volume26
Issue number3
DOIs
Publication statusPublished - 2009 May 27

Fingerprint

Formal methods
Engineers
Nuclear power plants
Demonstrations
Personnel

Keywords

  • Analytical models
  • Computer aided software engineering
  • Control systems
  • Data mining
  • Formal methods
  • Formal specifications
  • Function block diagram (FBD)
  • Modeling
  • Safety
  • Safety-critical software
  • Software
  • Verification

ASJC Scopus subject areas

  • Software

Cite this

Formal modeling and verification of safety-critical software. / Yoo, Junbeom; Jee, Eunkyoung; Cha, Sungdeok.

In: IEEE Software, Vol. 26, No. 3, 27.05.2009, p. 42-49.

Research output: Contribution to journalArticle

Yoo, Junbeom ; Jee, Eunkyoung ; Cha, Sungdeok. / Formal modeling and verification of safety-critical software. In: IEEE Software. 2009 ; Vol. 26, No. 3. pp. 42-49.
@article{3121b7a9431b4b7fada0496bbeda5a46,
title = "Formal modeling and verification of safety-critical software",
abstract = "Rigorous quality demonstration is important when developing safety-critical software such as a reactor protection system (RPS) for a nuclear power plant. Although using formal methods such as formal modeling and verification is strongly recommended, domain experts often reject formal methods for four reasons: there are too many candidate techniques, the notations appear complex, the tools often work only in isolation, and output is often too difficult for domain experts to understand. A formal-methods-based process that supports development, verification and validation, and safety analysis can help domain experts overcome these obstacles. Nuclear engineers can also use CASE tools to apply formal methods without having to know details of the underlying formalism. The authors spent more than seven years working with nuclear engineers in developing RPS software and applying formal methods. The engineers and regulatory personnel found the process effective and easy to apply with the integrated tool support.",
keywords = "Analytical models, Computer aided software engineering, Control systems, Data mining, Formal methods, Formal specifications, Function block diagram (FBD), Modeling, Safety, Safety-critical software, Software, Verification",
author = "Junbeom Yoo and Eunkyoung Jee and Sungdeok Cha",
year = "2009",
month = "5",
day = "27",
doi = "10.1109/MS.2009.67",
language = "English",
volume = "26",
pages = "42--49",
journal = "IEEE Software",
issn = "0740-7459",
publisher = "IEEE Computer Society",
number = "3",

}

TY - JOUR

T1 - Formal modeling and verification of safety-critical software

AU - Yoo, Junbeom

AU - Jee, Eunkyoung

AU - Cha, Sungdeok

PY - 2009/5/27

Y1 - 2009/5/27

N2 - Rigorous quality demonstration is important when developing safety-critical software such as a reactor protection system (RPS) for a nuclear power plant. Although using formal methods such as formal modeling and verification is strongly recommended, domain experts often reject formal methods for four reasons: there are too many candidate techniques, the notations appear complex, the tools often work only in isolation, and output is often too difficult for domain experts to understand. A formal-methods-based process that supports development, verification and validation, and safety analysis can help domain experts overcome these obstacles. Nuclear engineers can also use CASE tools to apply formal methods without having to know details of the underlying formalism. The authors spent more than seven years working with nuclear engineers in developing RPS software and applying formal methods. The engineers and regulatory personnel found the process effective and easy to apply with the integrated tool support.

AB - Rigorous quality demonstration is important when developing safety-critical software such as a reactor protection system (RPS) for a nuclear power plant. Although using formal methods such as formal modeling and verification is strongly recommended, domain experts often reject formal methods for four reasons: there are too many candidate techniques, the notations appear complex, the tools often work only in isolation, and output is often too difficult for domain experts to understand. A formal-methods-based process that supports development, verification and validation, and safety analysis can help domain experts overcome these obstacles. Nuclear engineers can also use CASE tools to apply formal methods without having to know details of the underlying formalism. The authors spent more than seven years working with nuclear engineers in developing RPS software and applying formal methods. The engineers and regulatory personnel found the process effective and easy to apply with the integrated tool support.

KW - Analytical models

KW - Computer aided software engineering

KW - Control systems

KW - Data mining

KW - Formal methods

KW - Formal specifications

KW - Function block diagram (FBD)

KW - Modeling

KW - Safety

KW - Safety-critical software

KW - Software

KW - Verification

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

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

U2 - 10.1109/MS.2009.67

DO - 10.1109/MS.2009.67

M3 - Article

AN - SCOPUS:65749085859

VL - 26

SP - 42

EP - 49

JO - IEEE Software

JF - IEEE Software

SN - 0740-7459

IS - 3

ER -