Development of a safety critical software requirements verification method with combined CPN and PVS: a nuclear power plant protection system application |
| |
Authors: | Han Seong Son Poong Hyun Seong |
| |
Affiliation: | Department of Nuclear Engineering, KAIST, 373-1 Kusong-dong, Yusong-gu, Taejon 305-701, South Korea |
| |
Abstract: | Safety-critical software systems such as certain nuclear instrumentation and control (NI&C) systems should be developed with thorough verification. This study presents a method of software requirement verification with a case study for a nuclear power plant (NPP) protection system. The verification introduces colored petri net (CPN) for system modeling and prototype verification system (PVS) for mathematical verification. In order to aid flow-through from modeling by CPN to mathematical proof by PVS, an information extractor from CPN models has been developed in this paper. In order to convert the extracted information to the PVS specification language, a translator has also been developed. This combined method has been applied to the functional requirements of the Wolsong NPP Shut Down System #2 (SDS2); logical properties of the requirements were verified. Through this research, guidelines and a tool support for the use of formal methods have been developed for application to NI&C software verification. |
| |
Keywords: | Requirement verification Prototype verification system Colored petri net |
本文献已被 ScienceDirect 等数据库收录! |