Especificación y verificación de sistemas reactivos utilizando métodos estructurados y lógica temporal

Abstract

En esta tesis se integran los metodos estructurados (sa/rt) junto con métodos formales de verificación basados en lógica temporal. El objetivo es utilizar un método operacional (sa/rt) para especificar el comportamiento del sistema, y complementar esta con una especificación declarativa basada en lógica temporal (ctl). La consistencia entre una y otra son entonces verificadas utilizando un comprobador de modelos (smv). Para poder analizar las propiedades del sistema se dota al método operacional de una sintaxis y semántica basadas en un sistema de transiciones, formando un modelo de procesos concurrentes entrelazados comunicados por variables compartidas. Además se enriquece la expresividad de los métodos sa/rt incorporando extensiones tales como la posibilidad de comunicación entre procesos de forma sincrona y a través de variables compartidas. Las transiciones pueden ser deterministas (con prioridades) o no deterministas. El modelo es traducido al lenguaje que será utilizado por el comprobador de modelos smv. Se proporcionan los algoritmos de traducción a este lenguaje. Con el objetivo de reducir el tamaño del modelo en el que se van a verificar las propiedades de seguridad, se proporciona un método para reducir su tamaño, y para componer especificaciones parciales. También se tratan otras propiedades de vivacidad. Finalmente, todo lo anterior se ilustra mediante tres ejemplos de diferentes tamaños, dos de ellos correspondientes a sistemas reales.