Lustre语言可信代码生成器研究进展

作     者：兰林 马权 侯荣彬 蒋维 杨斐 Lan Lin;Ma Quan;Hou Rongbin;Jiang Wei;Yang Fei

作者机构：中国核动力研究设计院核反应堆系统设计技术重点实验室成都610213 

出 版 物：《仪器仪表用户》 (Instrumentation)

年 卷 期：2020年第27卷第5期

页      面：68-72页

学科分类：08[工学] 0835[工学-软件工程] 0802[工学-机械工程] 080201[工学-机械制造及其自动化] 

主　　题：可信代码生成 Lustre 形式化验证 定理证明 翻译验证 安全攸关 

摘      要：安全攸关的嵌入式领域广泛使用基于Lustre语言描述的图形化逻辑。工程师通过图形化逻辑建模工具编写控制逻辑,再通过代码生成器把控制逻辑转换成可执行代码下装到嵌入式设备中运行。因此,如何保证代码生成器生成代码的正确性成为关注的焦点。通过测试等传统方法来确保代码生成器的正确性,其覆盖率有限,无法完全解决误编译的问题;而把形式化方法用于开发代码生成器,通过逻辑推理的方式证明代码生成的正确性,将最大限度地解决误编译的问题,使其成为一个可信代码生成器。本文首先分析了同步数据流语言Lustre的语法特征,然后介绍了Lustre语言可信代码生成器的研究进展和形式化开发方法,为开发应用于嵌入式安全攸关领域的Lustre可信代码生成器提供借鉴。