Hybrid system analysis with finite-state model checkers

Résumé

En esta tesis se aborda el problema del análisis de sistemas híbridos mediante el uso de herramientas de model checking para sistemas de estados finitos. El model checking es una técnica formal que se utiliza para detectar errores de diseño en sistemas. Se utiliza un modelo del sistema real descrito en un lenguaje de modelado específico, y un conjunto de propiedades que queremos verificar, que se describen normalmente con lógicas. El model checking se ha utilizado originalmente para analizar las diferentes ejecuciones de modelos de sistemas concurrentes, en los que había un número de estados finito. Los sistemas híbridos se utilizan para modelar sistemas reales que presentan una mezcla de comportamiento continuo y discreto. El comportamiento continuo se debe a que hay variables que evolucionan con el tiempo siguiendo ecuaciones diferenciales ordinarias. El comportamiento discreto normalmente está asociado a modos de funcionamiento o control. Estos sistemas presentan en la mayoría de los casos un número infinito de estados, por lo que no se pueden analizar directamente con las herramientas tradicionales. Existen técnicas formales que permiten analizar algunas clases de sistemas híbridos. Muchas de ellas tienen como base las técnicas formales tradicionales y la interpretación abstracta. En esta tesis proponemos una metodología para extender de manera modular y no intrusiva herramientas de model checking existentes para el análisis de sistemas híbridos. La metodología consiste en analizar una abstracción del sistema real como si fuera un sistema discreto, utilizando un conjunto de estructuras y librerías de abstracción externas a la herramienta de model checking. Por tanto la herramienta original no se modifica. Utilizando la misma metodología es posible incorporar a la herramienta un modelo de tiempo discreto o denso. En el caso del modelo de tiempo denso, analizamos sistemas descritos como autómatas rectangulares inicializados, una subclase del autómata híbrido para el que la alcanzabilidad y la verificación de propiedades LTL es decidible. En este caso utilizamos los poliedros convexos como abstracción de las variables continuas. En la tesis hemos formalizado la metodología y hemos implementado dos prototipos basados en las herramientas de model checking SPIN y Java PathFinder con modelo de tiempo denso. Para ello hemos utilizado la librería de abstracción numérica Parma Polyhedra. Hemos utilizado estos prototipos para analizar algunos casos de estudio. Así mismo, hemos utilizado una extensión de la herramienta SPIN con modelo de tiempo discreto para desarrollar una herramienta de ayuda a la decisión para la gestión de embalses en episodios de avenida. Lo que hace esta herramienta es sintetizar el controlador necesario en un embalse concreto para poder afrontar una avenida manteniendo los niveles de agua embalsada y desembalsada en unos márgenes.