核安全级控制算法描述语言的可信编译研究  

Research on Trusted Compilation of Nuclear Safety Level Control Algorithm Description Language

作　　者：张智慧[1] 冀建伟[1] ZHANG Zhihui;JI Jianwei(China Techenergy Co.,Ltd.,Beijing 100094,China)

机构地区：[1]北京广利核系统工程有限公司,北京100094

出　　处：《自动化仪表》2021年第S01期106-111,共6页Process Automation Instrumentation

摘　　要：核电站控制保护逻辑规模庞大、逻辑复杂,通常采用面向工程人员的图形语言开发,并自动生成C代码实现。如何保证图形语言到C代码转换的正确性,对核电运行安全意义重大。主要论述核安全级控制算法描述语言G-Lustre编译器的开发和形式化验证(语义保持性证明)。该编译器将图形化的G-Lustre程序编译为行为等价的C代码,用定理证明辅助工具Coq开发编译器并证明其正确性。在关注安全关键软件及其形式化验证的环境中,这种经过验证的编译器是极其重要的,可保证源代码与编译产生的目标代码语义等价。该研究成果目前已在阳江5^(#)、6^(#)机组等8台核电机组中得到大规模应用。The control and protection logic of nuclear power plant is large in scale and complex in logic,which is usually developed by graphic language oriented to engineers and realized by automatic generation of C code.How to ensure the correctness of graphic language to C code conversion is of great significance to the safety of nuclear power operation.The development and formal verification of G-lustre compiler for nuclear safety level control algorithm description language(semantic preserving proof)is discussed.The compiler compiles graphical G-Lustre programs into behaviorally equivalent C code,and develops the compiler using the theorem proving aid tool Coq and proves its correctness.In an environment focused on security-critical software and its formal validation,such a validated compiler is extremely important to ensure semantic equivalence between source code and compiled target code.The research results have been widely used in 8 nuclear power units such as Yangjiang 5^(#),6^(#)unit.

关 键 词：核安全级 编译器 形式化验证 定理证明 COQ ACG R2L L2C 

分 类 号：TH-39[机械工程]