A verification framework for FBD based software in nuclear power plants

Yoo Junbeom, Cha Sungdeok, Jee Eunkyoung

Research output: Contribution to journalConference articlepeer-review

13 Citations (Scopus)


Formal verification of Function Block Diagram (FBD) based software is an essential task when replacing traditional relay-based analog system with PLC-based software in nuclear reactor protection system (RPS). FBD programs are developed manually and revised frequently in process of development. There are a set of properties to be verified formally, which all FBD releases should satisfy. Whenever FBDs are modified, there is also a need to verify behavioral equivalence of subsequently modified FBDs. This paper proposes a software verification framework for FBD software in nuclear power plants. It uses SMV model checker for verifying whether an FBD meets its required properties, and VIS verification system for checking behavioral equivalence between modified FBDs. A case study, conducted using a nuclear power plant shutdown system being developed in Korea, demonstrated that the proposed verification framework is effective and useful.

Original languageEnglish
Article number4724570
Pages (from-to)385-392
Number of pages8
JournalNeonatal, Paediatric and Child Health Nursing
Publication statusPublished - 2008
Event15th Asia-Pacific Software Engineering Conference, APSEC 2008 - Beijing, China
Duration: 2008 Dec 22008 Dec 5

ASJC Scopus subject areas

  • Pediatrics


Dive into the research topics of 'A verification framework for FBD based software in nuclear power plants'. Together they form a unique fingerprint.

Cite this