Verification of HMI safety for process control systems: A formal approach

Human factors have been recognized as one of the main sources of accidents. For a process control system, to ensure the safety of its human machine interface (HMI) is of great importance to different levels of system design and implementation. Traditional safety analysis approach to a process control system involves the using of expert experiences and generic system safety techniques. However, such an approach does not usually consider the discretionary nature of human behavior. This paper proposes a formal approach to the safety verification of the HMI design of process control systems. Safety properties are formalized using computation tree logic; and the dynamic behavior of the operator, the hardware interface the control instrument and the HMI control logic are modeled using timed automata. Finally, an industrial case is provided to illustrate the verification procedure.