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

Resumen

EN ESTA TESIS SE INTEGRAN LOS METODOS ESTRUCTURADOS (SA/RT) JUNTO CON METODOS FORMALES DE VERIFICACION BASADOS EN LOGICA TEMPORAL. EL OBJETIVO ES UTILIZAR UN METODO OPERACIONAL (SA/RT) PARA ESPECIFICAR EL COMPORTAMIENTO DEL SISTEMA, Y COMPLEMENTAR ESTA CON UNA ESPECIFICACION DECLARATIVA BASADA EN LOGICA 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 METODO OPERACIONAL DE UNA SINTAXIS Y SEMANTICA BASADAS EN UN SISTEMA DE TRANSICIONES, FORMANDO UN MODELO DE PROCESOS CONCURRENTES ENTRELAZADOS COMUNICADOS POR VARIABLES COMPARTIDAS. ADEMAS SE ENRIQUECE LA EXPRESIVIDAD DE LOS METODOS SA/RT INCORPORANDO EXTENSIONES TALES COMO LA POSIBILIDAD DE COMUNICACION ENTRE PROCESOS DE FORMA SINCRONA Y A TRAVES DE VARIABLES COMPARTIDAS. LAS TRANSICIONES PUEDEN SER DETERMINISTAS (CON PRIORIDADES) O NO DETERMINISTAS. EL MODELO ES TRADUCIDO AL LENGUAJE QUE SERA UTILIZADO POR EL COMPROBADOR DE MODELOS SMV. SE PROPORCIONAN LOS ALGORITMOS DE TRADUCCION 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 METODO 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.