Innovating Works

EUIN2015-62768

Financiado
ESTRUCTURAS DE TIPO Y PRUEBA PARA VERIFICACION DE SOFTWARE CONCURRENTE
LA VERIFICACION DE PROGRAMAS CONCURRENTES ES UNA TAREA QUE PLANTEA NOTABLES DIFICULTADES, QUE RADICAN EN LA INCAPACIDAD DE LOS METODOS EXISTENTES PARA APROXIMARSE AL PROBLEMA DE LA VERIFICACION DE UNA MANERA MODULAR, ES DECIR, SIG... LA VERIFICACION DE PROGRAMAS CONCURRENTES ES UNA TAREA QUE PLANTEA NOTABLES DIFICULTADES, QUE RADICAN EN LA INCAPACIDAD DE LOS METODOS EXISTENTES PARA APROXIMARSE AL PROBLEMA DE LA VERIFICACION DE UNA MANERA MODULAR, ES DECIR, SIGUIENDO EL PRINCIPIO DE DIVIDE ET IMPERA,LOS TIPOS DEPENDIENTES CONSTITUYEN UN METODO FORMAL BIEN CONOCIDO POR SU HABILIDAD PARA IMPLEMENTAR PRUEBAS MATEMATICAS MODULARES Y AUMENTADAS EN ESCALA, PERO, EN EL CONTEXTO DE LA PROGRAMACION, LOS TIPOS DEPENDIENTES SE CONSIDERAN LIMITADOS RESPECTO A UN MODELO DE COMPUTACION PURAMENTE FUNCIONAL Y QUE TERMINA,EL PRESENTE PROYECTO PRETENDE ELIMINAR ESTA LIMITACION Y ESCALAR A LOS TIPOS DEPENDIENTES PARA FACILITAR SIMULTANEAMENTE LA IMPLEMENTACION DE LOS PROGRAMAS CONCURRENTES CON ESTADO MUTABLE, ASI COMO LAS PRUEBAS DE SU EXACTITUD, APLICANDO EL PODER DE MODULARIZACION DE LOS TIPOS DEPENDIENTES A LOS PROGRAMAS Y LAS PRUEBAS SIMULTANEAMENTE, ESTE PROYECTO PRETENDE CONSEGUIR NUEVOS Y ESCALABLES FUNDAMENTOS EN EL CAMPO DE LA VERIFICACION DE PROGRAMAS CONCURRENTES,LA COMPOSICION MECANIZADA DE LAS PRUEBAS DE SOFTWARE (CONCURRENTE O NO) ES CONSIDERADA GENERALMENTE IMPRACTICABLE, SIN EMBARGO NOSOTROS ARGUMENTAMOS QUE ESTO NO TIENE QUE SER ASI SI SE SELECCIONAN CORRECTAMENTE LAS ABSTRACCIONES LINGUISTICAS PARA EXPRESAR LAS PRUEBAS, ESTA OBSERVACION SE APOYA EN NUESTROS RESULTADOS PRELIMINARES, LOS CUALES HAN SIDO BASTANTE ALENTADORES, EL PROYECTO PRETENDE DESCUBRIR NUEVAS ABSTRACCIONES LINGUISTICAS QUE FACILITARAN LA CREACION PRACTICABLE DE PRUEBAS FORMALES, Y PROPORCIONARAN UNA EVALUACION EXPERIMENTAL POR MEDIO DE LA VERIFICACION MECANIZADA DE PROGRAMAS CONCURRENTES EXTENSIVOS DERIVADOS DE CONTEXTOS REALISTICOS, TAL COMO LOS GARBAGE COLLECTORS CONCURRENTES, NUCLEOS DE SISTEMAS OPERATIVOS Y LIBRERIAS POPULARES CONCURRENTES DE OPEN SOURCE,ESTE ES UN PROYECTO DE ALTO RIESGO YA QUE PRETENDE PROPORCIONAR NUEVOS FUNDAMENTOS PARA LA VERIFICACION CONCURRENTE, CUYO DESARROLLO REQUIERE DE UNA INTERCALACION PROFUNDA DE LAS TEORIAS LOGICAS Y DE LA SEMANTICA DE PROGRAMAS CON PRUEBAS FORMALES, PERO AL MISMO TIEMPO EL PROYECTO OFRECE GRANDES BENEFICIOS, PORQUE EL AUMENTO DE ESCALA DE LA VERIFICACION CONCURRENTE ES EL PROBLEMA MAS PROMINENTE EN EL CAMPO DE LOS LENGUAJES CONTEMPORANEOS DE PROGRAMACION Y LA INVESTIGACION DE SUS SEMANTICAS, CIENCIA DE LA COMPUTACIÓN TEÓRICA\MÉTODFS FORMALES Y COMPUTACIÓN CUANTICA\INGENIERÍA DEL SOFTWARE\SISSTEMAS OPERATIVOS\LENGUAJES DE ORDENADOR\VERFICIACIÓN DE SOFTWARE\CONCURRENCIA\TEORÍA TIPO-DEPENDIENTE\LÓGICA DE HORAE ver más
01/01/2015
IMDEA SOFTWARE INS...
3K€
Perfil tecnológico estimado

Línea de financiación: concedida

El organismo AGENCIA ESTATAL DE INVESTIGACIÓN notifico la concesión del proyecto el día 2015-01-01
Presupuesto El presupuesto total del proyecto asciende a 3K€
Líder del proyecto
IMDEA SOFTWARE INSTITUTE No se ha especificado una descripción o un objeto social para esta compañía.
Perfil tecnológico TRL 4-5 650K