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

发布时间：2024-04-11 22:38

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

【文章页数】：5 页

【部分图文】：

图1带有翻译验证的代码生成过程

在可信代码生成器形式化验证领域，JohnMccarthy等人已经做了大量工作[7-10]，但仍然无法自动证明给定的优化编译器的目标语言和源语言语义的一致性。如果不能证明代码生成器本身的正确性，也许可以检查每个编译过程的正确性。这启发了翻译验证技术，翻译验证的概念最早由Pnuel....

图2对代码生成器本身进行证明的开发流程图

另一种形式化开发可信代码生成器的方法是对代码生成器本身进行证明。这是一种将源语言的语法、语义模型及其满足规范的性质抽象为逻辑公式，然后使用逻辑推理技术来证明其语义一致性的技术，是最严格的开发方式。这种方法和数理逻辑相联系，常使用高阶逻辑系统进行形式化描述，可通过Coq[18]、I....

图3Velus架构图

学术界做了许多关于Lustre语言特性的形式化研究，JakubiecL[24]等人在Coq中使用归纳类型定义了Lustre语言的一个子集；G.Hamon[25]等人研究了同步数据流语言Lucid的高阶特性，并完成了Lucid时钟演算；E.Gimenez等人在开发Scade3代码....

本文编号：3951250