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

Research and Progress of Lustre Trusted Code Generator

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

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

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

摘　　要：安全攸关的嵌入式领域广泛使用基于Lustre语言描述的图形化逻辑。工程师通过图形化逻辑建模工具编写控制逻辑,再通过代码生成器把控制逻辑转换成可执行代码下装到嵌入式设备中运行。因此,如何保证代码生成器生成代码的正确性成为关注的焦点。通过测试等传统方法来确保代码生成器的正确性,其覆盖率有限,无法完全解决误编译的问题;而把形式化方法用于开发代码生成器,通过逻辑推理的方式证明代码生成的正确性,将最大限度地解决误编译的问题,使其成为一个可信代码生成器。本文首先分析了同步数据流语言Lustre的语法特征,然后介绍了Lustre语言可信代码生成器的研究进展和形式化开发方法,为开发应用于嵌入式安全攸关领域的Lustre可信代码生成器提供借鉴。Graphical logic based on the description of the Lustre language is widely used in security-relevant embedded fields.The engineer develop the control logics through a code generator and downloads it to the embedded device to run.Therefore,how to ensure the reliability of the Lustre code generator has become the focus of attention.Traditional development methods such as testing have limited coverage and cannot solve the problem of mis-compilation.However,using formal methods to develop trusted code generators and proving the correctness of the code through logical reasoning will maximize the resolution of mis-compilation.This article briefly analyzes the characteristics of the synchronous date flow language Lustre,mainly introduces the research progress of the Lustre trusted code generator,Provides a new idea for developing a Lustre trusted code generator.

关 键 词：可信代码生成 LUSTRE 形式化验证 定理证明 翻译验证 安全攸关 

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