核安全級(jí)DCS系統(tǒng)模型驅(qū)動(dòng)可信代碼自動(dòng)生成方法

蘭 林，馬 權(quán)，侯榮彬，李 勇，楊 斌，榮健兵，吳延群

（1.中國核動(dòng)力研究設(shè)計(jì)院 核反應(yīng)堆系統(tǒng)設(shè)計(jì)技術(shù)重點(diǎn)實(shí)驗(yàn)室，成都 610213；2.哈爾濱工程大學(xué)，哈爾濱 150000）

0 引言

核安全級(jí)儀控DCS系統(tǒng)（Nuclear Advanced Safety Platform Instrument Control System，簡(jiǎn)稱NASPIC）對(duì)于核電廠的安全、穩(wěn)定運(yùn)行具有重要的作用，傳感器把從核電廠現(xiàn)場(chǎng)采集來的數(shù)據(jù)上傳至控制器中，經(jīng)控制算法軟件處理后輸出，從而控制核電廠現(xiàn)場(chǎng)執(zhí)行器的安全動(dòng)作。因此，控制算法軟件的安全性、可信性直接關(guān)系著核電廠運(yùn)行的安全性、穩(wěn)定性。傳統(tǒng)的控制算法編寫多采用手工編碼的方式，此方法對(duì)于儀控工程師的編碼能力要求較高，由于在編碼過程中容易引入錯(cuò)誤，因而需要對(duì)編寫的代碼進(jìn)行大量的單元測(cè)試、集成調(diào)試以保證代碼的正確性和安全性，占用了儀控工程師大量的時(shí)間和精力。為解決當(dāng)前手工編碼存在的問題，高安全性的應(yīng)用程序開發(fā)環(huán)境（Safety-Critical Application Development Environment，簡(jiǎn)稱SCADE）[1,2]提出了模型驅(qū)動(dòng)代碼自動(dòng)生成的一種全新的控制算法軟件設(shè)計(jì)的思路。SCADE是法國Esterel Technologies公司研制的比較成熟的高安全性應(yīng)用程序開發(fā)環(huán)境，主要用于開發(fā)滿足DO-178B標(biāo)準(zhǔn)的嵌入式軟件[3,4]，廣泛用于嵌入式安全攸關(guān)領(lǐng)域，如核電、軌道交通、國防等。目前，國內(nèi)核電DCS系統(tǒng)控制領(lǐng)域還沒有一個(gè)類似于SCADE的高安全程序開發(fā)環(huán)境，為改變高安全性的控制算法軟件開發(fā)環(huán)境完全依賴進(jìn)口的局面，結(jié)合核電廠安全級(jí)DCS系統(tǒng)控制需求，研制一種適用于核電廠安全級(jí)DCS系統(tǒng)算法軟件設(shè)計(jì)的、由模型驅(qū)動(dòng)的代碼自動(dòng)生成的綜合性建模環(huán)境。基于數(shù)據(jù)流圖和有限狀態(tài)機(jī)方法，開發(fā)了圖形化建模軟件，用于儀控工程師通過拖拽功能圖符塊編寫控制算法；XML文件信息提取軟件，用于把圖符塊對(duì)應(yīng)的XML文件轉(zhuǎn)化為L(zhǎng)ustre程序的形式；基于形式化驗(yàn)證技術(shù)，開發(fā)了可信代碼生成軟件，用于把Lustre程序轉(zhuǎn)化為安全、正確的C程序。最后，將這些軟件集成在一起使用，為核安全級(jí)DCS系統(tǒng)控制算法開發(fā)提供了一個(gè)由圖形化算法模型驅(qū)動(dòng)代碼自動(dòng)生成的解決方案。本文將針對(duì)圖形化建模軟件、XML文件信息提取方法和可信代碼生成軟件進(jìn)行詳細(xì)介紹。

1 圖形化建模軟件

圖形化建模是核安全級(jí)DCS系統(tǒng)控制算法開發(fā)過程中的重要環(huán)節(jié)，為核安全級(jí)DCS系統(tǒng)模型驅(qū)動(dòng)代碼自動(dòng)生成方法提供算法模型。在充分研究核電廠DCS系統(tǒng)對(duì)象物理特性、結(jié)構(gòu)特性、行為特性的基礎(chǔ)上，將NASPIC平臺(tái)系統(tǒng)的設(shè)備（包括板卡、機(jī)箱、機(jī)柜）、變量（包括模擬量、數(shù)字量類型等）、核電廠控制算法功能塊抽象為對(duì)應(yīng)的圖形化的設(shè)備模型、變量模型和算法模型，它們分別用于創(chuàng)建虛擬硬件設(shè)備及其連接關(guān)系、通道綁定與通道配置、創(chuàng)建輸入信號(hào)的運(yùn)算邏輯。如圖1所示，在圖形化建模界面軟件中，通過拖拽模型來創(chuàng)建系統(tǒng)控制算法。以下將分別介紹圖形化設(shè)備建模、變量建模和算法建模。

1.1 設(shè)備建模

圖1 圖形建模結(jié)構(gòu)示意圖Fig.1 Schematic diagram of graphical modeling structure

設(shè)備建模主要負(fù)責(zé)創(chuàng)建硬件設(shè)備模型和硬件設(shè)備之間的映射關(guān)系，首先根據(jù)核電廠實(shí)際工程控制需要，創(chuàng)建機(jī)柜模型、機(jī)箱模型、板卡模型以及通道模型，為進(jìn)行變量建模提供設(shè)備通道以及設(shè)備間的連接關(guān)系。設(shè)備建模提供了豐富的設(shè)備庫，并根據(jù)當(dāng)前建模所處階段，自動(dòng)增減設(shè)備庫中可選硬件設(shè)備，這一設(shè)計(jì)提升了設(shè)備建模過程的便利性，同時(shí)也降低了誤操作的概率。設(shè)備建模包括：①機(jī)柜建模。根據(jù)機(jī)柜類型、機(jī)柜容量等信息創(chuàng)建機(jī)柜模型，用于搭建機(jī)柜集群，初步建立控制系統(tǒng)框架；②機(jī)箱建模。由機(jī)柜配置信息創(chuàng)建機(jī)箱模型，機(jī)箱模型作為板卡模型的容器，主要是將執(zhí)行控制功能的板卡進(jìn)行邏輯組合；③板卡建模。板卡是實(shí)現(xiàn)具體控制功能的硬件集成電路板卡，包括DO、AO、AI、DI等10余種類型，儀控工程師可根據(jù)系統(tǒng)數(shù)據(jù)采集任務(wù)需求來創(chuàng)建板卡模型，根據(jù)制定的建模規(guī)則在機(jī)箱相應(yīng)的槽號(hào)插入板卡，可滿足多樣化和定制化的系統(tǒng)控制功能需求；④通道建模。通道在建模過程中可以通常和變量建模同步進(jìn)行，底層設(shè)備的參數(shù)信息通過通道的變量模型信息展示和傳輸，同時(shí)通道用于建立兩個(gè)或多個(gè)機(jī)箱之間的通信。

1.2 變量建模

變量建模主要用于創(chuàng)建物理通道與虛擬通道的映射關(guān)系，配置通道屬性（如數(shù)據(jù)采集量程、通道安全行為、預(yù)設(shè)值等），創(chuàng)建設(shè)備間通信的網(wǎng)絡(luò)參數(shù)配置等。變量建模的前提是存在設(shè)備模型，即虛擬通道必須建立在物理通道之上，同時(shí)變量模型為后續(xù)的算法建模提供變量信息，用于關(guān)聯(lián)算法功能圖符塊。變量模型是整個(gè)控制系統(tǒng)的基本組成單元，具有屬性繁多、規(guī)則復(fù)雜等特點(diǎn)，其正確性直接影響控制系統(tǒng)的輸入、輸出的正確性。變量模型研究的關(guān)鍵在于建立覆蓋變量所有屬性、所有行為規(guī)則的模型檢查機(jī)制，包括檢查預(yù)期的特定屬性是否存在；預(yù)期的屬性是否已填值；預(yù)期的屬性值是否落在條件范圍內(nèi)；網(wǎng)絡(luò)路由關(guān)系是否正確等，保證了建模的正確性和安全性。

1.3 算法建模

算法建模是核安全DCS系統(tǒng)控制算法設(shè)計(jì)的核心，是基于形式化驗(yàn)證的可信代碼生成的基礎(chǔ)。算法建模基于數(shù)據(jù)流圖和有限狀態(tài)機(jī)方法，分別對(duì)連續(xù)系統(tǒng)和離散系統(tǒng)進(jìn)行建模，模型具有嚴(yán)格的數(shù)學(xué)語義，保證了算法模型的設(shè)計(jì)與需求具有一致性。其中，數(shù)據(jù)流圖用于連續(xù)系統(tǒng)建模，描述了數(shù)據(jù)的處理過程、反應(yīng)時(shí)序及因果關(guān)系，通過儀控工程師定義的輸入變量接收核電廠現(xiàn)場(chǎng)采集的控制信號(hào)，經(jīng)過圖形化控制算法模型處理后，再輸出給DO模塊，控制核電廠現(xiàn)場(chǎng)執(zhí)行器的安全動(dòng)作。數(shù)據(jù)流圖建模中最基本的功能單元是節(jié)點(diǎn)，類似于C語言中的函數(shù)，并且提供算術(shù)運(yùn)算、邏輯運(yùn)算、比較運(yùn)算、時(shí)間運(yùn)算等基本運(yùn)算符，利用這些預(yù)定義的運(yùn)算符及自定義的節(jié)點(diǎn)，可繼續(xù)構(gòu)建新的、更復(fù)雜的節(jié)點(diǎn)，以完成更復(fù)雜的功能。這兩種建模方式既可單獨(dú)使用也可結(jié)合使用，滿足了核電廠DCS系統(tǒng)多樣化的控制需求，大大提高了設(shè)計(jì)效率。

2 XML文件數(shù)據(jù)提取

在圖形化建模軟件中，儀控工程師根據(jù)工程實(shí)際控制需求進(jìn)行圖形化控制算法建模后，源程序以XML格式文件存在。工程的XML文件包含當(dāng)前工程中用到的組合邏輯塊XML文件、工程配置XML文件、預(yù)定義XML文件以及算法塊XML文件。為了簡(jiǎn)化可信代碼生成器的構(gòu)造和證明，在把圖形化控制算法模型轉(zhuǎn)化為可信代碼之前，用一種中間語言來表示圖形化算法模型，即把XML中的控制算法信息提取成Lustre程序。XML格式文件中的信息結(jié)構(gòu)如圖2所示，包括以下幾部分：①工程信息描述區(qū)域，主要存儲(chǔ)工程的基本信息；②輸入?yún)?shù)、輸出參數(shù)、局部變量描述區(qū)域，主要存儲(chǔ)從現(xiàn)場(chǎng)采集到的待處理的數(shù)據(jù)、局部變量數(shù)據(jù)以及輸出的結(jié)果；③控制算法描述區(qū)域，主要存儲(chǔ)處理輸入數(shù)據(jù)的算法；④圖形化數(shù)據(jù)區(qū)，主要存儲(chǔ)圖形化控制算法軟件的算法圖符塊的幾何信息。

Lustre是一種同步數(shù)據(jù)流語言[5]，一個(gè)Lustre程序是由多個(gè)node構(gòu)成，node相當(dāng)于C語言中的一個(gè)函數(shù)，不同點(diǎn)在于其輸入?yún)?shù)和輸出參數(shù)是一個(gè)流（Stream），源源不斷地處理從控制現(xiàn)場(chǎng)采集到的數(shù)據(jù)，node的基本結(jié)構(gòu)如圖3所示，其中node、returns、var、let、tel為L(zhǎng)ustre程序的關(guān)鍵字。在XML文件數(shù)據(jù)提取過程中，XML文件數(shù)據(jù)提取軟件首先加載工程配置XML文件，獲取到所有的組合邏輯塊XML文件、預(yù)定義XML文件、算法包XML文件中的算法邏輯塊的文件地址，再將文件地址存儲(chǔ)起來，隨后依據(jù)XML文件數(shù)據(jù)提取軟件的執(zhí)行流程，來解析所有的XML文件。XML文件數(shù)據(jù)解析的基本流程如圖4所示，讀取到XML文件中數(shù)據(jù)的開始標(biāo)簽＜start>，進(jìn)入此標(biāo)簽的數(shù)據(jù)存儲(chǔ)結(jié)構(gòu)，對(duì)標(biāo)簽內(nèi)的數(shù)據(jù)進(jìn)行數(shù)據(jù)的映射，包括讀到＜inputs>標(biāo)簽時(shí)，把數(shù)據(jù)存儲(chǔ)至node的輸入?yún)?shù)；＜o(jì)utputs>標(biāo)簽，把數(shù)據(jù)存儲(chǔ)至node的輸出參數(shù)；＜locals>標(biāo)簽，把數(shù)據(jù)存儲(chǔ)至node的局部變量；＜data>標(biāo)簽，把數(shù)據(jù)存儲(chǔ)至node的控制算法區(qū)，當(dāng)讀取到結(jié)束標(biāo)簽＜start>，則完成了這個(gè)XML文件信息的提取，循環(huán)讀取工程的其他XML文件信息。最終，實(shí)現(xiàn)了把一個(gè)工程的XML文件解析成了一個(gè)Lustre程序。

圖2 XML文件數(shù)據(jù)結(jié)構(gòu)圖Fig.2 XML File data structure diagram

圖3 Lustre代碼基本結(jié)構(gòu)Fig.3 Basic structure of Lustre code

圖4 XML文件信息提取過程Fig.4 XML File information extraction process

3 可信代碼自動(dòng)生成軟件設(shè)計(jì)

在基于形式化驗(yàn)證技術(shù)的可信代碼生成領(lǐng)域，常用的方法包括：翻譯驗(yàn)證（translation validation）[6-8]，它是一種等價(jià)性驗(yàn)證方式，是一種輕量級(jí)形式化驗(yàn)證技術(shù)，不需要對(duì)代碼生成軟件本身進(jìn)行驗(yàn)證，核心在于構(gòu)造一個(gè)翻譯驗(yàn)證器；定理證明[9,10]，這是一種重量級(jí)形式化驗(yàn)證技術(shù)，是最嚴(yán)格的驗(yàn)證方式，其對(duì)代碼生成過程本身進(jìn)行證明，可保證代碼生成過程的正確性，最著名的代表作是CompCert編譯器[11-14]。為解決圖形化模型轉(zhuǎn)化為C程序過程中可能存在的誤編譯問題，基于前人成功的經(jīng)驗(yàn)，在可信代碼生成軟件的開發(fā)過程中，引入形式化驗(yàn)證技術(shù)——定理證明，通過對(duì)代碼生成過程的正確性進(jìn)行驗(yàn)證，保證源語言與目標(biāo)語言語義的一致性，進(jìn)而保證代碼生成過程的正確性。如圖5所示，為可信代碼生成軟件的形式化開發(fā)架構(gòu)圖。總共包括4層：

1）形式化規(guī)范描述層：研究了可信代碼生成軟件的功能需求和安全屬性需求，并在輔助定理證明工具Coq[15]中將其轉(zhuǎn)換為形式化規(guī)范描述。如圖5所示，為了簡(jiǎn)化證明框架和滿足代碼生成軟件的功能需求，引入了7種中間建模語言將整個(gè)代碼轉(zhuǎn)換過程拆分成8個(gè)翻譯階段，對(duì)這些中間建模語言的控制語句、時(shí)態(tài)算子、高階算子的行為、狀態(tài)轉(zhuǎn)換以及安全屬性等使用操作語義[16-18]進(jìn)行規(guī)范描述，得到其動(dòng)態(tài)語義模型。在此基礎(chǔ)上，可開發(fā)語義一致性的性質(zhì)、定理，進(jìn)而對(duì)翻譯過程的語義一致性進(jìn)行驗(yàn)證，這是形式化邏輯驗(yàn)證層的基礎(chǔ)。

2）形式化邏輯驗(yàn)證層：圖5中雙箭頭表示對(duì)形式化規(guī)范描述層中定義的安全屬性和語義一致性進(jìn)行驗(yàn)證，經(jīng)過邏輯推理證明成功后，代碼生成過程中翻譯前后語義具有一致性且滿足定義的安全屬性。在邏輯驗(yàn)證過程中，為解決驗(yàn)證工作的可復(fù)用性差等問題，創(chuàng)造性地提出“小步驗(yàn)證”和“反向驗(yàn)證”的方法。“小步驗(yàn)證”基于7種中間建模語言將整個(gè)翻譯過程拆分為多個(gè)“小步”，每步只完成固定驗(yàn)證任務(wù)，降低了證明過程的難度。“反向驗(yàn)證”是由通常的從前往后按順序驗(yàn)證，轉(zhuǎn)變?yōu)閺暮笸暗尿?yàn)證方式，其目地是保證所做的證明過程完成后，不會(huì)因?yàn)楹罄m(xù)的證明過程出現(xiàn)錯(cuò)誤而推翻已證明的內(nèi)容。

3）驗(yàn)證后算法抽取層：驗(yàn)證后的可信算法抽取采用輔助定理證明工具Coq完成，在Coq中編寫的翻譯算法通常是可以用常規(guī)函數(shù)式程序設(shè)計(jì)語言實(shí)現(xiàn)的函數(shù)模型。通過Coq的抽取機(jī)制（Extraction），在可信代碼生成軟件開發(fā)過程中，把邏輯驗(yàn)證成功后的翻譯算法中的每個(gè)函數(shù)自動(dòng)映射到OCaml語言中對(duì)應(yīng)的函數(shù)，經(jīng)二次編譯后，得到可信代碼生成軟件的可運(yùn)行程序。在Coq中開發(fā)的翻譯算法如實(shí)地描述了抽取出的算法的行為，滿足在形式化開發(fā)中描述的規(guī)范說明，并且在邏輯驗(yàn)證層對(duì)算法的證明進(jìn)行了邏輯證明，故Coq抽取出的每個(gè)算法都是可信的，進(jìn)而保證了可信代碼生成軟件的安全性和可信性。

4）可信代碼生成軟件應(yīng)用層：圖形化的算法模型經(jīng)XML文件信息提取成Lustre程序后，經(jīng)可信代碼生成軟件的處理后生成可信的C程序。

圖5 可信代碼生成軟件架構(gòu)圖Fig.5 Software architecture diagram of trusted code generation

基于形式化驗(yàn)證技術(shù)的可信代碼生成軟件是基于嚴(yán)格的數(shù)學(xué)理論和形式化方法，其代碼生成的正確性和安全性經(jīng)過嚴(yán)格數(shù)學(xué)推理證明，可免去代碼單元測(cè)試環(huán)節(jié)，進(jìn)而有效縮短了驗(yàn)證時(shí)間和提升了建模效率。

4 軟件集成使用

目前，儀控工程師通過圖形化建模軟件NASPES來開發(fā)圖形化控制算法，然后通過調(diào)用SCADE KCG把它轉(zhuǎn)化C程序，然后把得到的C程序下裝到NASPIC平臺(tái)中，最后經(jīng)二次編譯后，生成可執(zhí)行代碼在控制器中運(yùn)行。基于本文的研究，實(shí)現(xiàn)了XML文件數(shù)據(jù)提取軟件和可信代碼生成工具后，可完全替換代碼生成工具KCG，實(shí)現(xiàn)NASPIC平臺(tái)的完全國產(chǎn)化。由于在可信代碼生成工具的開發(fā)過程中，除了使用V&V和測(cè)試的手段來保證其可信性，還采用形式化驗(yàn)證方法對(duì)代碼生成器的開發(fā)過程進(jìn)行正確性的驗(yàn)證。因此，生成的代碼的可信性在理論上超過KCG。

把圖形化建模軟件、XML文件數(shù)據(jù)提取軟件和可信代碼生成軟件集成后使用。如圖6所示，儀控工程師通過在圖形化建模軟件中拖拽算法圖符塊來創(chuàng)建控制算法，然后調(diào)用XML文件信息提取軟件把圖形化控制算法對(duì)應(yīng)的XML文件數(shù)據(jù)轉(zhuǎn)化為L(zhǎng)ustre程序，然后調(diào)用可信代碼生成軟件把生成的Lustre程序轉(zhuǎn)化為可信C代碼，最后經(jīng)二次編譯后下裝到核安全級(jí)DCS平臺(tái)，控制核電廠的安全、可靠地運(yùn)行。

5 結(jié)束語

本文針對(duì)核安全級(jí)DCS系統(tǒng)控制算法開發(fā)環(huán)境完全依賴國外進(jìn)口的現(xiàn)狀，基于圖形化建模技術(shù)、XML文件解析技術(shù)和形式化驗(yàn)證技術(shù)，提出了一種適用于核安全級(jí)DCS系統(tǒng)的、由模型驅(qū)動(dòng)代碼自動(dòng)生成的控制算法設(shè)計(jì)方法。圖形化控制算法設(shè)計(jì)降低了對(duì)儀控工程師的編碼能力要求，擺脫了傳統(tǒng)“手工編碼”設(shè)計(jì)控制算法的方式，把控制算法開發(fā)人員從易出錯(cuò)的編碼語義、語法設(shè)計(jì)和反復(fù)的代碼驗(yàn)證等繁復(fù)的工作中解放出來，更專注于核安全級(jí)DCS系統(tǒng)控制算法設(shè)計(jì)本身，從而提高控制算法設(shè)計(jì)效率，保證算法的可信性；形式化驗(yàn)證技術(shù)用于可信代碼生成軟件的開發(fā)，保證了圖形化算法模型轉(zhuǎn)化成正確的目標(biāo)C程序，可完成在NASPIC平臺(tái)中對(duì)代碼生成工具KCG的替換。完成NASPIC平臺(tái)中的代碼生成器KCG的替換具有重要的意義，一方面，可避免由于KCG代碼黑盒帶來的安全隱患，提高DCS系統(tǒng)安全性；另一方面，將擺脫核電關(guān)鍵建模軟件受制于人的境地，實(shí)現(xiàn)NASPIC平臺(tái)的完全自主化。

圖6 模型驅(qū)動(dòng)代碼自動(dòng)生成流程圖Fig.6 Flow chart of model-driven code automatic generation