Formal verification analysis of load-voltage power 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. The model is developed by ABB Schweiz AG Corporate Research as a test case intended for control synthesis and analysis of hybrid systems. Formal Verification of hybrid control system relies on the possibility to construct a (mite state transition model of a discretized system. An efficient search procedure is used to check whether desired system properties hold 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. The power control system properties were verified with the help of RuleBase, a formal verification tool developed by the IBM Haifa Research Laboratory. We successfully verify that relay controllers work according to specification and can stabilize a system after the collapse of the voltage transmission line. Our results show that formal verification techniques aze capable of finding heuristic control pazameters for this kind of control problem. © 2006 TSI® Press.