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

为最大程度地减少同步数据流语言编译过程中由编译器引入的错误,需要利用形式化方法自动生成代码,保证编译器产生的代码能够应用于核能仪控系统.本研究使用定理证明工具Coq,对同步数据流语言Lustre到Clight的主节点输入结构翻译阶段涉及的语法、语义及翻译算法进行了形式化定义,并完成翻译算法的形式化证明.研究表明这种经过形式化的编译器能够生成与源代码行为一致的可信目标代码,同时生成的目标代码能够很好满足核能仪控系统的执行规范.

Trustworthy Translation of Synchronous Data-flow Language Input Structures

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.