A systematic verification of behavioral consistency between FBD design and ANSI-C implementation using HW-CBMC

Controllers in safety critical systems such as nuclear power plants often use the Function Block Diagram (FBD) to design software embedded in the PLC (Programmable Logic Controller). Software engineers develop FBD programs manually, while engineering tools provided by PLC vendors translate them into ANSI-C programs mechanically. Every new PLC and its software engineering tool should demonstrate the so-called FBD-to-C translatorʹs correctness thoroughly. This paper proposes a verification process which can efficiently verify the translatorʹs correctness using the model checking technique. The HW-CBMC model checker verifies the behavioral consistency between FBD and ANSI-C programs formally according to the process and templates which this paper proposes. We also developed a CASE tool ‘CWrapper’ and performed a case study with simplified examples of the APR-1400 (Advanced Power Reactor-1400) nuclear reactor protection system in Korea.