A Technique for Demonstrating Safety and Correctness of Program Translators: Strategy and Case Study

The safety and correctness demonstration of program translators plays a critical role in software certification of digital I&C (Instrumentation & Control) systems in nuclear power plants. This paper proposes a strategy for the demonstration of the FBD to Verilog translator, which translates FBD programs into Verilog programs to synthesize FPGAs. It uses safety case to explain the strategy precisely and also implemented several supporting tools to derive evidences efficiently. A case study of a Korean nuclear power plant found the efficiency of the proposed demonstration strategy and supporting tools.