★北京廣利核系統(tǒng)工程有限公司 谷偉卿，張智慧，白濤，齊敏

可信編譯器中地址不相交的保持性證明

★北京廣利核系統(tǒng)工程有限公司 谷偉卿，張智慧，白濤，齊敏

同步數(shù)據(jù)流語言是一種廣泛應(yīng)用于核電及其他安全關(guān)鍵領(lǐng)域的語言，在同步數(shù)據(jù)流語言到順序執(zhí)行語言的翻譯轉(zhuǎn)換過程中，語義等價要保證賦值語句的左右值地址互不相交，這至關(guān)重要。本文使用形式化方法描述了翻譯過程中地址互不相交的性質(zhì)，并通過定理證明的方式對其進行了驗證。基于本方法的編譯器在某核電站的安全保護系統(tǒng)中得到了應(yīng)用。

同步數(shù)據(jù)流；定理證明；Coq；語義等價；地址不相交

1 引言

核電等安全關(guān)鍵領(lǐng)域中的軟硬件系統(tǒng)的可靠性越來越受到重視，這些系統(tǒng)的設(shè)計錯誤會帶來巨大的人身財產(chǎn)損失，所以對其功能設(shè)計的正確性驗證越來越受到重視。而傳統(tǒng)的編碼設(shè)計方式對工程設(shè)計人員帶來很大的困擾——開發(fā)效率低下、質(zhì)量沒有保證[1]，故算法組態(tài)軟件成為工程設(shè)計應(yīng)用的主流軟件，組態(tài)軟件的核心是編譯器，如果編譯器不可信，則很難保證系統(tǒng)所運行軟件的可信性。[2]

核電領(lǐng)域應(yīng)用甚廣的設(shè)計語言為Lustre——同步數(shù)據(jù)流語言，而我們的目標代碼為C語言。目前大多使用國際著名的SCADE工具[3]來將Lustre編譯成C代碼。SCADE工具雖然已獲得廣泛的應(yīng)用，但是其編譯器KCG尚未經(jīng)過嚴格的形式化驗證，它采用傳統(tǒng)的測試方法無法達到全覆蓋，在高可靠領(lǐng)域的應(yīng)用仍然存在考驗。

形式化驗證[4]根據(jù)某些形式規(guī)范或?qū)傩?，使用?shù)學(xué)的方法證明系統(tǒng)的正確性或非正確性，包括等價性驗證、模型檢測和定理證明[5]。其中定理證明用數(shù)學(xué)方法表達系統(tǒng)的規(guī)范和性質(zhì)，從邏輯上判斷設(shè)計的正確性，是最為嚴格和規(guī)范的方法，其結(jié)論的可信度也最高。定理證明系統(tǒng)基于已有的推理規(guī)則、公理和定理對要驗證的系統(tǒng)進行建模和推理，定理證明系統(tǒng)包含的理論庫越多，其建模和推理能力就越強。其中交互式定理證明工具Coq是在工業(yè)界和研究領(lǐng)域被廣泛應(yīng)用的。它提供大量的基礎(chǔ)性質(zhì)的形式化證明庫和證明策略。Coq有堅實的數(shù)學(xué)基礎(chǔ)，并能用同一語言描述程序、性質(zhì)和證明等形式化驗證的全過程。[6]

為提升核電系統(tǒng)設(shè)計的安全性，我們開發(fā)了一款經(jīng)過形式化驗證的自動化工具“Lustre編譯器”，將圖形化控制邏輯自動翻譯為符合IEC60880要求的C程序。編譯器是將高級語言轉(zhuǎn)換為較為低級的語言，將一個高級語言的操作進行拆分轉(zhuǎn)換為多步簡單的操作。由于同步數(shù)據(jù)流語言Lustre和Clight（C的一個子集）存在著巨大的差異，Lustre具有時鐘同步、數(shù)據(jù)流、并發(fā)及流數(shù)據(jù)對象等特征，而Clight則具有順序控制流特征，在翻譯轉(zhuǎn)換的過程中，會新產(chǎn)生中間變量或賦值結(jié)構(gòu)，我們在編譯器的前端檢查保證了源語言中變量和賦值語句左右值互不相交，如何將此性質(zhì)始終貫穿翻譯過程，保證在每一層的轉(zhuǎn)換之后地址互不相交至關(guān)重要。

本文其余部分組織如下：第一部分介紹相關(guān)工作。第二部分介紹Lustre編譯器的總體實現(xiàn)框架。第三部分介紹其中一次轉(zhuǎn)換前后的語法語義定義。第四部分介紹關(guān)鍵性質(zhì)——左右值不相交的保持性定義和證明。第五部分總結(jié)與展望。

2 相關(guān)工作

工業(yè)組態(tài)軟件SCADE的內(nèi)置編譯器為KCG，其采用嚴格的V&V過程管控實現(xiàn)了從Lustre到C的可靠翻譯，然而，這些方法并不能完全避免誤編譯的發(fā)生。[7]

國外的Compcert是一款經(jīng)過形式化驗證的，采用Coq來分步實現(xiàn)C的子集Clight到PowerPC匯編代碼的翻譯過程的C編譯器。[8]其采用Coq來分步實現(xiàn)C的子集Clight到匯編的翻譯過程，用Coq定義中間過程的語義，并用交互式定理證明器證明每個步驟在對應(yīng)的語義中執(zhí)行等價。相比普通的驗證技術(shù)，形式化驗證能在數(shù)學(xué)的層面對軟件的邏輯進行抽象和證明，因此具備更高的安全性。

目前，業(yè)界還沒有經(jīng)形式化驗證的方法來實現(xiàn)從Lustre到C的編譯器。由于同步數(shù)據(jù)流語言Lustre和Clight之間的巨大差異，為降低證明過程的復(fù)雜程度，我們將翻譯過程拆分成多個層次，保證每個層次語法和語義跨度不大，每個層完成特定的工作，比如時鐘歸一化、拓撲排序、消去高階運算等工作[7-13]已由合作者完成，本文的研究工作基于前面的翻譯證明工作展開。

3 Lustre編譯器實現(xiàn)框架

如圖1所示，為Lustre編譯器總體結(jié)構(gòu)。

圖1 Lustre編譯器總體結(jié)構(gòu)

轉(zhuǎn)換過程分為以下步驟：Lustre＊到Well-Typed Lustre＊（又稱LustreI）：前端的詞法、語法分析及靜態(tài)語義分析；LustreI到LustreS（PreProcessing）：翻譯全局常量、拆分表達式列表、翻譯類型、消去枚舉類型和化簡高階運算；L u s t r e S上的（TopoSorting）：拓撲排序；LustreS（排序后）到LustreQ（ClassifyConstVar）：將常量變量從變量列表分離；LustreQ到LustreT：高階操作符的語義變換；LustreT到LustreT1（TransHighorder）：將高階統(tǒng)一翻譯成for循環(huán)的形式；LustreT1到LustreT2（TransMainArgs）：主節(jié)點的輸入?yún)?shù)翻譯為結(jié)構(gòu)體；LustreT2到LustreT3（TransMainRets）：主節(jié)點的輸出參數(shù)翻譯為結(jié)構(gòu)體；LustreT3到LustreR（TransTypecmp）：生成數(shù)組和結(jié)構(gòu)體比較函數(shù)；LustreR到LustreN（Lr2ln）：對節(jié)點列表中的函數(shù)和節(jié)點的分類；LustreN到LustreF（TransTempo）：消去時態(tài)運算；LustreF到LustreE1（Lf2le）：生成節(jié)點對應(yīng)的結(jié)構(gòu)體類型；LustreE1到LustreE2（ClassifyRetsVar）：從變量列表中分離節(jié)點返回值；LustreE2到LustreE3（TransReset）：生成初始化函數(shù)列表；LustreE3到LustreE4（SimplEnv）：將所有節(jié)點的返回值翻譯成結(jié)構(gòu)體，并將調(diào)用節(jié)點的call運算翻譯成結(jié)構(gòu)體的一個實例的調(diào)用；LustreE4到LustreD（ClassifyArgsVar）：從變量列表中分離節(jié)點輸入?yún)?shù)；LustreD到Clight（ClightGen：CtempGen、TransCtemp）：到C的語法翻譯和證明，將memcpy內(nèi)存拷貝語義翻譯為內(nèi)存拷貝函數(shù)。

本文所做的工作主要是對翻譯過程中左右值地址不相交性質(zhì)的保持性進行形式化定義和證明。

4 語法和語義定義

在翻譯過程中左右值地址不相交性質(zhì)貫穿始終，對于普通類型的賦值運算可直接賦值，而對復(fù)雜類型，如結(jié)構(gòu)體和數(shù)組類型的賦值需要滿足左右值地址不相交的性質(zhì)，因為復(fù)雜類型的賦值需要翻譯到memcpy，memcpy的運算需要左右值地址范圍不相交。另外結(jié)構(gòu)體和數(shù)組類型的輸入?yún)?shù)在Clight中需要翻譯為指針的形式，返回值也需要翻譯為指針，這就要求call調(diào)用的左右值地址范圍也不能相交。

在以上翻譯過程中：

（1）將高階統(tǒng)一翻譯成for循環(huán)形式的過程（TransHighorder）；

（2）將所有節(jié)點的返回值翻譯成結(jié)構(gòu)體，并將調(diào)用節(jié)點的call運算翻譯成結(jié)構(gòu)體的一個實例調(diào)用過程（SimplEnv）；

（3）到C的語法翻譯和證明，將memcpy內(nèi)存拷貝語義翻譯為內(nèi)存拷貝函數(shù)過程（CtempGen）；

這三個步驟包含了生成結(jié)構(gòu)體、數(shù)組和call調(diào)用的過程，本文針對SimplEnv的翻譯轉(zhuǎn)換過程進行左右值地址不相交證明進行舉例說明。

4.1 語法

雖然在翻譯過程中分成多層，但是有些中間語言與其他語言的語法相同或相似，差別很少。為了簡化定義，我們將中間語言公用的抽象語法定義在公共語法文件中。有program、node、stmt和sexp四個層次，分別表示程序、函數(shù)節(jié)點、語句和表達式。

其中program表示整個程序，由類型定義列表、常量定義列表、node列表和主節(jié)點id組成。程序執(zhí)行會通過主node的id定位并執(zhí)行主node。

node為Lustre的程序執(zhí)行節(jié)點，相當于C程序的函數(shù)，由節(jié)點類型、輸入?yún)?shù)、返回值、局部變量、語句列表五部分組成。

stmt為Lustre程序的語句，由普通賦值語句、函數(shù)調(diào)用語句、for循環(huán)語句、數(shù)組和結(jié)構(gòu)體賦值語句和跟時序相關(guān)的語句，LustreE3、LustreE4層的語法與LustreF層的定義上相同，它們的stmt已消去了時態(tài)運算，具體定義如下：

stmt ：：= lh = sexp // 賦值語句。為方便，lh等同于 (id,)，下同。

| (oid, lhs) = call (calldef, sexp＊) // call 語句。

| Sfor (eqf, sexp, eqf, stmt) // 高階執(zhí)行語句。

| Sifs (sexp, stmt, stmt) // 條件語句

| Scase (sexp, sexp, (＜patn,sexp＞)＊) // case語句

| Sseq (stmt, stmt) // 序列語句。

| skip // 空語句。

sexp為Lustre程序的表達式，包括常量表達式、普通變量id、常量id、結(jié)構(gòu)體變量id、輸入變量id、數(shù)組子元素求值、結(jié)構(gòu)體子元素求值、類型轉(zhuǎn)化表達式、一元表達式和二元表達式。

4.2 語義環(huán)境

語義環(huán)境由全局和局部環(huán)境組成，對于node，由于要考慮時態(tài)特征，局部環(huán)境env的定義比普通串行語言的情形復(fù)雜很多：

Inductive env： Type ：= mkenv {

le： locenv;

sube： PTree.t (list env)

}.

其中，le和傳統(tǒng)語言語義的局部環(huán)境類似，刻畫了node在某個時鐘周期的局部環(huán)境。locenv的定義：

Definition locenv：= PTree.t (mvl＊type).

sube維護了本節(jié)點實例與子節(jié)點實例中局部變量、輸入和輸出變量的歷史取值。其中，類型PTree.t取 CompCert C中的定義，相當于一個（帶索引的）容器類型的數(shù)據(jù)結(jié)構(gòu)，方便增、刪、改以及檢索。

全局常量對應(yīng)的環(huán)境gc定義為

gc： PTree.t (mvl＊type)或gc： locenv

我們用gc表示全局常量環(huán)境，當前局部環(huán)境中，用te表示普通變量環(huán)境，用se表示自定義變量環(huán)境，用ta表示輸入變量環(huán)境，用eh表示本地局部環(huán)境變量列表。

翻譯前的語義環(huán)境為：

gc, eh, te├ lvalue_list_norepet (lhs) // lhs中所有id互不相交

gc, eh, te├ assign_list_disjoint (lhs, args) // args的類型列表與fd定義中的參數(shù)類型列表相匹配

翻譯后的語義環(huán)境為：

gc, ta, te, e├ lvalue_list_norepet (lhs) // lhs中所有id互不相交

gc, ta, te, e├ assign_list_disjoint (lhs, args) // args的類型列表與fd定義中的參數(shù)類型列表相匹配

翻譯前后將原有的樹形環(huán)境env簡化為簡單環(huán)境locenv。

5 地址不相交的保持性定義和證明

第3節(jié)描述的翻譯過程中，每兩層之間的翻譯都要保證語義的等價性，其中高階消去[6]、可信排序[11]和消去時態(tài)運算[12]的證明思想已在其他文章中介紹過，下面介紹左右值地址不相交的保持性定義和證明。

結(jié)構(gòu)體和數(shù)組類型賦值運算要翻譯為Clight中memcpy運算。在memcpy中需要滿足以下對地址的限制：要么源地址和目的地址的指針不同；要么源地址和目的地址的偏移量相同；要么源地址范圍和目的地址范圍不相交。而Lustre的值中不存在指針，在證明這一步的證明之前也沒有對Lustre賦值運算左右值的地址進行限制，所以需要定義Lustre中賦值的左右值地址不相交。而且在call運算的證明中也需要類似的定義，call運算中數(shù)組和結(jié)構(gòu)體類型的輸入?yún)?shù)會被翻譯成指針，輸出參數(shù)都會被翻譯成指針。同樣需要提供數(shù)組和結(jié)構(gòu)體類型的輸入?yún)?shù)和call的左值地址不相交；call的左值列表的地址不重復(fù)。

5.1 地址不相交的定義

在翻譯過程中，我們要保證語句左值和等式右值的地址范圍不相交，才能保證翻譯的正確性，其中語句的左右值不相交包括三種情況：

（1）數(shù)組和結(jié)構(gòu)體賦值語句的左右值地址不能相交

因為數(shù)組和結(jié)構(gòu)體賦值不能直接通過賦值符號來賦值，需要借助memcpy來完成，而通過memcpy的賦值操作需要滿足上述定義中的性質(zhì)。

（2）Call運算左值不相交定義

Call運算會生成新的變量作為左值，我們要保證新生成的變量id和已有的左值列表地址互不相交。

（3）Call運算左值和輸入?yún)?shù)地址不相交

Call運算新生成的變量id與原左值列表構(gòu)成的新左值列表還必須與輸入?yún)?shù)列表地址不相交。

LsemF中地址值不相交的定義：

（1）數(shù)組和結(jié)構(gòu)體賦值中不相交的形式化定義

assign_disjoint te e a1 a2 ：=

|- (普通變量賦值語句：chunk, a2的值訪問方式為值訪問方式=＞a1與a2地址不相交)

/ (數(shù)組結(jié)構(gòu)體賦值語句：id1 id2 o1 o2 k1 k2, a2的值訪問方式為指針或memcpy，a1的類型k1為局部變量或結(jié)構(gòu)體變量，(id1 ＜＞ id2 / Int.unsigned o1 + sizeof (typeof_s a1) ＜= Int.unsigned o2 /

Int.unsigned o2 + sizeof (typeof_s a2) ＜= Int. unsigned o1)%Z =＞

assign_disjoint te e a1 a2=＞l1與l2地址不相交）

其中te為普通變量環(huán)境，e為局部歷史環(huán)境，a1、a2分別表示賦值語句的左值和右值，chunk表示數(shù)據(jù)塊，id1為a1的左值id，o1為id1的起始地址，k1為a1的變量類型，id2為a2的左值id，o2為id2的起始地址，k2為a2的變量類型。當k1為局部變量或結(jié)構(gòu)體變量時，若id1不等于id2，或o1+a1的長度＜o2，或o2+a2的長度＜o1，則在普通變量環(huán)境te和局部歷史環(huán)境e下，a1和a2左值地址不相交。

（2）Call運算左值不相交的形式化定義

lval ue_disjoint te e a1 a2 ：=

eval_lvalue te e a1 id1 o1 k1 -＞

eval_lvalue te e a2 id2 o2 k2 -＞

k1 = Lid / k1 = Sid -＞

k2 = Lid / k2 = Sid -＞

(id1 ＜＞ id2 / Int.unsigned o1 + sizeof (typeof_ s a1) ＜= Int.unsigned o2 /

Int.unsigned o2 + sizeof (typeof_s a2) ＜= Int. unsigned o1)%Z -＞

lvalue_disjoint te e a1 a2.

其中te表示普通變量環(huán)境，e表示局部歷史環(huán)境，a1、a2分別表示不同的call運算表達式，id1為a1的左值id，o1為id1的起始地址，k1為a1的變量類型，id2為a2的左值id，o2為id2的起始地址，k2為a2的變量類型，當k1、k2為局部變量或結(jié)構(gòu)體變量時，若id1不等于id2，或o1+a1的長度＜o2，或o2+a2的長度＜o1，則在普通變量環(huán)境te和局部歷史環(huán)境e下，a1和a2左值地址不相交。

其次，列表形式的形式化定義如下：

Definition lvalue_disjoints(te e： locenv)(a：sexp)(l： list sexp)： Prop ：=a1, In a1 l =＞ lvalue_ disjoint te e a a1.

（3）Call運算左值和輸入?yún)?shù)不相交的形式化定義

Definition assign_list_disjoint(te e： locenv)(l1 l2： list sexp)： Prop ：=

a1 a2, In a1 l1 -＞ In a2 l2 -＞ assign_disjoint te e a1 a2.

對所有a1、a2，a1屬于表l1，a2屬于表l2，則在普通變量環(huán)境te和局部歷史環(huán)境e下，a1、a2不相交。

5.2 左右值不相交的保持性證明

左右值不相交的保持性證明分為以下三種，主要是針對數(shù)組和結(jié)構(gòu)體類型的左右值變量的地址范圍不相交的性質(zhì)的保持性證明。

（1）等式賦值左右值不相交的保持性定理

Lemma assign_disjoint_env_match：

assign_disjoint gc te eh a1 a2 -＞

env_match nd (mkenv eh se) e2 -＞

Z.max 1 (sizeof_struct (nd_fld (snd nd)) 0) ＜= Int.max_unsigned -＞

eval_sexp gc te eh a2 v -＞

locenv_getmvl gc te eh a1 v1 -＞

te ? OUTSTRUCT = None -＞

gc ? OUTSTRUCT = None -＞

assign_disjoint gc te e2 (trans_expr (makevar (snd nd)) a1) (trans_expr (makevar (snd nd)) a2).

其中，assign_disjoint表示等式左右值不相交，a1表示翻譯前的左值，a2表示翻譯前的右值。

對所有的全局常量環(huán)境gc、普通變量環(huán)境te、本地局部環(huán)境變量列表eh、自定義變量環(huán)境se、局部歷史環(huán)境e2、等式左值a1等式右值a2、局部環(huán)境nd，變量v、v1，若滿足①在gc、te、eh下a1、a2左右值不相交，②nd和eh與se構(gòu)成的環(huán)境相匹配，③nd的結(jié)構(gòu)體變量大小小于最大無符號數(shù)，④表達式a2在gc、te下執(zhí)行結(jié)果為v，⑤在環(huán)境gc、te、eh下，a2執(zhí)行結(jié)果為v，⑥在gc、te、eh下a1存儲方式為v1，⑦在te下，存在輸出結(jié)構(gòu)體為空，⑧在gc下，存在輸出結(jié)構(gòu)體為空，則有在gc、te、e2下，a1和a2經(jīng)表達式翻譯后的id列表不相交。

通過證明表達式執(zhí)行等價、表達式左值范圍為靜態(tài)、結(jié)構(gòu)體中變量的域互不重疊便可得證。

（2）call左值列表不重復(fù)的保持性定理

Lemma lvalue_list_norepet_env_match：

lvalue_list_norepet gc te eh l -＞

env_match nd (mkenv eh se) e2 -＞

Z.max 1 (sizeof_struct (nd_fld (snd nd)) 0) ＜= Int.max_unsigned -＞

locenv_getmvls gc te eh l vl -＞

te ? OUTSTRUCT = None -＞

gc ? OUTSTRUCT = None -＞

lvalue_list_norepet gc te e2 (trans_exprs (makevar (snd nd)) l).

該定理表示若①對所有的全局常量環(huán)境gc、普通變量環(huán)境te、本地局部環(huán)境變量列表eh、表達式列表l，若滿足左值列表不重復(fù)，②對所有的自定義變量se、局部歷史環(huán)境e2、局部環(huán)境nd和變量vl，若滿足nd和eh與se構(gòu)成的環(huán)境匹配，③ nd的結(jié)構(gòu)體變量大小小于最大無符號數(shù)，④在環(huán)境gc、te、eh下，1的存儲方式為v1，⑤在te下，存在輸出結(jié)構(gòu)體為空，⑥在gc下，存在輸出結(jié)構(gòu)體為空，則有在gc、te、e2下，經(jīng)表達式翻譯后的l的左值列表不重復(fù)。

通過展開表達式轉(zhuǎn)換的定義，證明左值不相交的保持性便可得證。

（3）call左值列表和右值表達式不相交的保持性定理

Lemma assign_list_disjoint_env_match：

assign_list_disjoint gc te eh l args -＞

env_match nd (mkenv eh se) e2 -＞

Z.max 1 (sizeof_struct (nd_fld (snd nd)) 0) ＜= Int.max_unsigned -＞

te ? OUTSTRUCT = None -＞

gc ? OUTSTRUCT = None -＞

eval_sexps gc te eh args vargs -＞

locenv_getmvls gc te eh l vl -＞

assign_list_disjoint gc te e2 (trans_exprs (makevar (snd nd)) l) (trans_exprs (makevar (snd nd)) args).

該定理表示若①對所有的全局常量環(huán)境gc、普通變量環(huán)境te、本地局部環(huán)境變量列表eh、表達式列表l，輸入?yún)?shù)列表args，若滿足在gc、te、eh下l與args列表地址不相交，②對所有的自定義變量se、局部歷史環(huán)境e2、局部環(huán)境nd、輸入?yún)?shù)列表args和變量vl，若滿足nd和eh與se構(gòu)成的環(huán)境匹配，③nd的結(jié)構(gòu)體變量大小小于最大無符號數(shù)，④在te下，存在輸出結(jié)構(gòu)體為空，⑤在gc下，存在輸出結(jié)構(gòu)體為空， ⑥在環(huán)境gc、te、eh下，args的執(zhí)行語義結(jié)果為vargs，⑦在環(huán)境gc、te、eh下，1的存儲方式為v1，則有在gc、te、e2下，經(jīng)表達式翻譯后的l與經(jīng)表達式翻譯后的args的地址不重復(fù)。

該定理可先證明非列表的形式成立，并通過Coq中的list函數(shù)庫的性質(zhì)得證。

證明過程通過前提列表中的定義展開，并結(jié)合Coq的自動推理能力得以證明。證明了以上三個情況的地址不相交，即包含了Lustre到C轉(zhuǎn)換中賦值語句變化部分的全部證明。

6 總結(jié)與展望

核電系統(tǒng)的開發(fā)流程必須滿足NUREG/CR-6463 1996國際標準。Lustre編譯器是廣利核系統(tǒng)工程有限公司提供的滿足NUREG/CR-6463 1996國際標準的，同時遵循IEC 60880-2006、MISRA-C：2004和ISO/ IEC 9899：1990編碼規(guī)范的代碼產(chǎn)生器。由于Lustre編譯器本身滿足這一標準并保證了代碼的正確性，它不僅大大節(jié)省了編碼工作，而且完全免去了代碼的單元測試，很大程度地節(jié)省了驗證工作和驗證時間。

本文基于高階邏輯定理證明器Coq，實現(xiàn)了Lustre到C的可信翻譯及證明，并列舉了左右值地址不相交性質(zhì)的證明，本文所描述的Lustre編譯器已經(jīng)過大量的測試及驗證確認工作，已經(jīng)過驗證并獲得國際驗證機構(gòu)ISTec的認可，并獲頒國內(nèi)首張第三方驗證與確認（IV&V）證書，且Lustre編譯器已應(yīng)用在核電系統(tǒng)神經(jīng)中樞的某系統(tǒng)中。地址不相交保持性證明在編譯器可信翻譯中的應(yīng)用為以后的相關(guān)轉(zhuǎn)換工具的可信研發(fā)奠定了堅實的基礎(chǔ)。

[1] 高玉娜. 基于SCADE的嵌入式軟件開發(fā)方法研究[J]. 電子設(shè)計工程, 2015, 21： 103 - 105.

[2] 何炎祥, 吳偉, 劉陶, 等. 可信編譯理論及其核心實現(xiàn)技術(shù)：研究綜述[J]. 計算機科學(xué)與探索, 2011, 05( 1 ) ： 1 - 22.

[3] Berry G. Synchronous design and verification of critical embedded systems using SCADE and Esterel[C]. Formal methods for industrial critical systems, 2007： 2 - 2.

[4] Clarke E M, Wing J M. Formal methods： state of the art and future directions[J]. Acm Computing Surveys, 1996, 28 ( 4 )： 626 - 643.

[5] 韓俊剛, 杜慧敏. 數(shù)字硬件的形式化驗證[M]. 北京：北京大學(xué)出版社, 2001, 12.

[6] Coqdevelopmentteam B. The coq proof assistant reference manual - version 8.0[C]. INRIA, INRIA Rocquencourt. 2010.

[7] 劉洋, 甘元科, 王生原, 等. 同步數(shù)據(jù)流語言高階運算消去的可信翻譯[J]. 軟件學(xué)報, 2015, 26 ( 2 ) ： 332 - 347.

[8] Yang X, Chen Y, Eide E, et al. Finding and understanding bugs in C compilers.[J]. Acm Sigplan Notices, 2015, 46 ( 6 ) ：283 - 294.

[9] 張智慧, 齊敏, 冀建偉, 等. 核安全級控制算法描述語言的可信編譯研究[C]. 2011.

[10] 石剛, 王生原, 董淵, 等. 同步數(shù)據(jù)流語言可信編譯器的構(gòu)造[J]. 軟件學(xué)報, 2014, 25 ( 2 ) ： 341 - 356.

[11] 王蕾, 石剛, 董淵, 等. 一個C語言安全子集的可信編譯器[J]. 計算機科學(xué), 2013, 40 ( 9 ) ： 30 - 34.

[12] 甘元科, 張玲波, 石剛, 等. 同步數(shù)據(jù)流程序的可信排序[J]. 計算機應(yīng)用與軟件, 2014 ( 5 ) ： 1 - 5.

[13] 張玲波, 甘元科, 石剛, 等. 同步數(shù)據(jù)流語言時態(tài)消去的可信翻譯[J]. 計算機工程與設(shè)計, 2014, 35 ( 1 ) ： 137 - 143.

Proof of the Preservation Property of Address Disjointness in Trustworthy Complier

Synchronous data-flow language is widely used in safety critical control system such as nuclear power systems. In the process of translation from synchronous data-flow language to order execution language, it is essential to guarantee the address disjointness between left and right values in assignment statement in semantic equivalence. In this paper, we formalized the property of address disjointness during the translation process, and verified the property via theorem proving. Compiler based on this method has been applied in safety protection system at some nuclear power plant.

Synchronous Data-Flow; Theorem Proving; Coq; Semantic Equivalence; Address Disjointness

谷偉卿（1987-），女，河北人，工程師，碩士，現(xiàn)就職于北京廣利核系統(tǒng)工程有限公司，主要研究方向為編譯系統(tǒng)，形式化驗證。

張智慧（1982-），男，內(nèi)蒙古人，工程師，碩士，現(xiàn)就職于北京廣利核系統(tǒng)工程有限公司，主要研究方向為安全級算法組態(tài)軟件、編譯系統(tǒng)、基于語言的可信軟件。

白 濤（1973-），男，河北人，高級工程師，碩士，現(xiàn)任北京廣利核系統(tǒng)工程有限公司總工程師，主要研究方向為核電站數(shù)字化儀控。

齊 敏（1974-），女，河南人，工程師，碩士，現(xiàn)就職于北京廣利核系統(tǒng)工程有限公司，主要研究方向為核電站反應(yīng)堆保護系統(tǒng)安全級DCS平臺設(shè)計和開發(fā)。