代码生成器形式化验证技术研究  

Research on Formal Verification of Code Generator

作　　者：侯荣彬 马权[1] 兰林 蒋维 杨斐 李昂 李丹 Hou Rongbin;Ma Quan;Lan Lin;Jiang Wei;Yang Fei;Li Ang;Li Dan(Science and Technology on Reactor System Design Technology Laboratory Nuclear Power Institute of China,Chengdu,610213,China)

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

出　　处：《仪器仪表用户》2021年第4期47-51,共5页Instrumentation

摘　　要：代码生成器已经广泛应用于嵌入式控制软件的开发。对于安全攸关的软件系统,对软件可靠性有很高的要求,代码生成器作为工具软件被要求与所生成代码有相同的可靠性,形式化验证方法可有效保证代码生成器的可靠性。本文介绍了用于构建形式化验证代码生成器的方法,针对Lustre到C的代码生成器给出Lustre和C的抽象语法,并定义Lustre到C翻译过程的语义保持性。Code generator has been widely used in the development of embedded control software. For software with critical security, there are high requirement for software reliability. Code generator as a tool software is required to have the same reliability as the generated code. Formal verification method can effectively ensure the reliability of code generator. This article introduce the method used to build a formal verification code generator. The abstract syntax of Lustre and C is given for the code generator from Lustre to C, and the semantic retention of Lustre to C translation process is defined.

关 键 词：形式化验证 代码生成器 语义保持性 软件可靠性 

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