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

Figures & data

Figure 1. CPS display for emergency operating procedure.

Figure 2. Procedure execution flow.

Figure 3. Alternative procedure flows.

Figure 4. Colored Petri net.

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

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.

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

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