An Algorithmic Approach for Stability Verification of Hybrid Systems

Resumen

Cyber-physical systems (CPS) are engineered systems which integrate computer-based algorithms and physical components. One of the main features of CPS is the interaction between the discrete algorithmic behaviour and the continuous physical behaviour, which results in a more intricate performance. This mixed behaviour can be modelled by hybrid systems. A critical property in hybrid systems design is stability, which ensures robustness of the system with respect to small perturbations of the input to the system. The state-of-the-art methodology for providing stability proofs lies on searching for Lyapunov functions. This thesis proposes an alternative and novel algorithmic approach to stability verification of hybrid systems, which uses formal methods. The aim of formal verification is to automatically provide strong guarantees of correctness. This thesis introduces the development and implementation of a formal verification method for analysing stability of hybrid systems. Such a stability verification approach consists of an automated proof which relies on abstraction and model checking techniques. The abstraction technique is a modified predicate abstraction that constructs a finite weighted graph from a hybrid system by preserving stability. The evaluation of an abstract weighted graph, which is a finite state system, is more efficient than evaluating a hybrid system with infinite states. Therefore, the abstract weighted graph is model checked to either infer stability of the former system or output a potential instability reason namely counterexample. The counterexample obtained through model checking can either correspond to an unstable behaviour of the hybrid system or be spurious. This thesis includes a validation algorithm to differentiate between the two possibilities by solving a non-bounded model checking problem, and it also introduces two refinement techniques for the case that the counterexample is spurious. These refinement techniques provide additional predicates, deducted from the counterexample, to construct a more accurate abstract weighted graph. All the developed techniques (abstraction, model checking, validation and refinement) are articulated to obtain a counterexample guided refinement abstraction (CEGAR) framework. This CEGAR framework allows to iterate over the abstract systems, returns a counterexample if the abstraction fails and uses such a counterexample for guiding the choice of the next abstraction. The introduced CEGAR algorithm is illustrated by verifying stability of an automatic gearbox and implemented in a software tool called Averist. Such an implementation provides empirical evidence of the correctness of the theoretical techniques. Some of the advantages of using Averist are that the input data can be easily defined by people with no experience in hybrid systems and running Averist does not require a formal knowledge on stability analysis.