used to
detect potential errors and to verify properties of operator procedures.
As there could be problems with modelling and model checking large
systems, incremental modelling and verication is proposed as a strategy
to help overcome these problems. A case study is presented to show how
model checking (with the model checker Spin [5]) and the incremental
strategy work in practise.
1 Introduction
Operator procedures are documents telling operators what to do in various situ-
ations. There are procedures to be used in normal operation situations, in case of
disturbances and in case of emergencies. Operator procedures are widely used in
process industries including the nuclear power industry. The correctness of such
procedures is of great importance. The following is a quote from the report on
the accident at the Three Mile Island [6]: A series of events - compounded by
equipment failures, inappropriate procedures, and human errors and ignorance
- escalated into the worst crisis yet experienced by the nations nuclear power
industry. Such inappropriate procedures included procedures for loss of coolant
accident and for pressurizer operations [7].
To assess the correctness of operator procedures, we need correctness require-
ments. The correctness requirements of an operator procedure include goals that
must be achieved upon completion of an execution of the procedure, safety con-
straints that must be maintained during an execution of the procedure and
general structural requirements. For achieving goals, necessary and eective in-
structions must be explicitly specied in the procedure. In addition, time and
resource constraints for carrying out the instructions must be satisable. For
maintaining safety constraints, preparation steps for the goal-oriented instruc-
tions must be included in the procedure. It is also important that instructions
are specied in the correct order and time and resource constraints for carrying
out the preparation steps are satisable. Structural requirements make a proce-
dure simple and easy to understand. They include no undened references and
unreachable instructions. Violation of the correctness requirements could result in many types of er-
rors. Although all types of violations are important with respect to correctness,
formal verication techniques only oer a partial solution to the verication of
procedures. Problems related to time and resource constraints are more com-
plicated and are not considered for verication in this paper. We divide the
types of errors to be considered for verication into three categories: structural
errors, execution errors and consistency errors. Structural errors include unde-
ned references and unreachable instructions as mentioned earlier. A reference
is undened, if it refers to no instruction in the procedure. The cause of an
undened reference could be that the reference is wrong or the instruction to
which it refers is missing. An instruction is unreachable, if it cannot be reached
from any potential execution of the procedure. For instance, if there is a block
of instructions without any reference from outside of the block, the instructions
in the block will be unreachable (unless one of the instructions in the block is
the starting point of the procedure). A more complicate situation is that there
are instructions refer to this block, but the conditions for using the references
never become true in all potential executions of the procedure. Execution errors
are errors that prevent an execution to be completed. They include deadlocks
and innite loops. There is a deadlock, if the operator stops at some point and
is not able to do anything in order to complete the procedure. For instance, the
operator may be waiting for a condition which never becomes true. There is an
innite loop, if the operator is captured by a loop and cannot jump out of the
loop by following the instructions of the procedure. The causes for innite loops
could be wrong actions, wrong conditions or wrong references in goto instruc-
tions, and other types of problems. Consistency errors indicate inconsistency
between the set of instructions of the procedure and given specications. They
include violation of assertions (representing conditions for performing actions),
violation of invariants and unreached goals. The basic question is how to detect
potential errors in operator procedures. In this paper, we discuss using model
checking for this purpose.
2 Verication Approach
To begin with, we have a procedure that needs to be veried. It is however not
sucient to analyse the procedure alone. We have to take into consideration the
environment in which the procedure is used. As our work is related to procedure
correctness in power plants, in the following, we refer to a power plant as the
environment of the procedure.
2.1 Model Checking
The idea of using model checking is as follows. When we design a procedure,
we do so in a natural or semi-formal language. When the procedure is executed,
the operator (in the following, the meaning of an operator is dened as a person
or a robot that strictly follows the procedure) gets responses from the plant as the procedure is being carried out. Such a procedure, the set of the possible
initial states of the plant, the plant processes and the interaction between these
processes determine a logical structure. On the other hand, there could be cor-
rectness conditions for the plant and the interaction between the operator and
the plant. For instance, we may want to express the following: Pump-A must
not be running at the time one starts repairing Valve-A (an assertion at a
point of an execution of the procedure), Valve-B is closed unless Valve-C is
closed (an invariant in an execution of the procedure), and the state of the plant
will become Normal after starting the procedure (a liveness property of the
procedure). These conditions can be veried against the logical structure.
2.2 Verication and Error Detection
As explained above, in order to be able to verify a procedure, there are two main
tasks: modelling the logical structure and verication with respect to correctness
conditions. The modelling task is to create the following processes:
A model-procedure process, which is used to model the procedure (or the
operator in a process of executing the procedure).
A set of plant processes, which are used to model the physical processes of
the plant (or assumptions on the physical processes).
A set of interaction processes, which are used to model the interaction be-
tween the model-procedure process and the plant processes.
An initialisation process, which is a process for choosing an initial state from
the set of possible initial states of the plant.
The following are the principles for modelling:
The model-procedure process communicates only with the interaction pro-
cesses and does not directly read or update variables representing the system
state. We impose these restrictions to the model-procedure process because
it is very helpful with a clear separation of the consequences of the actions
of the model-procedure process and the consequences of the actions of other
processes.
The interaction processes communicate with the model-procedure process
and the plant processes. They may read and update the system state and
may also initiate and activate some of the plant processes.
The plant processes communicate with the interaction processes and may
read and update the system state. Sometimes synchronisation mechanism is
necessary in order to ensure the ability of the interaction processes to take
appropriate actions immediately after changes are made to the system state
by the plant processes.
The initialisation process updates the system state before other processes
read or update the system state.
After these processes are created, we can use a model checker to check errors of
the types described in the previous section. The techniques for checking errors
are as follows: For detecting undened references, we check syntactic errors.
For detecting deadlocks and innite loops, we check execution errors of the
procedure (using an auxiliary variable to indicate the completion of an exe-
cution of the procedure).
For detecting unreachable instructions, it is not necessary to use any special
technique, since such problems can also be reported by checking execution
errors (unreachable instructions can be detected in cases where no execution
errors are found).
For detecting violation of conditions for performing actions, we need asser-
tions describing conditions for relevant actions and we check whether the
procedure is consistent with respect to the assertions.
For detecting violation of invariants, we need invariants and we check whether
the procedure is consistent with respect to the invariants (i.e. whether they
hold in all reachable states of the model).
For detecting unreached goals, we need goals and we check whether the
procedure is consistent with respect to the goals (i.e. whether they can be
reached in all reachable paths of the model).
As the verication can be carried out by using fully automated model checking
tools, the verication task is simple. The major problems of model checking oper-
ator procedures are the complexity of the modelling of the relevant processes of
the power plant and the complexity of the models. Because there are many pro-
cesses that interfere with each other in the power plant, a model of the relevant
processes of the power plant can be very complicated. On the other hand, it is
not necessary to have a complete model for using model checking. The necessary
and optimal complexity depends on the properties to be veried. In order to
limit the complexity, one has to make a decision on how complicated the plant
process model should be. This is a dicult decision, because a complicated model
may not be