Model Checking Safety Properties of Servo-Loop Control Systems

This paper presents the experiences of using a symbolic model checker to check the safety properties of a servoloop control system. Symbolic model checking has been shown to be beneficial when the system under analysis can be modeled as a finite state machine. Servo-loop control systems are typically represented by differential equations (Laplace transforms) – not as finite state machines. However, the control loop is only a part of the software system needed to properly and safely operate the system. This paper first validates the safety of the servo loop using control theory and simulation. Then, a simple state model of a servo loop is combined with the state model of entire system. This model is then entered into a model checker (SMV) along with safety predicates. The model checker is used to validate the safety predicates. This paper shows via a concrete example that safety issues can be discovered and defined for control systems using a model checker. Furthermore, it demonstrat...

• Type: Conference
• Year: 2002
• Where: DSN
• Authors: M. Edwin Johnson
• Keywords: Computer Networks, Control Systems, DSN 2002, Finite State Machines, Model Checker