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