Formal Verification of Safety Functions by Reinterpretation of Functional Block based Specifications

This paper presents the formal verification of a primary-to-secondary leaking (abbreviated as PRISE) safety procedure in a nuclear power plant (NPP). The software for the PRISE is defined by the Function Block Diagram specification method. Our approach to the formal verification of the PRISE safety procedure is based on the coloured Petri net (CPN) representation. The CPN model of the checked software is derived by reinterpretation from the FBD diagram, using a pre-developed library of CPN subnets. This results in a high-level, hierarchical coloured Petri net, that has an almost identical structure to the FBD specification. The state space of the CPN model was drastically reduced by "folding" equivalent states and trajectories into equivalence classes. Some of the safety properties could be proven based on the SCC (strongly connected components) graph of the reduced state space. Other properties were proven by CTL temporal logic based model checking.