核安全級DCS系統模型驅動可信代碼自動生成方法

蘭 林，馬 權，侯榮彬，李 勇，楊 斌，榮健兵，吳延群

（1.中國核動力研究設計院 核反應堆系統設計技術重點實驗室，成都 610213；2.哈爾濱工程大學，哈爾濱 150000）

0 引言

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

1 圖形化建模軟件

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

1.1 設備建模

圖1 圖形建模結構示意圖Fig.1 Schematic diagram of graphical modeling structure

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

1.2 變量建模

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

1.3 算法建模

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

2 XML文件數據提取

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

Lustre是一種同步數據流語言[5]，一個Lustre程序是由多個node構成，node相當于C語言中的一個函數，不同點在于其輸入參數和輸出參數是一個流（Stream），源源不斷地處理從控制現場采集到的數據，node的基本結構如圖3所示，其中node、returns、var、let、tel為Lustre程序的關鍵字。在XML文件數據提取過程中，XML文件數據提取軟件首先加載工程配置XML文件，獲取到所有的組合邏輯塊XML文件、預定義XML文件、算法包XML文件中的算法邏輯塊的文件地址，再將文件地址存儲起來，隨后依據XML文件數據提取軟件的執行流程，來解析所有的XML文件。XML文件數據解析的基本流程如圖4所示，讀取到XML文件中數據的開始標簽＜start>，進入此標簽的數據存儲結構，對標簽內的數據進行數據的映射，包括讀到＜inputs>標簽時，把數據存儲至node的輸入參數；＜outputs>標簽，把數據存儲至node的輸出參數；＜locals>標簽，把數據存儲至node的局部變量；＜data>標簽，把數據存儲至node的控制算法區，當讀取到結束標簽＜start>，則完成了這個XML文件信息的提取，循環讀取工程的其他XML文件信息。最終，實現了把一個工程的XML文件解析成了一個Lustre程序。

圖2 XML文件數據結構圖Fig.2 XML File data structure diagram

圖3 Lustre代碼基本結構Fig.3 Basic structure of Lustre code

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

3 可信代碼自動生成軟件設計

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

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

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

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

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

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

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

4 軟件集成使用

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

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

5 結束語

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

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