Model checking operator procedures.pdf

Model Checking Operator Procedures Wenhui Zhang Institute for Energy Technology, P.O.Box 173, N-1751 Halden, Norway Wenhui.Zhang@hrp.no Abstract. Operator procedures are documents telling operators what to do in various situations. They are widely used in process industries including the nuclear power industry. The correctness of such procedures is of great importance. We describe how model checking can be 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 verification 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 nation’s 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 effective in- structions must be explicit