10.3969/j.issn.1000-7024.2014.01.026
同步数据流语言时态消去的可信翻译
为解决实现同步数据流语言Lustre到串行命令式语言C语言可信编译器过程中碰到的时态运算翻译的困难,提出了将所有的时态运算翻译单独分层定义和证明的方法.在同步数据流语言的时态特性和C语言的循环特性分析的基础上,结合可信编译器实现框架上下层的语言结构,使用Coq证明工具,形式化的定义了两种中间语言的语法和语义,经过分析时态翻译过程特点,归纳定义了时态变量传递性质,实现了翻译工作严格的形式化验证,最终完成了时态消去翻译的等价性证明.
同步数据流语言、可信编译器、形式化验证、时态消去、Coq
35
TP314(计算技术、计算机技术)
国家自然科学基金项目61170051、61272086、90818019;核高基重大专项经费基金项目2012ZX01039-004
2014-03-12(万方平台首次上网日期,不代表论文的发表时间)
共7页
137-143