★北京广利核系统工程有限公司李幼媛，张亚栋，武方杰，杜乔瑞，首云旭，孙王强，洪鑫哲

关键词：核电嵌入式操作系统；形式化建模；内存管理；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月刊