Hybrid systems refer to dynamical systems exhibiting a mixed discrete and continuous behaviours. Such behaviors appear naturally in embedded control systems, where one or more embedded processors executing discrete behaviors interacts with a continuous physical world. Stability is a fundamental property in control system design, which assures that small perturbations in the initial state or input to the system result in only small variations in the future behaviour. The classical methods for stability analysis rely on exhibiting a particular kind of function, called Lyapunov function. There exist automated methods for computing Lyapunov functions, which choose a template with certain parameters as a candidate Lyapunov function, and use certain constraint solvers to search for the parameters. However, the main difficulty with these template based methods is that choosing the right template requires user ingenuity. Further, a failed search for parameters does not provided any insights into the potential reasons for instability or guide the choice of subsequent templates.

We propose an alternate approach for stability analysis of hybrid systems, namely,a counterexample guided abstraction refinement (CEGAR) framework. Here, an abstraction of the original (concrete) system is constructed and model-checked,which either results in a stability proof or an abstract counter-example indicating a potential reason for instability.In the latter case, the abstract counter-example is analysed to either infer a bug in the concrete system or construct a finer abstraction.This approach addresses the shortcomings of the template based search through a counter-example guided refinement.

Our CEGAR algorithm has been implemented in the tool AVERIST, and we report experimental evaluations on some examples for demonstrating the feasibility of the approach.