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

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

0 引言

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

1 圖形化建模軟件

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

1.1 設(shè)備建模

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

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

1.2 變量建模

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

1.3 算法建模

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

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

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

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

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

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

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

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

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

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

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

4 軟件集成使用

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

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

5 結(jié)束語

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

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