摘要：同步數(shù)據(jù)流語言(如Lustre、Signal)在航空、高鐵、核電等安全關(guān)鍵領(lǐng)域得到廣泛應(yīng)用。例如,適合這些領(lǐng)域?qū)崟r控制系統(tǒng)建模和開發(fā)的Scade工具就是基于一種類Lustre語言。這類語言相關(guān)開發(fā)工具,特別是編譯器的安全性問題也自然受到高度關(guān)注。近年來,基于形式化驗(yàn)證實(shí)現(xiàn)可信編譯器構(gòu)造成為程序設(shè)計(jì)語言領(lǐng)域的研究焦點(diǎn)之一,也取得了矚目的成果,如CompCert項(xiàng)目實(shí)現(xiàn)了產(chǎn)品級的可信C編譯器。同樣,人們也采用這種方法開展了同步數(shù)據(jù)流語言可信編譯器的研發(fā)工作。主要關(guān)注從事這一工作的兩個長線項(xiàng)目,二者均研發(fā)面向基于Lustre的同步數(shù)據(jù)流語言編譯器,分別以Vélus和L2C代稱。對Vélus和L2C從多個重要的角度進(jìn)行較為深入的分析與比較。