在高温气冷堆核电站(high temperature gas-cooled reactor, HTGR)数字化主控室中，计算机化运行规程系统是操纵员运行辅助支持系统的重要组成部分^[1]。目前，国内二代改进型^[2]和三代压水堆核电站^[3]都配置了计算机化运行规程。国家科技重大专项华能石岛湾核电厂高温气冷堆核电站示范工程(high temperature reactor-pebble-bed modules, HTR-PM)的数字化仪控系统也为计算机化运行规程预留了接口。计算机化运行规程系统将规程以流程图^[4]的形式显示在计算机屏幕上，由2部分组成：执行规程的软件系统和计算机化的规程。计算机化的规程由软件系统进行加载，并按照预定义的流程和逻辑被执行^[5]。规程流程需要在制定计算机化运行规程时预定义，且必须正确可靠。如果规程的执行流程存在错误，就可能导致操纵员的操作错误，从而影响到核电站的运行安全。因此，为保证规程操作步骤流程无误，对计算机化规程流程进行建模和验证十分必要^[6]。

当前，对计算机化规程流程建模和验证的研究不多，这主要因为目前配置的计算机化规程大都采用产生式规则形式，这种形式的规程各个规则之间相对独立，不能有效反映相互之间的联系，不便于规程流程的建模和验证。Jung等^[7]用成功逻辑树的方法研究设计了一种电站操作规程的模型，但是，这个模型只涉及到计算机化运行规程的执行和显示，并没有包括规程执行的形式化验证。

高温气冷堆核电站具有“多个核蒸汽供应系统模块带一台汽轮机”的结构和运行特点，在其运行过程中，存在多种不同的运行工况，其规程的执行不仅有顺序流程，还会存在中断执行等流程。本文针对此特点，进行基于改进着色Petri网的计算机化规程流程的建模和验证，为高温气冷堆核电站计算机化运行规程系统的研制打下基础。

1 高温气冷堆核电站计算机化规程的特点

高温气冷堆核电站的计算机化规程是多级结构，其结构层次包括规程、步骤、指令和诊断逻辑。步骤和指令是高温气冷堆核电站计算机化规程的主要单元，一项规程包含多个步骤，每个步骤含有若干个指令。规程的执行流程即为步骤和指令的完成流程。其中，指令包括单态和双态2种类型：单态指令只有一种流向，双态指令有两种流向。指令的诊断逻辑包括手动诊断和自动诊断2种，手动诊断需要操纵员输入诊断结果，自动诊断是系统通过参数或状态监测自动判断诊断结果。每种指令的诊断结果和类型都会影响指令的执行流程。

以高温气冷堆核电站氦风机误加速异常事件处理规程为例，该规程包括以下步骤^[8]：

步骤1  降低并调整主氦风机转速；

步骤2  向值长报告并详细记录异常事件的现象、参数和恢复操作过程；

步骤3  查找造成主氦风机误加速的原因并排除故障，判断是否能在6 h内排除故障；

步骤4  按照“保护信号处理程序”进行处理；

步骤5  若在6 h内不能排除故障，则报告值长并同时停堆。

其中步骤1的指令为降低主氦风机转速，步骤2的指令为报告值长和记录现象、参数、恢复操作过程，步骤3的指令包括查找原因、判断6 h内是否能排除故障，步骤4的指令包括保护停堆后各处理程序，步骤5的指令包括不能排除故障时上报值长、停堆。规程的执行流程如图 1所示。当规程开始执行时，规程的步骤1中的第一个指令开始被执行。在常规流程中，当该步骤中的所有指令完成时，该步骤执行结束，然后进入到下一步骤。当规程的最后一个步骤执行完成时，规程执行完成。

模块式高温气冷堆核电站具有“多堆带一机”的结构和运行特点^[9]，每个操纵员需要监控操纵不止一个反应堆模块，每个反应堆规程的执行可能存在中断。这是因为多模块高温气冷堆核电站在运行过程中，不同的反应堆模块可能面临不同的操作。比如当一个反应堆正在执行升功率操作时，另一个反应堆出现异常情况需要处理，此时执行升功率操作的反应堆需要暂停操作，待操纵员对另一个反应堆的异常情况处理以后，再重新开始升功率操作。

因此，规程的执行除了顺序流程外，还会有存在中断的执行流程，比如置后执行、重新执行、变序执行，如图 2所示，图中Y代表已完成的步骤，Z代表正在执行的步骤，W代表未开始执行的步骤。操纵员可以在当前步骤完成之前开始下一步骤。也就是说，操纵员可以推迟当前步骤的完成，而开始进行下一步骤。被推迟的步骤仍在被执行。这就意味着操纵员在同时执行推迟的步骤和下一步骤。而且，已完成的步骤可以在需要的时候由操纵员重新执行，根据重新执行的结果，规程流程可以进行改变。此外，通过改变流程，操纵员可以开始执行任意一个未开始的步骤。根据事先预定义的流程及对流程起决定作用的核电站状态信息，确定了一个规程的执行流程，规程的执行流程可以由操纵员或系统改变。规程执行流程的正确与否直接影响到反应堆的运行状态安全，因此在对规程进行计算机化时，执行流程的验证是必需的。

在这种存在中断的规程执行流程中，每一个步骤都存在3种状态，即“待执行”“执行中”和“已完成”，建模时需对这3种状态进行合理有效表示。

2 改进着色Petri网

着色Petri网(colored Petri nets，CPN)是一种形式化和图形化的系统建模语言^[10]。用传统Petri网对复杂系统进行建模时，Petri网模型的节点很多，规模非常庞大。针对这个问题，着色Petri网被提出，它在Petri网模型^[11]的基础上，添加了颜色集、颜色函数、弧表达式函数和守护函数等元素^[12]，其主要思想是将托肯(Token)赋予颜色标记，以区分不同种类的托肯^[13]。一般的着色Petri网如图 3所示^[14]。

着色Petri网可以对高温气冷堆核电站计算机化的运行规程进行建模，用以表述规程步骤的不同执行状态。但对于变体规程流程模型，需要增加大量附加的变迁和连接弧，使得模型变得复杂而庞大。

针对着色Petri网建模的不足，为了减少附加的变迁和连接弧，对着色Petri网进行改进，用一个状态器进行托肯的动态着色。在改进着色Petri网中，托肯的状态可以由状态器进行建模。因此，托肯的颜色是动态的而非静态的，库所不用附加额外的变迁就能够有多种状态。这样，系统就可以用2种独立的方式进行建模：基于Petri网的库所变迁模型和托肯的状态器模型。

改进着色Petri网有如下特点：托肯有状态，状态的形式为颜色的设置；托肯的状态以状态器的形式表现和转换；在守护函数的约束条件下变迁可以被点火；状态器中的一个事件的发生可以改变另一个托肯的状态；整个模型的一部分被建模为托肯状态；托肯的状态变迁相对于库所的变迁是独立的；托肯的状态变迁能对有中断的工作流程进行建模。

在改进着色Petri网中，托肯有一个状态器，托肯当前的颜色就是状态器当前的状态。基于改进着色Petri网模型及托肯与网之间的关系如图 4所示。变迁B存在守护条件，只有当Token B为状态4时变迁B才能够被触发。当Token A的状态从状态1变为状态2时，事件B生成，事件B的生成进而会使Token B的状态发生改变。这就意味着，当第一个Petri网中有一个事件A，那么第二个Petri网的变迁便会被触发。

改进着色Petri网中的托肯状态器是动态的，可以用于整个系统的库所。如果一个库所有托肯，那么这个库所就有一个可以动态设置的状态标志。有中断的规程执行流程中存在动态状态标志。根据高温气冷堆核电站的状态，操纵员可以对正在执行的规程进行中断，当中断结束时，根据需要可以回到中断之前的状态。

3 基于改进着色Petri网的计算机化规程流程建模

用改进着色Petri网对高温气冷堆核电站计算机化的规程进行建模时，规程的步骤、指令以及步骤指令的操作被建模为普通的着色Petri网，步骤的状态被建模为托肯的状态器。

以双模块高温气冷堆核电站为例，有多个NSSS模块的高温气冷堆核电站与此类似。假设1#核蒸汽供应系统模块(1#NSSS)正常功率运行，2#NSSS正在正常启动过程中。当2#NSSS执行到步骤5时，处于反应堆升功率的过程中时，1#NSSS发生二回路给水管道破口异常事件，则1#NSSS转入异常处理规程，而2#NSSS暂停步骤5，待1#NSSS异常处理规程结束后，2#NSSS重新开始步骤5。表 1为二回路给水管道破口异常处理规程的主要步骤^[8], 表 2为2#NSSS正常启动规程的主要步骤^[15]。

表 1中备用流程在相应期望流程条件不满足时应用。步骤1有一个入口条件，当条件符合时该步骤的指令被执行。当发生二回路给水管道破口异常事件时，操纵员需要确认保护停堆触发。如果此时保护停堆没有触发，操纵员必须进入备用流程，手动触发“紧急停堆”按钮。步骤2是一个常规步骤，监督并操作所有的子指令。步骤3可操作任意一项子指令。在任何时候，操纵员都能够推迟当前步骤，开始下一步骤。此外，操纵员可以重新执行已完成的步骤。

表 1和2规程中的每一个步骤都有3种状态：“待执行”“执行中”和“已完成”。最初，所有步骤的第一个库所的托肯都是“待执行”状态。当一项规程开始时，第一个步骤的托肯状态变为“执行中”，并且其变迁被触发。当操纵员完成了所有的指令，托肯到达标志该步骤完成的库所。当操纵员完成一个步骤，托肯的状态从“执行中”变为“已完成”，并且下一步骤的托肯状态从“待执行”变为“执行中”。这意味着每个完成的步骤都有一个状态为“已完成”的托肯。操纵员可以根据需要重新执行已经完成的步骤，此时托肯的状态由“已完成”变为“执行中”，并转移到该步骤的顶端。对于“执行中”的步骤，操纵员可以对其进行置后操作，随后，该步骤的下一步的托肯状态会由“待执行”变为“执行中”。

在用改进着色Petri网对其建模时，步骤状态的改变由状态器来完成，图 5为基于改进着色Petri网的二回路给水管道破口异常事件处理规程的模型。图 6为基于改进着色Petri网的正常启动规程主要步骤的模型。

在模型图中，SiS为第i个步骤的开始库所，SiIj为第i个步骤的第j个指令库所，SiC为第i个步骤的完成库所，Tij为第i个步骤的第j个变迁。

当2#NSSS执行到步骤5时，由于1#NSSS发生二回路给水管道破口异常事件，2#NSSS需置后步骤5的执行，等待1#NSSS异常处理规程结束后，2#NSSS重新执行步骤5。这个过程中，2#NSSS正常启动规程步骤5的置后执行和重新执行都由状态器来进行状态的标记和转换。

从模型图中可以看出，改进着色Petri网将复杂的计算机化规程操作步骤转变为2个简单的部分，如果要对规程的操作步骤进行“置后执行”“重新执行”等操作，不需要增加额外的变迁，这些变体流程所需的状态改变和步骤转移由状态器完成。这种建模方式使得Petri网的结构更加简单，将计算机化的规程模型和状态模型分离开来，更加便于规程结构的维护，也更易于规程执行流程的理解和验证。

4 计算机化规程执行的形式验证

基于模型的可达性分析^[16]，能够对计算机化规程执行进行形式化验证。Petri网能够计算出规程模型所有的可达状态，并以有向图的方式表示。计算机化规程执行的形式验证，需要验证其每一个步骤和指令都有有效的执行途径，不能存在任何步骤或指令无法被执行；同时还需要验证，在没有操纵员进行中断的正常顺序规程中，规程的所有步骤都与其他步骤相通；对于有操纵员中断的计算机化规程，其状态空间会根据托肯的状态而进行扩展。以高温气冷堆核电站异常事件处理规程中二回路给水管道破口异常事件处理规程为例，规程的前2个步骤用改进着色Petri网进行建模，并在步骤1中加入“置后执行”“重新执行”和“变序执行”操作，如图 7所示。图 8为构建模型的可达标识图。

从规程模型的可达标识图可以看出，二回路给水管道破口异常事件处理规程中的每一个步骤和指令都有有效的执行途径，不存在任何步骤或指令无法被执行。因此，说明此规程的执行经过形式验证是正确的。

5 结论

用改进着色Petri网建模方法建立了高温气冷堆核电站正常规程执行模型和存在中断的变体规程执行模型，能够将变体规程中复杂的中断模型与正常流程模型分开来，使得变体规程模型的结构更加简单，也简化了验证。基于规程执行流程模型，利用Petri网可达性分析。

限于篇幅，本文以双模块高温气冷堆核电站为例，其中1#核蒸汽供应系统模块(1#NSSS)正常功率运行，2#NSSS在正常启动过程中，1#NSSS发生二回路给水管道破口异常事件。该处理过程涉及到正常启动规程和二回路给水管道破口异常处理规程，2种规程皆为正常运行规程和异常处理规程的典型规程。用该处理过程进行计算机化规程流程的建模和形式化验证，具有典型性和代表性，说明了使用基于改进着色Petri网进行高温气冷堆核电站计算机化规程建模和验证的有效性。