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

摘要

核电站控制保护逻辑规模庞大、逻辑复杂,通常采用面向工程人员的图形语言开发,并自动生成C代码实现.如何保证图形语言到C代码转换的正确性,对核电运行安全意义重大.主要论述核安全级控制算法描述语言G-Lustre编译器的开发和形式化验证(语义保持性证明).该编译器将图形化的G-Lustre程序编译为行为等价的C代码,用定理证明辅助工具Coq开发编译器并证明其正确性.在关注安全关键软件及其形式化验证的环境中,这种经过验证的编译器是极其重要的,可保证源代码与编译产生的目标代码语义等价.该研究成果目前已在阳江5#、6#机组等8台核电机组中得到大规模应用.