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

作者：侯荣彬; 马权; 兰林; 蒋维; 杨斐; 李昂; 李丹

来源：仪器仪表用户, 2021, 28(04): 47-51.

• 形式化验证
• 代码生成器
• 语义保持性
• 软件可靠性

代码生成器已经广泛应用于嵌入式控制软件的开发。对于安全攸关的软件系统,对软件可靠性有很高的要求,代码生成器作为工具软件被要求与所生成代码有相同的可靠性,形式化验证方法可有效保证代码生成器的可靠性。本文介绍了用于构建形式化验证代码生成器的方法,针对Lustre到C的代码生成器给出Lustre和C的抽象语法,并定义Lustre到C翻译过程的语义保持性。

• 单位
  中国核动力研究设计院