计算机工程与设计
計算機工程與設計
계산궤공정여설계
COMPUTER ENGINEERING AND DESIGN
2014年
1期
137-143
,共7页
张玲波%甘元科%石刚%王生原%董渊%张智慧%王沿海
張玲波%甘元科%石剛%王生原%董淵%張智慧%王沿海
장령파%감원과%석강%왕생원%동연%장지혜%왕연해
同步数据流语言%可信编译器%形式化验证%时态消去%Coq
同步數據流語言%可信編譯器%形式化驗證%時態消去%Coq
동보수거류어언%가신편역기%형식화험증%시태소거%Coq
synchronous data-flow languages%trustworthy compiler%formal verification%temporal features eliminating%Coq
为解决实现同步数据流语言Lustre到串行命令式语言C语言可信编译器过程中碰到的时态运算翻译的困难,提出了将所有的时态运算翻译单独分层定义和证明的方法.在同步数据流语言的时态特性和C语言的循环特性分析的基础上,结合可信编译器实现框架上下层的语言结构,使用Coq证明工具,形式化的定义了两种中间语言的语法和语义,经过分析时态翻译过程特点,归纳定义了时态变量传递性质,实现了翻译工作严格的形式化验证,最终完成了时态消去翻译的等价性证明.
為解決實現同步數據流語言Lustre到串行命令式語言C語言可信編譯器過程中踫到的時態運算翻譯的睏難,提齣瞭將所有的時態運算翻譯單獨分層定義和證明的方法.在同步數據流語言的時態特性和C語言的循環特性分析的基礎上,結閤可信編譯器實現框架上下層的語言結構,使用Coq證明工具,形式化的定義瞭兩種中間語言的語法和語義,經過分析時態翻譯過程特點,歸納定義瞭時態變量傳遞性質,實現瞭翻譯工作嚴格的形式化驗證,最終完成瞭時態消去翻譯的等價性證明.
위해결실현동보수거류어언Lustre도천행명령식어언C어언가신편역기과정중팽도적시태운산번역적곤난,제출료장소유적시태운산번역단독분층정의화증명적방법.재동보수거류어언적시태특성화C어언적순배특성분석적기출상,결합가신편역기실현광가상하층적어언결구,사용Coq증명공구,형식화적정의료량충중간어언적어법화어의,경과분석시태번역과정특점,귀납정의료시태변량전체성질,실현료번역공작엄격적형식화험증,최종완성료시태소거번역적등개성증명.
