Software safety is an important issue for embedded real-time control systems such as those found in nuclear power plants. When verifying safety-critical software, formal methods play critical roles in demonstrating compliance to regulatory requirements. The Korea Nuclear Instrumentation & Control System R&D Center (KNICS) project1 used the NuSCR formal specification language and tool-set to formally specify and verify software requirements for reactor protection systems (RPS) for the Advance Power Reactor-1400 (APR-1400). During the design and implementation phases, programmable logical controllers (PLC) software were written in IEC 61131-3 Function Block Diagram (FBD), and software safety was verified thoroughly. Each release of FBDs becomes official only when authorities have verified the software; two types of formal verification, model checking and equivalence checking, were applied to our FBDs. While the former examined whether or not FBD meets required properties, the latter determined behavioral equivalence between two FBD revisions.
Units of equivalence checking can vary from a small module to a whole system, and verification tasks fulfill various needs of FBD programmers and safety engineers. Formal verification contributes to the demonstration of the software safety of PLC programs written in FBD. This paper proposes how the Verification Interacting with Synthesis (VIS) system can automatically verify FBDs. VIS is widely used in hardware analysis, and with its Verilog front-end, it is also suitable for software analysis. VIS supports computational tree logic (CTL) model checking, language emptiness checking, combinational and sequential equivalence checking, cycle-based simulation, and hierarchical synthesis.
Although we explored the possibility of using VIS's sequential equivalence checking and simulation to verify FBD programs for the Advance Power Reactor-1400 (APR-1400) RPS, we chose Cadence Symbolic Model Verifier (SMV) for model checking because VIS's CTL model checking has restrictions when specifying properties. To enable VIS's equivalence checking using VIS, we first defined the semantics of FBD as a state transition system and developed rules for translating FBDs into semantically equivalent Verilog. We also implemented the FBD Verifier 1.1 software tool to automate the translation and then used it on a subset of FBDs for APR-1400's RPS. We found VIS equivalence to be effective.