文献标识码：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月刊