Entre los formalismos utilizados para especificación de sistemas en tiempo real y sistemas reactivos destacan los métodos estructurados. Son métodos operacionales que tienen amplia difusión en la industria por ser gráficos, fáciles de aprender, de utilizar y de revisar. Sin embargo, al no ser métodos formales, no existe, en general la posibilidad de analizar propiedades tan importantes como pueden ser las de seguridad.
En esta tesis se integran los métodos 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 ésta 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 síncrona 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. Tambien 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.