文獻標識碼：B文章編號：1003-0492（2025）11-105-07中圖分類號：TL362

★洪鑫喆，張亞棟，武方杰，杜喬瑞，首云旭（北京廣利核系統工程有限公司，北京100094）

關鍵詞：安全軟件；形式化驗證；可靠性；安全性；數學模型；邏輯推理

核電作為一種高效、低碳的能源，在全球能源結構中占據著日益重要的地位。當前世界各國的核電廠廣泛使用數字化的儀表控制系統。國際原子能機構（International Atomic Energy Agency，IAEA）的統計數據顯示，截至2024年，全球在運核電機組中，超過95%的機組使用了先進的儀控系統。在中國，隨著國內核電產業的快速發展，我們自主研發的數字化儀控系統如和睦系統等，已成功應用于華龍一號等自主化三代核電項目中，為我國核電項目的安全穩定運行提供了有力保障。

隨著數字化的儀表控制系統的廣泛應用，核電安全軟件的復雜性日益增加，這給軟件的開發、維護和驗證帶來了巨大挑戰。1999年，法國格拉夫林核電站的計算機控制系統軟件錯誤導致反應堆被迫緊急停堆；2005年，英國欣克利角B核電站控制系統的軟件未能正確處理蒸汽發生器的傳感器數據，錯誤地觸發了保護機制，導致反應堆自動停堆。

目前，我國針對核安全級軟件的驗證主要采用傳統的V&V方法。V&V方法通過測試評估和分析等綜合手段，顯著提高了核電系統的可靠性和安全性，還能夠為核電站的許可證申請、運行許可和合規性評估提供關鍵證據，確保其符合國際和國內的法規標準。盡管傳統V&V方法在核電中具有重要作用，但其實施也面臨一些挑戰和不足：由于核電系統的規模和復雜性，V&V方法可能難以覆蓋所有可能的運行場景，存在一定的局限性。而形式化驗證方法通過數學建模和邏輯推理，能夠系統性地驗證軟件的正確性，顯著提升了驗證的全面性和可靠性，因此在核電安全軟件中逐漸成為重要的驗證手段。

本文對核電廠儀控系統的軟件驗證方式開展了研究，并對近年來形式化驗證技術的應用案例進行總結，分析了形式化驗證技術在核電軟件中的可行性，展望了形式化驗證的未來發展方向。

1　形式化驗證方法概述

1.1　定義與原理

形式化驗證是一種借助數學邏輯和形式化語言，對系統進行嚴格驗證的方法。其核心在于將系統的行為和屬性通過精確的數學模型予以描述，并運用嚴密的數學推理來證明系統是否滿足預先設定的性質和需求。

形式化語言是描述系統行為和屬性的基礎工具，它具有精確、無歧義的語法和語義規則，能夠清晰、準確地表達系統的各種特性和約束條件。基于這些形式化語言，形式化驗證通過構建系統的形式化模型，將系統轉化為數學對象，以便進行精確的分析和推理。

在構建形式化模型后，形式化驗證運用不同的方法對模型進行驗證，以證明系統滿足預定的性質和需求。它運用的主要方法有定理證明^[1]和模型檢測^[2]。

其中，模型檢測通過狀態搜索來驗證軟件系統模型的有窮狀態空間，從而檢驗系統的行為是否具備預期性質。模型檢測的基本思想是用狀態遷移系統（S）表示系統的行為，用模態/時序邏輯公式（F）描述系統的性質。這樣一來，系統是否具有所期望的性質就轉化為數學問題：狀態遷移系統S是否是公式F的一個模型。模型檢測的優點是可以自動化驗證，但主要問題是狀態空間爆炸問題。

而定理證明的主要思想是以邏輯推理為基礎，通過公理或者推理規則，證明系統具有某些性質。邏輯推理的方法有自然推演、歸納、Hoare邏輯、時序演算等。定理證明的優點是可以用歸納方法處理無限狀態的問題，缺點是不能做到完全自動化驗證。對于稍微復雜的系統，人工推理驗證的效率很低。

1.2　形式化驗證的優勢

在核電安全軟件中，對于一些復雜的模塊，傳統測試方法很難覆蓋到所有可能的輸入組合和邊界條件，而形式化驗證可以通過建立精確的數學模型，對這些算法和邏輯進行嚴格的推理和驗證，從而發現潛在的錯誤和不一致性。這種精確性和可靠性使得形式化驗證能夠為核電安全軟件提供更高的可信度，有效降低了軟件故障引發安全事故的風險。

在對核電安全軟件的驗證中，形式化驗證可以從軟件的需求規格說明書出發，通過建立形式化模型，對軟件的需求、設計和實現過程進行全程跟蹤和驗證，涵蓋軟件開發周期的各個層面和環節，大大降低了軟件開發的成本和風險，提高了開發效率，并最終確保了軟件在整個生命周期內都符合安全標準和要求。

1.3　核電安全標準適用性分析

目前國際上用于指導核電廠系統軟件開發的標準和法規主要來源于IEC國際標準、LAEA有關導則和美國IEEE標準。其中，部分標準對形式化驗證提出了相關要求：在核電標準IEC 60880^[3]中，建議使用形式化語言描述需求，對于代碼生成器部分建議使用形式化驗證；在核電標準IEC 61508^[4]中，如圖1所示，建議對安全完整性等級SIL 2及以上的系統采用形式化方法。

圖1核電標準IEC 61508中對形式化驗證方法的要求

2　形式化驗證技術研究

2.1　核電軟件多層模型驗證框架

針對核電數字化儀控系統軟件的特點和安全需求，在核電軟件的形式化驗證過程中一般采用分層驗證的方式，和軟件的生命周期一一對應，從需求、設計和實現階段，分別進行形式化驗證。這種分層驗證策略能夠降低驗證的復雜度，提高驗證的效率和準確性。

在需求層，主要定義內存管理組件軟件需求，一般采用形式化驗證語言進行描述和構造。首先，需求層主要通過狀態機模型，給出內存管理組件的狀態定義以及基本執行模型；其次，基于這個執行模型，定義內存管理組件需求功能點。在設計層，主要定義軟件的設計和技術要求，用形式化語言構造設計層的數據結構以及基于這些數據結構的算法設計。在實現層，主要是等價地表示C代碼的語句，采用Simpl語言庫，從C代碼等價地構造Simpl語言的語句，可以有效表達操作系統C代碼的語法和語義。

在具體的驗證方法上，主要技術包括模型檢測和定理證明。由于對于底層系統軟件的形式驗證，模型檢測存在狀態空間爆炸的問題，因此本文重點介紹基于定理證明的驗證方法：即基于形式規范求精（Refinement）技術。該技術使用精化證明方式驗證不同抽象層次模型間的一致性，用于需求、設計、實現階段的正確性和安全性驗證；采用增量證明的方法驗證各層模型的安全性質，以減輕迭代開發過程中的證明工作量，最終提供滿足軟件認證要求的形式化證據。

圖2形式化驗證策略圖

2.2　定理證明驗證過程

使用定理證明方法驗證核電軟件的通常思路如下：

（1）構建抽象模型

抽象模型由狀態機、安全屬性以及安全屬性的推導關系組成。在狀態機模型中，狀態變量表示系統的狀態，轉移函數和輔助函數用以描述狀態變量的變化過程。狀態轉移函數是系統對外暴露接口的抽象，它們描述了系統狀態如何變化。安全屬性是系統安全需求的形式化描述。在形式化的安全模型中，最為關鍵的部分就是安全性證明，它的核心證明為對安全屬性的可滿足性證明。抽象模型使用Isabelle的locale關鍵字定義，其中的參數都是抽象類型，而不涉及具體的數據結構和函數實現，以便聚焦于系統性質的描述，這些抽象參數在具體模型中被精化為具體實現。

（2）構建具體模型

具體模型即是對抽象模型的精化，由執行模型和事件規約組成。具體來說是在系統狀態中增加了新的狀態變量，并描述了更具體的程序行為。

（3）正確性證明

正確性證明可以拆解為對模型的事件規約中每個具體事件的正確性證明。通常使用霍爾邏輯描述并驗證模型的正確性。霍爾邏輯的核心是霍爾三元組：{P}C{Q}，其中P和Q是一階邏輯公式，分別表示前置條件和后置條件，C表示程序片段。霍爾三元組表示：只要前置條件P在執行命令C之前的狀態下成立，那么執行之后后置條件Q也應該成立。如果命令C不終止，后置條件Q可以是任何語句，甚至可以為假，這被稱為部分正確性。如果C終止并且在終止時Q為真，則表達式被稱為全部正確性，終止性必須單獨證明。

（4）精化證明

具體模型是對抽象模型的精化，精化證明需要驗證具體模型的行為與抽象模型行為保持一致。通過引用抽象模型中提出的規約，在具體模型中找到對應的規約，利用定理證明器證明兩者之間的一致性。如圖3所示，既要證明抽象模型和具體模型的狀態滿足精化關系，還要證明兩者的狀態由于事件φ發生遷移后依然保持一致性。通過精化關系的驗證，可以復用抽象模型中已經驗證的性質，從而減少具體模型中證明的工作量。

圖3模型精化關系圖

（5）增量證明

在精化證明確保了所有事件對于原有狀態變量的修改與上層一致之后，下層模型可以充分利用上層已驗證的性質，只需對新增狀態變量進行正確性和安全性驗證。這種做法有助于提高驗證的效率，避免重復的驗證工作。

3　形式化驗證工具介紹

形式化驗證工具是確保系統（如軟件、硬件、嵌入式系統等）在所有可能的輸入和執行路徑下都能正確運行的重要手段。這些工具通過數學建模和邏輯推理，驗證系統是否滿足特定的規范。在形式化驗證中，常用的工具主要分為模型檢測器（針對模型檢測）、定理證明器（針對定理證明）以及其他專門化的驗證工具。

模型檢測器（Model Checkers）是形式化驗證中最常用的一類工具，它們通過構建系統的狀態空間并檢查這些狀態是否滿足給定的邏輯規范（如線性時序邏輯LTL或計算時序邏輯CTL）。目前，學術和工業界已開發出了大量的模型檢驗器，它們根據所檢驗規格的特點可分為時態邏輯模型檢驗器、行為一致檢驗器和復合檢驗器。

（1）時態邏輯模型檢驗器

時態邏輯模型檢驗器中，EMC和CESAR是最早的兩個；SMV^[5]中使用了OBDD；Spin^[6]中采用偏序關系簡化來改善狀態組合復雜性；Murphi和UV基于Unity編程語言；Kronos用于實時系統。

（2）行為一致檢驗器

行為一致檢驗器中，Cospan/Formal Check基于自動機間的包含；FDR檢驗CSP程序的細化；Concurrency Workbench檢驗CCP程序的細化。

（3）復合檢驗器

復合檢驗器中，HSIS復合模型檢驗和語言包含；Step復合模型檢驗和演繹方法；VIS復合模型檢驗和邏輯綜合；PVS定理證明器中有用于模態mμ演算的模型檢驗器；META Frame是支持整個軟件開發過程模型檢驗的環境。

定理證明器（Theorem Provers）是另一種重要的形式化驗證工具，它們通過邏輯推理來驗證系統是否滿足特定的規范。定理證明器主要包括交互式定理證明器和自動定理證明器兩大類。以下是一些具體的工具介紹：

（1）交互式定理證明器

交互式定理證明器需要使用者的引導，要求用戶有豐富的數學經驗。它們允許用戶逐步構建證明過程，并在每個步驟中檢查證明的正確性。主要的交互式定理證明器包括：

·Coq^[7]：Coq是一種強大的交互式定理證明工具，廣泛應用于形式化驗證和數學定理的證明。它提供了一種嚴格的類型系統，支持依賴類型和多態類型，使得編寫復雜的證明和程序變得更加容易。Coq還提供了豐富的庫和插件系統，支持用戶定制和擴展其功能。

·HOL^[8]（Higher-Order Logic）：HOL是指一系列使用高階邏輯作為支撐的交互式定理證明器。它們的特點是使用謂詞演算，允許變量在謂詞和函數之間進行游離轉換。HOL通過模型謂詞來驗證公理的可靠性，廣泛應用于形式化驗證和數學定理的證明。

·Isabelle^[9]：Isabelle也是一個強大的交互式定理證明器，它基于高階邏輯，提供了豐富的編程功能和自動化證明工具。它已經被成功應用于多個操作系統內核的驗證，并顯示了良好的效果和可靠性。

（2）自動定理證明器

自動定理證明器能夠自動或半自動地生成和驗證定理的證明，較少或不需要人為干預。主要的自動定理證明器包括：

·CiME：CiME是法國國立高等信息企業學院編寫的自動定理證明器。它通過在用戶所定義的項代數上進行計算、歸一、重寫邏輯和數學推導來進行策略驗證。CiME彌補了某些交互式定理證明器需要手動提取構造生成證明過程的缺點。

·Prover9：Prover9是一種采用一階邏輯的自動定理證明器。其輸入文件是邏輯規范與待證明的目標列表，最終給出對約束是否滿足的判斷。Prover9在自動驗證角色訪問控制策略等領域有著廣泛的應用。

此外，還有其他一些自動定理證明器，如Vampire、Z3等，它們各自具有不同的特點和優勢，適用于不同的驗證場景和需求。

交互式定理證明器相比自動定理證明器具有幾個顯著的優勢，主要體現在以下方面：

交互式定理證明器不僅能夠判斷定理的真假，更重要的是能夠提供形式化的證明過程。這使得用戶能夠深入理解定理的證明邏輯和細節，有助于增強對定理的理解，幫助用戶處理更廣泛、更復雜的數學問題。相比之下，自動定理證明器雖然能夠自動或半自動地生成證明，但往往只提供最終的證明結果，而不展示詳細的證明過程，這在一定程度上限制了用戶對證明過程的理解和掌握。

綜上所述，交互式定理證明器在提供形式化證明過程、處理復雜數學問題、直觀展示證明過程和定制化證明過程等方面具有顯著的優勢。這些優勢使得交互式定理證明器在數學、計算機科學和工程學等領域中得到了廣泛的應用，而在核電安全軟件的證明中同樣適合使用交互式定理證明器進行證明。

4　形式化驗證技術在核電廠DCS的應用

4.1　可信編譯器的驗證

核電應用軟件的開發流程，在需求、設計和實現階段分別有各自的模型描述語言。如圖4所示，在實際開發過程中，可以使用代碼生成工具實現上述語言的自動轉化。通常代碼生成工具不僅需要完成語言的轉換，還要求保證轉換前后語義具有一致性。在這個過程中，“誤編譯”問題是編譯器中常見的錯誤之一。對于核電這樣的安全攸關系統^[10]而言，必須考慮編譯器引入的錯誤，否則在源程序級進行的驗證工作可能在目標程序級失效。為保證編譯器的正確性，傳統上一般采用大量的測試以及嚴格的軟件過程管理，但這并不能杜絕“誤編譯”的發生。對編譯器進行正確性驗證是解決問題的根本途徑，而最嚴格的驗證手段莫過于采用形式化方法。可信編譯技術開發的代碼生成工具恰好具備上述性質。近年來，有關編譯器形式化驗證的研究工作取得了長足的進步，已達到了實用化水平。使用定理證明方法開發的編譯器的成功案例為核電應用軟件的開發流程，在需求、設計和實現階段分別有各自的模型描述語言。如圖4所示，在實際開發過程中，可以使用代碼生成工具實現上述語言的自動轉化。通常代碼生成工具不僅需要完成語言的轉換，還要求保證轉換前后語義具有一致性。在這個過程中，“誤編譯”問題是編譯器中常見的錯誤之一。對于核電這樣的安全攸關系統^[10]而言，必須考慮編譯器引入的錯誤，否則在源程序級進行的驗證工作可能在目標程序級失效。為保證編譯器的正確性，傳統上一般采用大量的測試以及嚴格的軟件過程管理，但這并不能杜絕“誤編譯”的發生。對編譯器進行正確性驗證是解決問題的根本途徑，而最嚴格的驗證手段莫過于采用形式化方法。可信編譯技術開發的代碼生成工具恰好具備上述性質。近年來，有關編譯器形式化驗證的研究工作取得了長足的進步，已達到了實用化水平。使用定理證明方法開發的編譯器的成功案例為。

圖4可信編譯技術在核電廠儀控工程應用軟件開發過程中的應用

4.2　應用軟件驗證

算法塊作為核電站數字化儀控系統中應用軟件的重要組成部分，其運行在核安全級相關控制系統的控制器中，是控制核反應堆安全穩定運行的關鍵。如何針對算法塊進行測試用例的設計，保證其在核電站控制系統中運行的正確性，對保障核電儀控系統運行的穩定性和安全性、實現核反應堆控制功能等方面具有重要意義。

算法塊測試用例的設計是保證其質量的重要手段，也是算法塊軟件測試的核心內容^[13]。核電儀控系統驅動算法塊的輸入/輸出信號較多，且在結構和功能上比一般的算法塊更加復雜。為提高算法塊測試的針對性和效率、保證算法塊功能達到要求的可用性和安全性，算法塊測試用例的設計工作對核電儀控系統的安全性測試具有重要意義。

核電站數字化儀控系統中，應用軟件的傳統算法測試用例是基于功能性的設計方法進行輸入輸出關系的推理，從而形成測試用例。但驅動算法塊邏輯較為復雜，且與現場操作流程及工藝密切相關，需要結合核電站現場的指令操作進行輸入輸出關系的推斷。因此，保證測試用例設計的完整性和充分性就更加困難。孔艷等人^[14]提出了一種基于場景的驅動算法塊測試用例設計方法。該方法將應用軟件中的算法塊劃分為多個場景，一個場景的狀態由場景的狀態集合和變遷條件的集合構成。根據生成的場景狀態圖，基于場景路徑覆蓋的分析，便可生成測試設計及用例，并滿足測試充分性要求。

4.3　操作系統驗證

在核電安全軟件中，操作系統是最復雜的軟件之一，它大多用C語言內嵌匯編語言實現，還包含許多難以分解的相互依賴的組件和程序模塊。C語言中混合匯編語言還需要進行寄存器和棧的操作，導致語義非常復雜。作為安全關鍵嵌入式系統的核心基礎軟件，嵌入式操作系統的安全性成為關注的焦點，用形式化的方法證明嵌入式操作系統的正確性已成為當前工業界和學術界的熱點。當前國內外使用形式化驗證方法驗證的操作系統有seL4^[15]、PikeOS^[16]、CertiKOS^[17]等，其中seL4微內核操作系統是目前操作系統形式化驗證的典范。seL4大約有8700行C代碼，在形式化驗證之前，該操作系統通過測試僅發現了16個缺陷，而通過形式化驗證共發現了144個缺陷。seL4操作系統的形式化驗證方法是交互式機器協助定理證明，使用的定理證明工具是Isabelle/HOL。姜菁菁等人^[18]利用定理證明工具Coq對操作系統任務管理模塊進行了需求層建模及形式化驗證。

目前，核電行業的操作系統形式化驗證案例尚且缺乏，而實時操作系統屬于核電廠數字儀控系統的核心部分，要在規定的時間內對控制系統作出快速響應，在核電廠數字化儀控系統中具有無可替代的重要性。如果在未來能用形式化驗證的方法測試核電的實時操作系統，就能夠驗證操作系統是否滿足核電IEC 62138標準和操作系統相關標準中的接口、功能和性能需求，從而確保其可靠性和安全性。

圖5操作系統的形式化設計和驗證框架

5　形式化驗證方法未來發展趨勢

目前形式化方法存在一些局限性，比如定理證明方法存在驗證效率較低、模型檢測方法存在狀態爆炸問題。

隨著人工智能技術的快速發展，未來形式化驗證技術將與人工智能等新興技術進行融合應用，實現形式化驗證過程的自動化和智能化。

在算法優化方面，未來形式化驗證技術將致力于提升驗證效率和處理復雜系統的能力。智能增強技術能夠很好解決上述問題，其主要包含以下的驗證算法：

（1）基于機器學習的自動定理證明方法：其將機器學習技術應用于自動定理證明，以提高自動定理證明方法的效率和可擴展性。

（2）基于符號和數值相結合的自動定理證明方法：其將符號方法和數值方法相結合，以解決復雜和大型的邏輯公式或推理問題。

（3）基于分布式和并行計算的自動定理證明方法：其將分布式計算和并行計算技術應用于自動定理證明，以提高自動定理證明方法的可擴展性。

在工具開發方面，未來將更加注重形式化驗證工具的易用性、自動化和集成化。

6　結論

核電安全軟件的形式化驗證是保障核電站安全運行的重要技術手段。本文通過分析核電安全軟件的發展現狀、形式化驗證方法的原理與工具及其在核電領域的應用，揭示了形式化驗證在提升軟件可靠性和安全性方面的獨特優勢。盡管形式化驗證在實際應用中仍面臨成本高、工具復雜性和專業人才稀缺等挑戰，但其在核電安全軟件中的應用前景依然廣闊。未來，隨著人工智能、算法優化和工具開發的進一步發展，形式化驗證技術將更加高效、智能化和易用，為核電安全軟件的開發和驗證提供更強大的技術支持，從而推動核電產業的可持續發展。

★國家重點研發計劃資助項目（項目號2022YFB4501905）。

作者簡介：

洪鑫喆（2000-），男，安徽人，工程師，理學學士，現就職于北京廣利核系統工程有限公司，主要從事于核安全級儀控系統的軟件測試工作。

參考文獻：

[1] Nipkow T, Paulson L C, Wenzel M. Isabelle/HOL: A proof assistant for higher - order logic[M]. Berlin, Heidelberg: Springer, 2002.

[2] Kokologiannakis M, Vafeiadis V. GenMC: A model checker for weak memory models[C]//Silva A, Leino K R M. Proceedings of the 33rd International Conference on Computer Aided Verification. Berlin, Heidelberg: Springer, 2021: 427 - 440.

[3] Nukleare Instrumentierung. Erfahrungsbericht ueber die Anwendung der IEC 60880 (1986) Nuclear Instrumentation - A Review of the Application of IEC 60880(1986) Instrumentation nucleaire. Revue de lpplication de la CEI 60880 (1986) IEC 61940: 1998.

[4] Functional safety of electrical/electronic/programmable electronic safety - related systems - Part 6: Guidelines on the application of IEC 61508 - 2 and IEC 61508 - 3(IEC 61508 - 6:2010); German version EN 61508 - 6:2010

[5] Bengtsson J, Larsen K, Larsson F, et al. Uppaal - a Tool Suite for Automatic Verification of Real - Time Systems[C]//New Brunswick, New Jersey: Proceedings of the 4th DIMACS Workshop on Verification and Control of Hybrid Systems, 1995 : 232 - 243.

[6] Holznmnn J. The Model Checker SPIN [J]. IEEE Transactions on Software Engineering, 1997, 23 (5) : 279 - 295.

[7] Coq Development Team. The Coq Proof Assistant[EB/OL], 2012 - 07.

[8] Michael J. Introduction to the HOL System[R]. TPHOLs. New York, USA: IEEE Computer Society, 1991: 2 - 3.

[9] Nipkow T, Paulson L, Wenzel M. Isabelle/HOL - A Proof Assistant for Higher - Order Logic[M]. Germany: Springer, 2002.

[10] KNIGHT J C. Safety critical systems: challenges and directions[C]// Proceedings of the 24th International Conference on Software Engineering. 2002: 547 - 550.

[11] LEROYX. Formal verification of a realistic complier [J]. Communications of the ACM, 2009, 52(7): 107 - 115.

[12] 潘建勇, 陳邦興. 基于場景的測試用例設計方法研究[J]. 通信技術, 2011, 44 (12) : 4.

[13] 孔艷, 裴紅偉. 核電儀控系統驅動算法塊測試設計研究與應用[J]. 自動化儀表, 2021, 42 (S01) : 5.

[14] Klein G, Elphinstone K, Heiser G, et al. seL4: Formal verification of an OS kernel[C]//Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles. New York: ACM Press, 2009: 207 - 220.

[15] SYSGO. PikeOS home page[EB/OL], 2020 - 06 - 02.

[16] The Flint Group. CertiKOS home page[EB/OL], 2020 - 06 - 02.

摘自《自動化博覽》2025年11月刊