| 同步数据流语言输入结构体的可信翻译 |
| |
| 作者姓名： | 刘莛杨 吴锡 杨斐 侯荣彬 马权 王汝桥 梁根华 |
| |
| 作者单位： | 成都信息工程大学 计算机学院, 成都 610225;中国核动力研究设计院 核反应堆系统设计技术重点实验室, 成都 610213 |
| |
| 基金项目： | 四川省科技厅科技计划(2020JDTD0020, 2022YFG0042); 四川科技厅重大科技专项(2019ZDZX0007, 2022ZDZX0008) |
| |
| 摘 要： | 为最大程度地减少同步数据流语言编译过程中由编译器引入的错误,需要利用形式化方法自动生成代码,保证编译器产生的代码能够应用于核能仪控系统.本研究使用定理证明工具Coq,对同步数据流语言Lustre到Clight的主节点输入结构翻译阶段涉及的语法、语义及翻译算法进行了形式化定义,并完成翻译算法的形式化证明.研究表明这种经过形式化的编译器能够生成与源代码行为一致的可信目标代码,同时生成的目标代码能够很好满足核能仪控系统的执行规范.
|
| 关 键 词： | 同步数据流语言 形式化验证 仪控系统 可信编译器 |
| 收稿时间： | 2022-11-04 |
| 修稿时间： | 2022-12-10 |
|
| 点击此处可从《计算机系统应用》浏览原始摘要信息 |
|
点击此处可从《计算机系统应用》下载免费的PDF全文 |
|
