Title :
A Verification Framework for FBD Based Software in Nuclear Power Plants
Author :
Yoo, Junbeom ; Cha, Sungdeok ; Jee, Eunkyoung
Author_Institution :
Div. of Comput. Sci. & Eng., Konkuk Univ., Seoul
Abstract :
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.
Keywords :
control engineering computing; nuclear power stations; power engineering computing; program verification; programmable controllers; PLC-based software; formal verification; function block diagram; model checker; nuclear reactor protection system; Computer science; Formal verification; IEC standards; Inductors; Power engineering and energy; Power generation; Power system modeling; Programmable control; Software safety; Software systems; FBD; equivalence checking; model checking; verification framework;
Conference_Titel :
Software Engineering Conference, 2008. APSEC '08. 15th Asia-Pacific
Conference_Location :
Beijing
Print_ISBN :
978-0-7695-3446-6
DOI :
10.1109/APSEC.2008.26