Tesis:
An Algorithmic Approach for Stability Verification of Hybrid Systems
- Autor: GARCÍA SOTO, Miriam
- Título: An Algorithmic Approach for Stability Verification of Hybrid Systems
- Fecha: 2017
- Materia: Sin materia definida
- Escuela: E.T.S DE INGENIEROS INFORMÁTICOS
- Departamentos: LENGUAJES Y SISTEMAS INFORMATICOS E INGENIERIA DE SOFTWARE
- Acceso electrónico: http://oa.upm.es/47805/
- Director/a 1º: PRABHAKAR, Pavithra
- Resumen: Los sistemas ciberfísicos son sistemas tecnológicos interconectados que integran componentes de índole física y elementos software. Los elementos software evolucionan de forma discreta, mientras las características físicas son de naturaleza continua; la interacción entre ambos comportamientos da lugar a un comportamiento mucho más complejo, que es característico de los sistemas ciberfísicos. Una herramienta clave para modelar este tipo de comportamientos son los sistemas híbridos. Una propiedad relevante en el diseño de sistemas híbridos es la estabilidad, puesto que garantiza solidez en el estado del sistema a pesar de posibles pequeñas modificaciones en las condiciones iniciales del sistema. El estado del arte en cuanto a la metodología que se emplea en el análisis de estabilidad radica en la búsqueda de funciones de Lyapunov, puesto que la existencia de dicha función supone una demostración de estabilidad. Esta tesis propone un método alternativo y novedoso en el análisis de estabilidad de sistemas híbridos, que consiste en una técnica algorítmica que hace uso de métodos formales. El objetivo de las técnicas de verificación formal es proporcionar de forma automática garantías sólidas del correcto funcionamiento de un sistema. En esta tesis se desarrolla e implementa un método de verificación formal que analiza la estabilidad en sistemas híbridos. Este método analítico consiste en un proceso automático basado en técnicas de abstracción y verificación de modelos (o model checking). El método de abstracción es una modificación de las abstracciones basadas en predicados, que a partir de un sistema híbrido construye un grafo ponderado finito que conserva la estabilidad. El análisis sobre el grafo ponderado resulta más eficiente que el que se realizaría directamente sobre el sistema híbrido, puesto que este último contiene infinitos posibles estados. Por lo tanto, el grafo abstracto ponderado se analiza para inferir estabilidad del sistema híbrido u obtener una causa potencial de inestabilidad del sistema, denominada contraejemplo. El contraejemplo, obtenido mediante el análisis aplicado al grafo ponderado, se corresponde a un comportamiento inestable del sistema híbrido o es falso. Esta tesis incluye un algoritmo de validación que distingue entre estas dos posibilidades y que implica verificar una ejecución del modelo con infinitas posiciones. También se incluyen dos técnicas de refinamiento de la abstracción, para el caso en que el contraejemplo sea falso. Las técnicas de refinamiento proveen nuevos predicados, que se añaden en la construcción del grafo ponderado para que este resulte más preciso. La articulación de todas las técnicas desarrolladas en esta tesis (abstracción, verificación de modelos, validación y refinamiento) conforman una técnica algorítmica conocida como refinamiento de abstracción guiado por contraejemplo (cegar). Este enfoque cegar permite iterar sistemáticamente sobre el sistema abstracto, devolviendo un contraejemplo en caso de que la abstracción no resulte informativa, y usando este contraejemplo como guía para la elección de la siguiente abstracción. También se presenta el desarrollo de una herramienta software, llamada Averist, que incluye la implementación del algoritmo cegar y proporciona evidencia empírica de los resultados teóricos. Los datos de entrada de este software se pueden definir fácilmente sin necesidad de experiencia en sistemas híbridos, y su ejecución no requiere conocimientos formales en cuanto al análisis de estabilidad. ----------ABSTRACT---------- Cyber-physical systems (cps) are engineered systems which integrate computerbased 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 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.