Model checking safety properties of servo-loop control systems

Presents the experiences of using a symbolic model checker to check the safety properties of a servo-loop 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 apart of the software system needed to properly and safely operate the system. The 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 the 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. The paper shows via an example-an antenna tracking system-that safety issues can be discovered and defined for control systems using a model checker. Furthermore, it demonstrates that effective hazard analysis may require multiple techniques.