Modeling of computerized procedure execution with State Token Petri Net for formal verification of procedure flow

Abstract

Computerized procedure system (CPS) is one of the primary operating support systems in the digital main control room (MCR) of a nuclear power plant. CPS displays the procedure at computer screen in the form of a flow chart and displays plant operating information along with procedure instructions. It also supports the operator to make a decision by providing system decision with logic. Most importantly, CPS guides the operator to follow a procedure flow that is predefined when the computerized procedure (CP) is written. A procedure flow should be correct and reliable, as error would lead to operator misjudgment and inadequate control. As such, the procedure flow should be verified before being applied to the MCR. In this article, we present a model of CPS that enables formal verification based on Petri nets. The proposed State Token Petri Net also supports modeling of a procedure flow that has various interruptions by the operator according to the plant condition.

Keywords :

• computerized procedure system
• digital MCR
• operator supporting system
• workflow management
• Colored Petri net
• formal verification
• digital quality assurance

1. Introduction

An advanced feature of a digital main control room (MCR) of a nuclear power plant is that there are various digital systems for display, monitoring, and control to support operator situation awareness and decision making. One of the main operating support systems is computerized procedure system (CPS). CPS has been accepted by regulatory bodies of different countries and have been applied to several nuclear power plants including APR1400 (Advanced Power Reactor 1400) in Korea. CPS provides integrated operating means such as a procedure and plant information [1–4]. CPS guides the operator to follow a procedure flow and CPS monitors plant status required for procedure execution. Figure 1 shows an example of APR1400 CPS display. CPS is applied not only to normal operating procedures needed for general operation, but also emergency operating procedures needed for accident mitigation, safe shutdown, and emergency response. The functionality of CPS is increasing along with digital technologies and as experience is accumulated.

Figure 1. CPS display for emergency operating procedure.

Procedure based automation (PBA) is an example of high functionality of CPS. In PBA, CPS automatically processes a series of actions including control of plant equipment. One essential requirement of CPS for PBA is digital system quality assurance including verification and validation. However, there are many procedures in a nuclear power plant, and they can be revised during the life-time of the plant. For the management of procedures, CPS consists of two parts, software that executes procedures and the procedures themselves (computerized procedures (CP)). A CP is loaded to CPS and executed with predefined execution flows and logics. CPS software is needed to be verified and validated when CPS is developed and provided to the plant. However, the CP cannot be included in the verification and validation (V&V) of CPS, because the CP itself will be revised and a new CP will be added as needed. The CP includes the execution flow of procedures that guides the operator, and if there is an error in the execution flow of procedures, it could affect the safety of the nuclear power plant (NPP) operation. Therefore, the CP must be verified and validated not only with respect to the software, but also with respect to the procedures of the plant.

Design guidelines for CPS in human factor engineering are addressed by NUREG-0800 (Chapter 18), NUREG-0700, and NUREG-0711, but they do not address the detail V&V of a CP as a digital system quality assurance. The V&V of previously paper-based emergency operating procedures (EOP) has been required at NUREG 0899, “Guidelines for the Preparation of Emergency Operating Procedures.” In this guideline, the V&V of EOP is required to establish the accuracy of information and/or instructions, to determine that the procedures can be accurately and efficiently carried out, and to demonstrate that the procedures are adequate to mitigate transients and accidents. When CPS is applied, the V&V for accuracy of instruction and procedure process is more severely required, because CPS guide the procedure process and evaluate instruction automatically. NUREG 0899 also, presents several V&V methods which are simulator validation, control room walk-through, desk top review and computer modeling/analysis. NUREG 6634 by John M. O'Hara [5] have established human factors review guidance for CPS and V&V of a CP have been required as procedure development activity. Recently, EPRI Guidelines (2010) address guidelines for design and implementation of CPS. It also addresses that digital system QA and V&V should be emphasized when CPS is applied to procedures for risk-significant tasks such as EOPs. Therefore, V&V of a CP is needed when the operator writes a procedure. Also, V&V of emergency operating procedures is required by the regulatory body and the V&V should include structural completeness that ensures there are no process flow errors.

CPS is a kind of workflow system. Modeling and analysis of workflow systems started in the 1970s with factory automation. Various studies on workflow management systems (WfMS) have been conducted and many formal modeling languages are applied to WfMS for verification. Petri net is one of effective modeling tool for WfMS and have been extensively studied by several researchers [6–9]. K. Salimifard and M. Wright [10] explained a general methodology to map workflow into Petri nets and summarized researches that concentrated on Petri net-based modeling of workflow. W.M.P. van der Aalst have proposed YAWL that is one of the leading studies for workflow verification based on Petri nets modeling. Aalst has defined a direct and intuitive workflow pattern with Petri nets and proposed multiple instances for handling work flow patterns. A CP has both characteristics of software and workflow. A CP also has multiple instances that have dynamic relations required by the operator. Once the CP is modeled with formal language, formal verification such as structural analysis can be applied to the CP.

2. Modeling of computerized procedure execution for verification.

2.1. Characteristic of computerized procedure

CPS in APR1400 consists of a multi-hierarchical structure entailing procedure, step, instruction, and evaluation logic. Execution of a procedure is determined by the main unit of the procedure: a step and an instruction. A procedure is executed according to the flow of steps and each step is completed according to instructions in that step. There are two types of instructions, unitary instruction that has one way of flow, and binary instruction that has two ways of flow. Also, the evaluation logic for instructions consists of manual evaluation, where the operator inputs the evaluation result, and auto evaluation, where the system determines the evaluation result. Each evaluation result and type of instruction affects the execution flow of an instruction. Y. Jung et al. [11] have developed a model for plant operating procedure with flowchart and success logic tree. However, the modeling deals with only execution and display of CPS that do not cover the verification of the execution of procedure. Simplified normal procedure execution flow is shown in Figure 2 . When the procedure is started, the first step and first instruction of that step start. In normal flow, a step is completed when the completion of an instruction in the step is connected to the other step. When a step is completed, the next step is started. When the step that is linked to the end of procedure is completed, then the procedure is completed. However, there are alternative flows such as “postpone,” “re-execute,” and “change flow” as depicted in Figure 3 . An operator can start next step before a current step is completed. In other word, an operator can postpone the completion of a current step and start next step. The postponed step is still being executed. It means that operator execute the postponed step and next step simultaneously. Moreover, a completed step can be re-executed when requested by the operator, and the procedure flow can be changed according to the result of re-execution. In addition, an operator can start any step that is not started by “change flow.” As explained, a procedure has execution flow according to the predefined process flow and plant information that is used to determine the process. Therefore, the execution flow of a procedure is changed by the operator or system, and V&V of the execution flow are needed when the procedure is being written.

Figure 2. Procedure execution flow.

Figure 3. Alternative procedure flows.

2.2. Modeling of CP with Colored Petri net

Colored Petri net is one of formal and graphical language for modeling system. Many computer tools for Colored Petri net were proposed by Kurt Jensen [12] and Kurt Jensen et al. [13]. Colored Petri net combines the strengths of ordinary Petri net with the strengths of a high-level programming language. Colored Petri net also has a formal and mathematical representation with a well-defined syntax and semantics. It is possible to formulate a standard request for verification properties such as reachability, deadlock, and liveness as well as user defined requests using modeling language. The main characteristic of Colored Petri net is that tokens have a color set, making it possible to carry data with a token. Ordinary Colored Petri net is shown in Figure 4 .

Figure 4. Colored Petri net.

In modeling of CPS with Colored Petri net steps and instructions of a computerized procedure are modeled as places and the processes of steps and instructions are modeled as transitions. The processes of a procedure are controlled by tokens. Colored Petri net modeling for procedure execution flow is depicted in Figure 5 . When the step is started, the token is transited to the instruction 1. When the evaluation of the instruction is “YES” then the token is transited to the instruction 2. When the evaluation of the instruction 1 is “NO” then the token is transited to the instruction 3. Colored Petri net can model the normal process of the procedure as explained. However, when the operator postpones the completion of the current step at the instruction 1 of the step 1, then the step 2 should be started. It means that the token from the instruction 1 of the step 1 should be transited to the step 2 and one additional token should be left in the instruction of the step 1. When a postponed step is completed, the token should not be transited to the next step, because the next step started already. Moreover, the operator can postpone at any instruction. There are three additional transitions for postpone and one additional place and transition for completion. Generally, the required number of transitions for postpone is the sum of the number of instruction for token transfer and one for postponed step completion.

Figure 5. Colored Petri net modeling for normal procedure execution flow.

In the same manner “re-execution” and “change flow” can be modeled by Colored Petri net as depicted in Figure 6 . When an operator changes procedure flow, then the token at current instruction should be transited to the first instruction of the changed step. When an operator re-executes already completed step, then the token at current instruction from current step should be transited to the first instruction of the re-executed step. For these alternative procedure flows modeling, the additional transition and place is needed. Table 1 identifies the required number of transition, arc and place for alternative procedure flow. The additional transitions and places make the modeling complicated and it is hard to understand normal flow when there are additional transitions and places.

Figure 6. Colored Petri net modeling for alternative procedure flows.

Table 1. Required numbers of transitions, arcs and places for ordinary Colored Petri net modeling.

	Number of transition (Ntr)	Number of arc (Na)	Number of place (Np)
Postpone			–
Change procedure flow			–
Re-execution			–
Step completion of alternative flow (NOTE1)
Notes: NOTE1: Additional place for the step completion is needed because the next step already started. NIi, Number of instructions in step I; NS, Number of steps in procedure.

2.3. Definition of State Token Petri Net (STPN)

State Token Petri Net (STPN) is an extended Colored Petri net. STPN uses a state machine for the dynamic color of a token. In STPN, a token has states that can be modeled by the state machine. This means that a token has dynamics instead of static color. The state of the token makes it possible that a place can have many states without any transition. Hence, the dynamics of the system can be modeled in two independent ways: transition of place in the Petri net model and the state machine of the token.

The characteristics of STPN are as follows.

•	A token has states in the form of a color set.
•	Token states act like a state machine.
•	Transition can be fired under guard condition.
•	An event in state machine can change another token state.
•	A part of the total model can be modeled as a token state.
•	The state transition of a token is independent of the transition of place.
•	State transition of a token is adequate to model an interruption of the work flow.

In STPN token has a state machine and the current color of token is the current state of the state machine. STPN modeling and the example of relation between token and transition is depicted in Figure 7 . Transition B has guard condition and it fires only when the state of token B is state 4. The state of token B is changed when there is an event B and the event B is generated when the state of token A is changed from state 1 to state 2. This means that when there is an event A in the first Petri net, the transition in second Petri net is fired. Therefore, STPN can model, respectively, for the normal process and the alternative flow caused by event. STPN simplifies the normal process part of the model and makes it easier to understand. Also, the state machine of token in STPN is a simpler modeling language as compared to Colored Petri net. Hence, the simple part of the total model can be modeled as a state token, thereby making total modeling simpler than with an ordinary Colored Petri net.

Figure 7. STPN modeling and the example of relation between token state machine and Petri net.

STPN is expected to be useful in the following cases of modeling.

2.3.1. System with interruption

A token in STPN carries dynamics that can apply to the entire place of the system. In other words, if a place has a token, then the place also has a dynamic set of states that is modeled in the token. One familiar example of this dynamics is an interruption. The user can interrupt the execution independently with the state of the system, and when the interruption is over, the system should return to the state before being interrupted. The state of the token can be modeled as an interruption. Then, every place that has a token can be interrupted and, moreover, the interruption can be transferred along with Petri net depends on the type of interruption.

2.3.2. System with multi-dynamics

More than one token can carry dynamics. A Petri net was originally used for concurrent system modeling; however, STPN can be used for multi dynamic systems that have concurrent execution flows in the Petri net and another independent dynamic system as state machines in a token.

2.4. Modeling of computerized procedure with State Token Petri Net

CPS is modeled with STPN. Steps, instructions and the processes of a procedure are modeled as ordinary Petri nets. However, the state of a step is modeled as the state of the token, as described in section 2. Every step in the computerized procedure has one of three states: “Before Execution,” “Under Execution,” and “Completed.” Initially, the first place of all steps has a token with a state of “Before Execution.” When a procedure is started, the state of token of first step is changed to “Under Execution” and the transition can be fired. When the operator finishes all instructions, the token arrives at the place named completable. When the operator completes the step, the state of the token changes from “Under execution” to “Completed” and the event is generated that changes the state of token in next step from “Before Execution” to “Under Execution.” This means that every completed step has a token with a state of “Completed.” The completed step can be re-executed when requested by the operator. The state of the token changes from “Completed” to “Under Execution” and it transits to the first place of the step. During the “Under execution” the operator can postpone the completion of current step. The event is generated that changes the state of token in the next step from “Before Execution” to “Under Execution.”

An emergency operating procedures (EOP) is used when there is an accident at a nuclear power plant. The purpose of an EOP is to mitigate the accident and to make the plant safe and stable. The EOP should be performed quickly and accurately, and thus there should be no error in the flow of procedure in the EOP. Table 2 shows the three major types of steps in an EOP. There are two columns, one is for expected flow and the other is for the contingency flow that is performed when expected flow cannot be applied. Step 1 has an entry condition, and instructions that are executed when the condition is met. When the pressurizer pressure is less than the set point, the operator must verify that safety injection actuation system (SIAS) is actuated. If SIAS is not actuated under this condition, the operator must proceed to contingency flow and manually actuate SIAS. Step 2 is an ordinary step that checks all of the child instructions and Step 3 checks any one of the child instructions. At anytime, the operator can postpone the current step and start the next step. For example, when the operator executes Step 1, he/she can start step 2 before step 1 is completed. Moreover, the operator can execute again a step that is already completed. Therefore, the CP has two types of dynamics, one is the flow of the process and the other is the operator's work flow changes. Because the operator's work flow changes are various, modeling with incorporation of these changes is complex. The process of a procedure can be modeled as a flowchart as depicted in Figure 8 and STPN modeling of the EOP is depicted in Figure 9 .

Figure 8. Procedure execution flow.

Figure 9. STPN modeling of EOP.

Table 2. Typical steps of emergency operating procedures.

No	Expected flow (Normal flow)	Contingency flow
1	IF pressurizer pressure is less than [SIAS set point], THEN verify SIAS is actuated	Ensure SIAS is actuated
2	Isolate the LOCA by performing ALL of the following: a. Ensure letdown containment isolation valve is closed b. Ensure RCS sampling containment isolation valves are closed c. Ensure ALL POSRVs are closed
3	Depressurize the RCS to SCS Entry Conditions by performing ANY of the following: a. Operate main or auxiliary pressurizer sprays b. Control charging and letdown

One of important EOP in APR1400 is a procedure for loss of coolant accident (LOCA). LOCA procedure consists of 73 steps and 367 instructions. When LOCA procedure is modeled with Colored Petri net, the additional transition for alternative flow is needed. The required number of additional transition has been calculated according to Table 1. Every instruction needs transition to the next step for “re-execution.” Every instruction needs transition to the step in forward direction for “change flow.” And every instruction needs transition to the step that is already completed for “re-execution.” Three hundred and fifty-nine transitions for “postpone,” 13,853 transitions for “change flow,” and 12,212 transitions for “re-execute” are required for alternative flow modeling with Colored Petri net. In STPN those additional transition is not needed. The simple state machine in token can be used to model alternative flow. Also, the number of state space that is needed for verification is decreased.

3. Discussion

3.1. Verification with STPN

The state of a token in STPN can be used for modeling of the operator's actions for procedure execution including interruptions. The operator actions such an interruption can change the procedure execution flow in various way, and it is difficult to model all of the possible procedure execution flow by ordinary Petri nets. STPN modeling can be divided by state machine part and Petri net part. Therefore, the verification of STPN can be performed with state machine and Petri net tools. Many existing Petri nets software tools can be applied including Petri nets tool for WfMS as a matter of course. Current Petri nets tools automatically compute all reachable states and represent state changes as a directed graph consisting of nodes and arcs. The state space method supports structural analysis including reachability and deadlock. The procedure is to be verified in terms of every step and instruction having a valid path of process. In other words, there should be no step or instruction that cannot be executed. Also, the procedure must be verified in terms of all steps having a path to other steps in normal flow without operator interruption; in other words, there should be no step or instruction that does not have at least one link to other step or instruction, including procedure completion. For CP modeling with operator interrupt, the state space is expanded according to the dynamic token state. In this case, the Petri net tool can be used to compute states by marking the condition as the state of the token.

When CPS has STPN as a modeling language for procedure writing and execution, CPS can provide a structural analysis when the operator is writing a procedure. This systematically prevents procedure flow errors and ensures the completeness of the procedure flow. V&V of the emergency procedure also can be supported with this formal verification. Also, qualified and error free procedure execution is essential to PBA, because some controls in a nuclear power plant can affect the safety of the NPP. STPN modeling and formal verification can be one of the required conditions for PBA.

3.2. Simple expression of procedure execution

STPN modeling has separate display formats: the behavior of the step process is in a Petri net format and behavior according to the operator interrupt is in a state machine of token. In CPS modeling, the Petri nets part of modeling describes the procedure process directly. It is easy to be understand and easy to be verified. When STPN-based modeling and verification is widely applied to CPS, the display format of CPS can be designed with ordinary Petri net symbols. This means that Petri net format at Figure 6 can be used directly or used after simplification. Simple expression of STPN also makes other complicated system modeling possible, because complicated system behavior is separated according to the Petri nets part and the state machine part.

4. Conclusion

STPN modeling language and formal modeling of computerized procedures are presented. STPN can be used for basic workflow modeling and various user interrupt modeling. CPS modeling with STPN supports formal verification of procedure execution. STPN also provides abstract modeling of procedures, because it can separate complex interrupt modeling from normal flow of modeling. Formal verification of CPS can provide an error free procedure for PBA. When CPS modeling is included in procedure writing software, the plant operator can verify the procedure when it is being written. Also, when CPS modeling is applied to a simulator with PBA, many accident scenarios can be simulated and analyzed automatically and the optimized procedure for the accident can be improved and specified according to the experiment results.