Formal modeling and verification of safety-critical software

Junbeom Yoo, Eunkyoung Jee, Sungdeok Cha

    Research output: Contribution to journalArticlepeer-review

    48 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

    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

    Fingerprint

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

    Cite this