Diseño y verificación de sistemas distribuidos mediante la aplicación combinada de métodos formales

Resum

ESTA TESIS DOCTORAL SE CENTRA EN LA APLICACIÓN DE LAS TECNICAS FORMALES AL DISEÑO Y VERIFICACION DE SISTEMAS DISTRIBUIDOS, CONCRETAMENTE A LA FASE INICIAL DE CAPTURA DE LOS REQUISITOS DE USUARIO, EL TRABAJO DEFINE UN PROCEDIMIENTO METODOLOGICO PARA OBTENER LA ARQUITECTURA INICIAL EN FORMA DE SISTEMA DE TRANSICIONES SIMBOLICO. PARA ELLO, DEFINE LA LOGICA TEMPORAL LTCS Y UN ALGORITMO DE MODEL CHECKING PARA LA VERIFICACION DE LAS PROPIEDADES QUE SE DESEA QUE CUMPLA EL SISTEMA. EN CASO DE NO CUMPLIRSE UNA PROPIEDAD, EN LA TESIS SE PROPONE UNA VARIANTE DE MODEL CHECKING CON REGISTROS DE INFORMACIÓN PARA IDENTIFICAR POSIBLES MODIFICACIONES DEL SISTEMA QUE DERIVEN EN EL CUMPLIMIENTO DE LA CITADA PROPIEDAD. EL MODELO RESULTANTE ES AUTOMATICAMENTE TRADUCIDO A UNA ESPECIFICACION ELOTOS QUE SIRVE COMO PUNTO DE PARTIDA PARA UN PROCESO DE REFINAMIENTOS.