| Lustre语言可信代码生成器研究进展 |
| |
| 引用本文： | 兰林,马权,侯荣彬,蒋维,杨斐.Lustre语言可信代码生成器研究进展[J].仪器仪表用户,2020(5):68-72. |
| |
| 作者姓名： | 兰林 马权 侯荣彬 蒋维 杨斐 |
| |
| 作者单位： | 中国核动力研究设计院核反应堆系统设计技术重点实验室 |
| |
| 摘 要： | 安全攸关的嵌入式领域广泛使用基于Lustre语言描述的图形化逻辑。工程师通过图形化逻辑建模工具编写控制逻辑,再通过代码生成器把控制逻辑转换成可执行代码下装到嵌入式设备中运行。因此,如何保证代码生成器生成代码的正确性成为关注的焦点。通过测试等传统方法来确保代码生成器的正确性,其覆盖率有限,无法完全解决误编译的问题;而把形式化方法用于开发代码生成器,通过逻辑推理的方式证明代码生成的正确性,将最大限度地解决误编译的问题,使其成为一个可信代码生成器。本文首先分析了同步数据流语言Lustre的语法特征,然后介绍了Lustre语言可信代码生成器的研究进展和形式化开发方法,为开发应用于嵌入式安全攸关领域的Lustre可信代码生成器提供借鉴。
|
| 关 键 词： | 可信代码生成 LUSTRE 形式化验证 定理证明 翻译验证 安全攸关 |
Research and Progress of Lustre Trusted Code Generator |
| |
| Lan Lin,Ma Quan,Hou Rongbin,Jiang Wei,Yang Fei.Research and Progress of Lustre Trusted Code Generator[J].Electronic Instrumentation Customer,2020(5):68-72. |
| |
| Authors: | Lan Lin Ma Quan Hou Rongbin Jiang Wei Yang Fei |
| |
| Affiliation: | (Science and Technology on Reactor System Design Technology Laboratory Nuclear Power Institute of China,Chengdu,610213,China) |
| |
| Abstract: | |
| |
| Keywords: | trusted code generation lustre formal methods theorem proof translation validation safety-critical |
| 本文献已被 CNKI 维普 等数据库收录！ |
|
