• Título:  ESPECIFICACION Y VERIFICACION DE SISTEMAS REACTIVOS UTILIZANDO METODOS ESTRUCTURADOS Y LOGICA TEMPORAL
• Autor:  TUYA GONZALEZ PABLO JAVIER
• Universidad:  Universidad de Oviedo
• Fecha de Lectura:  01/01/1995
• Programa de doctorado:  DESCONOCIDO
• Dirección: 
  • CORRALES GONZALEZ, JOSÉ ANTONIO (DIRECTOR)
• Tribunal: 
  • BOTELLA LÓPEZ, PERE (PRESIDENTE)
  • DIEZ GONZALEZ, ALBERTO BENJAMIN (SECRETARIO)
  • MARTINEZ RODRIGUEZ FCO. JAVIER (VOCAL)
  • OJEA MERIN, GUILLERMO (VOCAL)
  • GONZÁLEZ ALONSO, OLIVERIO (VOCAL)
• Descriptores: 
  • CIENCIAS TECNOLOGICAS
  • TECNOLOGIA DE LOS ORDENADORES
  • INGENIERIA DE CONTROL
  • TECNOLOGIA DE LA INSTRUMENTACION
  • SISTEMAS EN TIEMPO REAL
• 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.