Formal verification analysis of load-voltage power dynamics and control

This paper introduces an application of a Formal Verification (or model checking) technique to improve performance in a voltage collapse power control system. The model of the control system has a hybrid character and is comprised of a continuous-time load dynamics model, algebraic equations of the power balance on the load bus, and a discrete tap changer controller. Formal Verification of hybrid control system relies on the possibility to construct a finite state transition model of a discretized system. An efficient search procedure is used to check whether a desired system property holds true in that model. Formal verification methods provide full coverage of all possible cases (scenarios), and thereby check whether the specified system properties are satisfied. In order to apply FV to a hybrid control system, the system needs to be discretized. The power control system properties were verified with the help of RuleBass, a formal verification tool developed by the IBM Haifa Research Laboratory. We verify that relay controllers work according to specification and can stabilize a system after the collapse of the voltage transmission Line. Our results shows that formal verification techniques are capable of finding heuristic control parameters for these kind of control problem.