形式化验证技术在核电厂DCS中的应用研究  

Application of Formal Verification Technology in Nuclear Power Plant DCS

作　　者：侯荣彬 马权[1] 兰林 李勇[1] 杨斐 薛凯 吴亚波 Hou Rongbin;Ma Quan;Lan Lin;Li Yong;Yang Fei;Xue Kai;Wu Yabo(Science and Technology on Reactor System Design Technology Laboratory Nuclear Power Institute of China,Chengdu,610213,China)

机构地区：[1]中国核动力研究设计院核反应堆系统设计技术重点实验室,成都610213

出　　处：《仪器仪表用户》2020年第12期56-60,共5页Instrumentation

摘　　要：大部分软件开发中主要关注源代码级别的可靠性,通常默认编译器和操作系统是可信的。但是作为与安全攸关的软件还必须考虑编译器引入的误编译和操作系统漏洞引入的软件执行错误。形式化方法是一种有效提高软件可靠性的方法,本文对现有形式化技术在核电厂DCS中的可能应用方向进行研究,主要包括DCS逻辑算法的正确性验证、程序的可信编译、实时操作系统的验证。Source-code level reliability is the primary concern in most software development,and usually the default compiler and operation system are trusted.However,as a security-critical software execution errors.Formal method is an effective method to improve software reliability.In this paper,the possible applications of the existing formal techniques in DCS of nuclear power plants are studied.The main consideration of DCS logic algorithm is positive confirmation,program trusty compilation,real-time operation system verification.It is hoped that the formal method can be introduced to improve the software reliability based on the existing DCS design and development.

关 键 词：形式化验证 可信编译 核电厂仪控系统 软件可靠性 

分 类 号：TP273[自动化与计算机技术—检测技术与自动化装置]