翻译确认方法在核安全级GCG中的应用研究

Application Research of Translation Validation in Nuclear Safety-level Graphic Code Generator

在核安全级数字化仪控系统中,人机交互安全控制显示装置的显示内容和控制逻辑由图形化组态工具实现。由于显示内容规模庞大,结构复杂,如何保证实现从图形到C转换的图形代码生成器(GCG)的正确性是一个难题,通过引入形式化验证方法对GCG生成过程的正确性进行验证。本文在对两种形式化验证技术比较并结合应用场景分析之后,选取了翻译确认方法,并通过示例说明了方法的可行性,为之后图形代码生成器的形式化验证工作奠定了基础。

In the digital control system of nuclear safety level, the display content and control logic of HMI （Human Machine Interlace） safety control display device are realized by graphical configuration tool. Because the display content in large scale, complex structure, how to ensure the realization of the conversion from graphics to C graphic code generator is correct is a problem, verified the correctness of the GCG by introducing a formal verification method. In this paper, based on the analysis of two kinds of formal verification technology and GCG application scenarios, selects the translation validation method, and illustrates the feasibility of the method by example, lays the foundation for the later formal verification of the graphic code generator.