Formal modeling and verification of safety-critical software

Junbeom Yoo, Eunkyoung Jee, Sungdeok Cha

Research output: Contribution to journalArticlepeer-review

44 Citations (Scopus)


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
Issue number3
Publication statusPublished - 2009


  • 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


Dive into the research topics of 'Formal modeling and verification of safety-critical software'. Together they form a unique fingerprint.

Cite this