同步数据流语言输入结构体的可信翻译  

Trustworthy Translation of Synchronous Data-flow Language Input Structures

作　　者：刘莛杨 吴锡[1] 杨斐 侯荣彬 马权[2] 王汝桥 梁根华 LIU Ting-Yang;WU Xi;YANG Fei;HOU Rong-Bin;MA Quan;WANG Ru-Qiao;LIANG Gen-Hua(School of Computer Science,Chengdu University of Information Technology,Chengdu 610225,China;Science and Technology on Reactor System Design Technology Laboratory,Nuclear Power Institute of China,Chengdu 610213,China)

机构地区：[1]成都信息工程大学计算机学院,成都610225 [2]中国核动力研究设计院核反应堆系统设计技术重点实验室,成都610213

出　　处：《计算机系统应用》2023年第6期269-277,共9页Computer Systems & Applications

基　　金：四川省科技厅科技计划(2020JDTD0020,2022YFG0042);四川科技厅重大科技专项(2019ZDZX0007,2022ZDZX0008)。

摘　　要：为最大程度地减少同步数据流语言编译过程中由编译器引入的错误,需要利用形式化方法自动生成代码,保证编译器产生的代码能够应用于核能仪控系统.本研究使用定理证明工具Coq,对同步数据流语言Lustre到Clight的主节点输入结构翻译阶段涉及的语法、语义及翻译算法进行了形式化定义,并完成翻译算法的形式化证明.研究表明这种经过形式化的编译器能够生成与源代码行为一致的可信目标代码,同时生成的目标代码能够很好满足核能仪控系统的执行规范.Formal methods are required for the automatic generation of codes to ensure that the code generated by the compiler can be applied to nuclear power instrument and control systems and thus minimize the errors introduced by the compiler during the compilation of synchronous data-flow languages.This study uses the theorem proving tool Coq to formally define the syntax,semantics,and translation algorithms involved in the translation phase of the master-node input structure of the synchronous data-flow language from Lustre to Clight and completes the formal proof of the translation algorithm.It is shown that this formalized compiler can generate credible target code that is consistent with the behavior of the source code,and meanwhile,the generated target code can well satisfy the implementation specifications of nuclear power instrument and control systems.

关 键 词：同步数据流语言 形式化验证 仪控系统 可信编译器 

分 类 号：TP314[自动化与计算机技术—计算机软件与理论]