Formal verification of synchronous data-flow program transformations toward certified compilers  

作　　者：Van Chan NGO Jean-Pierre TALPIN Thierry GAUTIER Paul Le GUERNIC Loic BESNARD 

机构地区：[1]INRIA Rennes-Bretagne Atlantique, Rennes 35042, France [2]IRISA/CNRS, Rennes 35042, France

出　　处：《Frontiers of Computer Science》2013年第5期598-616,共19页中国计算机科学前沿（英文版）

摘　　要：Translation validation was invented in the 90＇s by Pnueli et al. as a technique to formally verify the correctness of code generators. Rather than certifying the code generator or exhaustively qualifying it, translation validators attempt to verify that program transformations preserve semantics. In this work, we adopt this approach to formally verify that the clock semantics and data dependence are preserved during the compilation of the Signal compiler. Translation valida- tion is implemented for every compilation phase from the initial phase until the latest phase where the executable code is generated, by proving the transformation in each phase of the compiler preserves the semantics. We represent the clock semantics, the data dependence of a program and its trans- formed counterpart as first-order formulas which are called clock models and synchronous dependence graphs （SDGs）, respectively. We then introduce clock refinement and depen- dence refinement relations which express the preservations of clock semantics and dependence, as a relation on clock mod- els and SDGs, respectively. Our validator does not require any instrumentation or modification of the compiler, nor any rewriting of the source program.Translation validation was invented in the 90＇s by Pnueli et al. as a technique to formally verify the correctness of code generators. Rather than certifying the code generator or exhaustively qualifying it, translation validators attempt to verify that program transformations preserve semantics. In this work, we adopt this approach to formally verify that the clock semantics and data dependence are preserved during the compilation of the Signal compiler. Translation valida- tion is implemented for every compilation phase from the initial phase until the latest phase where the executable code is generated, by proving the transformation in each phase of the compiler preserves the semantics. We represent the clock semantics, the data dependence of a program and its trans- formed counterpart as first-order formulas which are called clock models and synchronous dependence graphs （SDGs）, respectively. We then introduce clock refinement and depen- dence refinement relations which express the preservations of clock semantics and dependence, as a relation on clock mod- els and SDGs, respectively. Our validator does not require any instrumentation or modification of the compiler, nor any rewriting of the source program.

关 键 词：formal verification translation validation certi-fied compiler multi-clocked synchronous programs embed-ded systems. 

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