★北京廣利核系統工程有限公司李幼媛，張亞棟，武方杰，杜喬瑞，首云旭，孫王強，洪鑫哲

關鍵詞：核電嵌入式操作系統；形式化建模；內存管理；Isabelle

核電儀控系統的軟件^[1]主要構成如圖1所示，其中安全軟件主要是基于計算機系統的軟件，包括操作系統軟件、應用軟件以及通信軟件等。其中，操作系統軟件為其他軟件提供基本的任務管理、內存管理等支撐功能，是系統運行的基礎，也是核安全級儀控系統的靈魂，具有不可替代的作用。操作系統軟件的安全可靠是構建高可靠平臺軟件的關鍵，任何一個微小的內核錯誤都可能導致整個系統的崩潰。

圖1基于計算機的系統中硬件與軟件的典型關系

IEC61513^[2]是儀控系統總體要求全面規定了核電整個生命周期內各項活動的安全準則，為儀控系統的總體設計提供了指導。一些基本要求由下一層的核電廠安全重要儀控系統軟件相關標準IEC60880^[3]和IEC62138^[4]進行補充。在IEC61513的指導下，形成了核安全級軟件開發和驗證需要滿足的安全重要I&C系統軟件的基礎標準。核電安全相關系統中對軟件質量的相關標準是IEEE1012^[5]，即操作系統軟件作為一類典型的安全攸關嵌入式軟件，在投入使用前必須按照IEEE1012經過嚴格的驗證。

與傳統的仿真、測試等驗證技術相比，基于嚴格數學理論的形式化驗證技術能夠有效地進行全路徑檢查，且易于發現隱藏較深層次的錯誤，極大提高了驗證的覆蓋率和可信度。

形式化驗證技術主要包括定理證明和模型檢測。目前工業界和學術界大多使用定理證明的形式化方法對嵌入式操作系統軟件進行實踐，例如較典型的案例有seL4、CertiKOS等，都是通過形式化定理證明的方法來說明程序的執行效果滿足我們對它的期望（即形式規約）。

本文提出了適配核電生命周期流程的形式化建模和驗證整體框架，以及生命周期中各個階段的形式化執行流程，并以核電嵌入式操作系統軟件中的內存管理核心模塊為研究對象，深入分析了核電相關標準的安全要求和內存管理的特性，研究了內存管理的語義描述與驗證的一般性方法與理論。應用這些理論方法，本文驗證了一種具有實際應用的嵌入式操作系統的內存管理算法，證明了該方法可以作為驗證操作系統其他模塊的普適性方法。該研究成果有望直接應用于我國新一代儀控系統軟件的驗證，具有較高的實用價值。

1技術背景

1.1 核電驗證過程

核電儀控系統軟件開發和驗證的生命周期過程如圖2所示，驗證和確認（V&V）活動需按照標準IEEE1012中要求的軟件完整性等級執行。IEEE1012^[4]相關標準中也給出了各個階段的驗證目標，主要是檢驗并報告軟件開發過程中引入的錯誤，確保各個階段數據項的正確性、完備性、準確性、一致性等。其中一致性是指本階段的內容與上一階段的關系是一致的，例如設計階段中軟件設計與軟件需求的內容是一致的；正確性是指本階段實現內容是正確的，例如設計階段所實現的內容本身是正確的。

圖2儀控系統生命周期過程與驗證和確認活動之間的典型關系

1.2 定理證明

定理證明是系統及其特性均以某種數學邏輯公式表示的技術。邏輯由一個包含公理和推理規則的形式化系統給出。定理證明實質上是從系統公理中尋找特性證明的過程。證明采用公理或者規則，且可能推演出定義和引理。不同于模型檢驗，定理證明可以處理無限狀態空間問題。定理證明通常包括以下主要內容：

（1）形式規約：是指用精確的數學或邏輯描述系統必須滿足的性質或行為，它是形式化驗證的基礎，用于明確系統設計的正確性標準。

（2）形式建模：使用形式化工具來建立系統或程序行為的數學模型。

（3）形式驗證：使用數學方法來證明系統或程序行為的數學模型滿足給定的形式規約。

1.3　Isabelle

常用的定理證明器有Isabelle、Coq、Lean、W-Cert等。Isabelle作為一種通用的交互式定理證明器，其形式證明資源庫包含300多個開源項目。seL4內核4萬行的形式規約和20多萬行的形式證明均在Isabelle中開發證明，并且使用其微小的邏輯內核進行機器檢查。從技術上分析，Isabelle工具提供了基本的語言環境，即可以描述需求等抽象的規范，也可以描述算法等設計層的規范。另外，Isabelle支持多種對象邏輯、可擴展定義新的邏輯系統、豐富的類型系統和編程語言語法和語義的開發，C/Java等編程語言都可以在Isabelle中進行形式化的表示和證明。因此，本文采用Isabelle工具作為嵌入式操作系統內存管理算法的形式化驗證工具。

2形式化整體框架

本節將簡單介紹基于定理證明的嵌入式操作系統形式化建模和驗證框架。如圖3所示，該框架適用于圖2中需求、設計、實現過程的驗證目標，形式化對需求、設計、實現階段輸出的軟件進行驗證。其總體設計原則包括：

(1)在統一的驗證工具環境Isabelle中，建立需求、設計和源代碼的形式規范，確保三個層次的形式規范互相可集成、可驗證。

(2)針對不同的抽象層次，采用各自合適的形式規范語言，建立各層的形式描述，分別應對需求的抽象性、設計的邏輯性和實現的具體性。

(3)總體上，建立需求到設計、設計到實現之間嚴格的符合性，并提供形式化的證據。

圖3基于定理證明的形式化流程框架

需求、設計、實現三個階段的具體執行流程如圖4所示，需依照常規開發軟件所采用的輸入文檔材料，包括標準和三個階段的需求文檔、設計文檔和C代碼，并為各個階段相關的驗證目標提供證據支持。

圖4基于定理證明的階段形式化驗證執行流程

（1）建立形式規約：形式化的輸入是需求描述，即自然語言描述的文本文件和標準要求，①通過標準分析，提取相關系統性方面的要求，例如安全性、確定性等；②通過輸入文本文件，研究對象特點和邏輯，建立形式規約；

（2）構建狀態機模型：通過輸入文本文件，深入分析對象邏輯，構造出系統狀態機模型；

（3）構造形式模型：依據狀態機和對象的行為邏輯在Isabelle、工具中對操作行為進行建模。形式化模型是驗證的基礎，需深入分析行為邏輯，確保模型的正確性和準確性；

（4）驗證形式模型：將形式規約在Isabelle工具中轉化成引理，驗證行為模型是否滿足引理。如果滿足，則生成相應的驗證文件，如果不滿足則查看模型是否正確，直到性質滿足。

3　應用案例

根據國際上采用定理證明對操作系統的核心模塊進行驗證的成功案例，例如耶魯大學的Yu等人曾對一個C標準庫中的malloc/free簡化算法進行了嚴格的形式化驗證^[6]，本文結合形式化驗證整體框架和執行流程，圍繞核電某嵌入式操作系統的內存管理的設計層面的核心算法進行研究和應用。

3.1　核電需求描述

核電內存管理的需求主要來源于核電軟件相關標準以及操作系統相關標準。核電軟件相關標準^[3,4]中提出了在軟件的設計和實現過程中要考慮確定性方面的要求，即行為確定性、空間確定性和時間確定性。而時間確定性，即WCET（Worst-Case Execution Time，最壞響應時間），一般與特定的硬件平臺有關系。針對內存管理模塊核心算法，本文主要考慮行為確定性和空間確定性。

從設計層面考慮確定性，嵌入式操作系統內存管理的堆內存空間需提前靜態配置，即依據系統配置的兩個參數，一個是堆內存的物理起始地址Start，一個是堆結束地址End，來劃定整個堆內存空間。

根據操作系統的posix標準接口^[7]，內存管理按照圖1向其他軟件提供的API接口函數如表1所示，主要是分配和釋放。當其他軟件產生調用malloc，內存管理根據所需的內存大小去向其他軟件分配合適的內存空間，當其他軟件應用結束后調用free，內存管理去釋放相應的內存空間。

表1內存管理API接口

內存管理核心是通過三級管理算法（Three-Level，簡稱TL算法）來進行管理和實現的，采用雙向鏈表和位圖匹配兩種機制結合的方法快速定位空閑塊。TL算法分為三級：第一級中每個內存塊遞增8個字節，對應索引號從1～m；第二級中每個內存塊遞增64個字節，對應索引號從m+1～n；第三級中每個內存塊遞增1024個字節，對應索引號從n+1～k。每一個內存塊有一個索引號，從1到n，如圖5所示。

圖5三級空閑塊內存管理

每個索引號下的空閑內存塊都是通過雙向鏈表的形式處理移除和插入內存塊，使用位圖方式查找索引號，采用首次適配（First-Fit）原則，選取第一個匹配的內存塊，盡量在嵌入式操作系統中達到快速匹配的效果，而空閑內存塊在內存空間中的排列不是順序排列的。

3.2　形式規約

形式化中常見的形式規約類型有安全性、不變性等，其中不變性是系統始終滿足的邏輯約束，與核電領域關注的確定性比較契合。本文結合內存管理的文本要求，提取內存管理在核電行為、空間確定性和功能正確性方面的規約。

3.2.1　確定性規約

結合內存管理算法特點，分別從行為、空間資源角度進行確定性要求的提取。針對分配和釋放的行為需始終滿足的邏輯約束，提取的主要屬性如下：

（1）經給分配/釋放操作的內存塊狀態是確定的，即分配后的內存塊狀態是已使用，未分配的內存塊狀態應是空閑。

（2）經給分配/釋放操作的內存塊的地址是確定的，即任何兩個內存塊的地址不能重合。

（3）經過分配/釋放操作的空閑內存塊大小應在指定的三級范圍內。

（4）位圖中的每個True值對應的空閑塊列表為非空。

多次分配和釋放后的用戶使用的空間也是確定的，主要包括：

整個內存池空間是提前靜態配置確定的，即不管經給多少次分配/釋放操作后，已分配的和空閑的內存塊之和應是整個內存池的大小。

3.2.2　功能正確性規約

功能正確性是內存管理分配/釋放操作必須完成的基本功能，其通過霍爾邏輯中的霍爾三元組表示，符號形式為{P}c{Q}，其中P和Q是一階邏輯公式，分別表示前置條件和后置條件。霍爾三元組的含義為：P有效的情況下執行程序c后，Q有效。本文依據霍爾邏輯，采用霍爾三元組表示功能正確性，針對功能正確性提取的主要屬性如下：

（1）分配的內存塊如果大于請求的內存塊，且大于最小內存塊，需對內存塊進行切割；切割后的內存塊一塊提供給用戶使用，一塊進入到空閑內存塊進行管理；

（2）分配的內存塊如果大于請求的內存塊，且小于最小內存塊，不需考慮切割，直接提供給用戶使用；

（3）已經被分配的內存空間是可以被釋放的；

（4）經給釋放操作后，需進行合并操作，即不能有兩個相鄰的空閑塊。

3.3　狀態機模型

本文使用狀態機來描述內存管理模型，也為后續建立形式模型提供了基礎。將內存管理系統的運行視為狀態機的執行，狀態機的組成要素包括狀態和事件：狀態記錄了系統的變量值；事件描述實際系統的操作，每個事件對應一個狀態的遷移。

狀態機模型定義為M=<S，φ，S0>，其中需包含確定模型的要素（操作函數）、狀態：

S表示所以狀態的集合。

φ表示狀態轉移函數，φ(e)∈S×S，表示系統中 一個狀態下執行單個事件后到達一個新的狀態；

S0表示系統的初始態，S0∈S。

基于狀態機定義構建內存管理的狀態機模型，內存管理的事件操作只有分配和釋放操作，且整個內存池按系統配置{start│end}初始化后，根據長度end-start形成一個用戶最大可用的空閑內存塊。整個系統的狀態機模型可以抽象為對整個內存池的狀態空間進行描述，而內存池的狀態機空間是由一個個的內存塊組成。

內存塊對象模型可抽象描述如圖6所示，baseAddress為內存塊的起始地址，對應的是真實物理地址；size為內存塊本身大小屬性，用以描述內存塊的大小，均為自然數類型。一個內存塊狀態就只有兩種，一種是已使用狀態，一種是空閑狀態，是在被分配之后其狀態就為已使用狀態，被釋放后為空閑狀態。

圖6內存塊對象形式化描述

用戶經過一系列的分配/釋放操作后，整個內存池的系統狀態如圖7所示，可抽象描述為由一系列已使用的內存塊和空閑內存塊構成。

圖7內存池狀態描述

3.4　形式化建模

基于內存管理狀態機模型的基本抽象描述，以及三級內存管理數據結構的設計描述，對內存管理基本數據結構和內存池狀態進行擴充，并基于基本數據和狀態模型進行分配和釋放操作行為的構造。

3.4.1　構造基本數據結構

內存管理基本數據結構的設計模型如圖8所示，pre_size是指物理空間中的前塊大小，size是指物理空間中的本塊大小，next是指指向下一個內存塊的指針，previous是指指向前一個內存塊的指針。

圖8內存塊對象設計描述

通過嵌入式操作系統內存管理的數據結構，基于圖6內存塊基本抽象模型，把整個內存地址抽象為自然數的一個連續的空間，基本數據類型是nat類型。通過baseAddress確定實際物理地址，pre_size和size與圖6對象設計描述中的屬性描述一致。內存塊對象形式化描述如下：

record block_t=

baseAddress:: nat

pre_size::nat

size::nat

status::block_status

還需要一個狀態用來標志內存塊的狀態，即空閑還是已使用，類型如下：

block_status=Idle|Used

3.4.2　構造系統狀態

整個內存空間的狀態如圖7所示，是由一系列使用塊和空閑塊組成，并通過位圖的形式來快速定位三級空閑內存塊的索引號。位圖的設計模型如圖9所示，用數組Map來表示對應的index，其中1表示對應的index上有空閑塊，0表示對應的index上沒有空閑塊。在形式化中將位圖抽象成bool list的形式，True表示對應的index上有空閑塊，False表示對應的index上沒有空閑塊。

圖9空閑內存塊的位圖

三級空閑內存管理中index下面的空閑內存塊都是通過雙向鏈表來進行管理的，即某個index下面都掛了指定大小的空閑內存塊。例如圖10所示，index為4的下面掛著長度為32的空閑塊，第1和第2個元素表示pre_size和size，第3和第4個元素表示后向指針和前向指針。

圖10空閑內存塊鏈表示意圖

故針對空閑內存塊的鏈表管理抽象成list list，用來表示某個對應index下面的空閑內存塊。由于整個內存池的系統狀態由一系列的已使用塊、空閑塊和位圖組成，故而內存池的系統狀態形式化描述如下：

record State_t=

used_block_list∶:"block_t list"

idle_block_matrix∶:"(block_t list) list"

Bitmap::bool list

3.4.3　構造初始化模型

根據系統配置的兩個參數，一個是起始地址，一個是結束地址，獲得用戶配置的空間長度size。通過InsertBlockToList將整個內存塊掛接到對應index的空閑鏈表上，同時將Bitmap位圖置為1，表示對應的索引上有空閑塊，系統內存池狀態為S0。

S0::nat?nat?State_t

S0startend=

block=(|baseAddress=start,size=end start,status=Idle,pre_size=0|)

S'=(|idel_block_matrix=replicate 320[],used_ block_list=[],Bitmap=bitmap_list|)

InsertBlockToList S' block

表2內存管理形式化建模內部接口

3.4.4　構造內存分配模型

內存管理的分配malloc給用戶返回一個內存塊的指針，即具體算法邏輯通過下列操作執行：

（1）當輸入分配請求的大小req_size是0時，返回錯誤EINVAL；

（2）否則，將req_size按照進行8字節對齊bsize_up_align，然后再按照三級內存管理進行調整AjustSize，即如果在第一級范圍內，進行8字節對齊，如果在第二級范圍內進行64對齊，如果在第三級范圍內進行1024對齊；

（3）依據調整后的大小獲取HeadIndex，且過程中考慮MinBlk，設計階段進行實例化，即MinBlk=BLOCK_MIN_SIZE+BLOCK_MEM_HEAD；

（4）依據HeadIndex在空閑內存塊中查找合適的且有效的mallocIndex；如果找不到則返回錯誤碼ENOSPC；

（5）否則內存池系統狀態中有大于請求分配的大小的空閑塊時，則進行分配并獲取返回的地址GetMemByHeadIndex，且應考慮分割的情況。如果有效的mallocIndex=320，并按照first-fit去查找find_suitable_free_block內存塊大小，否則取此列表下的第一個塊去進行分配。針對分配的需求建模形式化描述定義如下：

malloc::State_t?nat?(State_t ×nat)

malloc state req_size=if req_size =0 then err_no =EINVAL

else let

adjust_size=AdjustSize(bsize_up_align req_ size+MinBlk) ;

mallocIndex=Convert2ValidHeadIndex (HeadIndex (adjustSize)) in

if mallocIndex =None then err_no =ENOSPC

else if mallocIndex=320 then find_suitable_free_ block

else hd (idle_block_matrix state)!mallocIndex

表3內存管理形式化建模內部接口

3.4.5　構造內存釋放模型

內存管理的釋放free將用戶申請的一段內存釋放到空閑空間中，即具體算法邏輯通過下列操作執行：

（1）如果請求釋放的地址addr在已使用塊中不存在，則返回錯誤；否則

（2）通過addr找到find_prev_block前一個內存塊prev_block和find_next_block后一個內存塊next_block；

（3）如果前塊狀態空閑，后塊狀態使用，則與前塊合并形成大塊后插入到空閑內存塊中；

（4）如果前塊狀態使用，后塊狀態空閑，則與后塊合并形成大塊后插入到空閑內存塊中；

（5）如果前塊狀態空閑，后塊狀態也是空閑，則與前后塊合并形成大塊后插入到空閑內存塊中；

（6）否則僅將本塊插入到空閑內存塊中。

free::State_t?nat?State_t

free state addr=

block=find λ.addr (used_block_list state)

if block =None then err_no =EINVAL else

prev_block =find_prev_block state block

next_block =find_next_block state block

if prev_block.status =Idle? next_block.status =Used then InsertBlockToList status merge_prev_block else if prev_block.status =Used ? next_block.status =Idle then InsertBlockToList status merge_next_block else if prev_block.status =Idle ? next_block.status=Idle then merge_prev_next_block then InsertBlockToList status merge_prev_next_block

else InsertBlockToList status block

表4內存管理形式化建模內部接口

3.5　形式化驗證

形式化驗證主要是依據提取的正確性和確定性方面的形式規約在Isabelle工具中進行形式化轉換，并依據形式模型，對提取的確定性和正確性屬性分別進行證明。由于不變式是在任何狀態下均成立的，而功能正確性是狀態前后的整理，故而證明順序首先需證明不變式的成立，其次是功能正確性的證明。依據提取的確定性方面提取的6條不變式，形式化描述分別如下：

（1）已分配的和空閑的內存塊之和應是整個內存池的大小；

∑b∈(set(used_block_list)∪set(idle_block_matrix s !i)|i.i∈{idx..n}.size b=end-start

（2）不能有兩個相鄰的空閑塊；

b∈idle_block_set.baseAddress b+size b≠b'∈idle_ block_set.baseAddress b'

（3）一個內存塊的狀態是互斥的，即在空閑塊中，就不能在使用塊中；

(block∈ used_block_list.status block=Used)?(block∈ idle_block_matrix.status block=idle)

（4）任何兩個內存塊的地址不能重合；

(u i.u∈ used_block_list∪idle_block_matrix→i∈ used_ block_list∪idle_block_matrix→?block_overlap u i

（5）經過分配/釋放操作的空閑內存塊大小應在指定的三級范圍內；

(block∈set(idle_block_matrix s ).blk∈set(blocks. status blk=Idle→size blk∈{min..max}

（6）位圖中的每個True值對應的空閑塊列表為非空；

(i.(bitmap s)!i =True→(idle_block_matrix s)! i≠[]

以malloc函數為例，功能正確性按照霍爾三元組{P}c{Q}引理如下：

{find(λ v.size v≥req_size)(idle_block_ matrix s)}malloc state req_size{v∈used_block_ list s')}

在形式化驗證過程中，我們發現了兩個主要軟件缺陷，并通過實際測試進行了確認：

（1）每次已分配的和空閑的內存塊之和沒有等于整個內存池的大小，而是每次損失一個內存頭的空間；

（2）獲取到最大空閑內存塊后，按照最大的size進行分配，分配不成功。

4　結束語

本文將形式化方法引入到核電操作系統中，提出了形式化建模和驗證整體框架，并以核電某嵌入式操作系統內存管理設計層面算法為案例進行了研究。該研究考慮了復雜的數據結構，建立了狀態機模型，構建了內存管理的所有操作，并在Isabelle工具中建立了形式模型，形式化了功能正確性、確定性的相關屬性的研究。

基于形式模型，需針對提取的所有屬性在Isabelle工具中進行形式化驗證，避免這些問題遺留到工程應用中。在未來后續工作中，需將提取的所有屬性進行一一驗證，并考慮需求、設計等各個階段模型精化和增量證明的工作，繼續將形式化方法的研究工作進行完善，以有效提高嵌入式操作系統軟件的質量。

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

作者簡介：

李幼媛（1983-），女，河南人，高級工程師，碩士，現就職于北京廣利核系統工程有限公司，主要從事核安全級數字化儀控系統測試與驗證的工作。

參考文獻：

[1] HAD 102/10-2021, 核動力廠儀表和控制系統設計[S].

[2] IEC61513:2001, Nuclear Power Plants –Instrumentation and Control for Systems Important to Safety –General requirements for Systems[S].

[3] IEC60880:2006, Nuclear Power Plants -Instrumentation and Control Important for Safety-Software Aspects for Computer-Based Systems Performing Category A Functions[S].

[4] IEC62138:2018, Nuclear Power Plants -Instrumentation and Control Important for Safety -Software Aspects for Computer-Based Systems Performing Category B or C Functions[S].

[5] IEEE Std 1012TM-2016, IEEE Standard for System, Software, and Hardware Verification and Validation[S].

[6] POSIX.1-2017/IEEE Std 1003.1-2017 IEEE Standard for Information Technology-Portable Operating System Interface (POSIX?), IEEE Computer Society and The Open Group, 2017.

[7] 章樂平, 趙永望, 王布陽, 等. L4虛擬內存子系統的形式化驗證[J]. 軟件學報, 2023, 34.

[8] Klein G, Elphinstone K, Heiser G, et al. seL4: Formal verification of an OS kernel[C]. In: Proc. of ACM SIGOPS the 22nd Symp. on Operating Systems Principles. ACM, 2009, 207 - 220.

[9] research and Application of Memory Space Deterministic Verification of Embedded Operating System Software in Nuclear Safety Level Instrument and Control System.

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