Innovating Works

TIN2008-06622-C03-02

Financiado
VERIFICACION Y DEPURACION AGILES ORIENTADAS A MEJORAR LA SEGURIDAD DEL SOFTWARE
LAS TECNICAS FORMALES OFRECEN MUCHAS VENTAJAS DE CARA A ASEGURAR LA FIABILIDAD DEL SOFTWARE, TAL Y COMO ATESTIGUA LA "ACCION ESTRATEGICA DE TELECOMUNICACIONES Y SOCIEDAD DE LA INFORMACION" DEL PROGRAMA NACIONAL 2008-2011, RESULTA... LAS TECNICAS FORMALES OFRECEN MUCHAS VENTAJAS DE CARA A ASEGURAR LA FIABILIDAD DEL SOFTWARE, TAL Y COMO ATESTIGUA LA "ACCION ESTRATEGICA DE TELECOMUNICACIONES Y SOCIEDAD DE LA INFORMACION" DEL PROGRAMA NACIONAL 2008-2011, RESULTA PRIORITARIO ASEGURAR LA E-CONFIANZA EN LOS SERVICIOS PROPORCIONADOS POR LA SOCIEDAD DE LA INFORMACION, SIN EMBARGO, A PESAR DE LOS MUCHOS AVANCES EN LOS FORMALISMOS SUBYACENTES PARA LA ESPECIFICACION, VERIFICACION Y TRANSFORMACION, LAS TECNICAS FORMALES SE USAN MUY POCO EN LA PRACTICA, PODRIAMOS CONSIDERAR, ENTRE OTRAS, LAS SIGUIENTES CAUSAS PARA ESTA SITUACION:- LA APLICACION DE TECNICAS FORMALES ES A MENUDO COMPUTACIONALMENTE MUY COSTOSA, COMO CONSECUENCIA, RESULTA DIFICIL QUE SE PUEDA APLICAR A SISTEMAS SOFTWARE REALISTAS,- SU APLICACION REQUIERE USUARIOS CON UN CONOCIMIENTO PROFUNDO DE LAS TEORIAS SUBYACENTES, EN OCASIONES, INCLUSO ENTENDER LOS RESULTADOS PUEDE SER UNA TAREA MUY COMPLEJA (POR EJ,, ENTENDER Y LOCALIZAR LA POSICION DE UN ERROR INDICADO POR UNA HERRAMIENTA DE VERIFICACION),PARA EVITAR ESTOS PROBLEMAS, MUCHAS PROPUESTAS RECIENTES ABOGAN POR EL USO DE TECNICAS FORMALES "AGILES", EN ALGUNOS CASOS, LAS TECNICAS CONSIDERADAS NO SON NI CORRECTAS NI COMPLETAS; SE TRATA DE UNA DECISION DE DISEÑO DELIBERADA PARA MEJORAR LA EFECTIVIDAD DE LAS HERRAMIENTAS ASOCIADAS (ESTE ES EL CASO, POR EJ,, DE LA HERRAMIENTA ESC/JAVA PARA EL ANALISIS ESTATICO DE PROGRAMAS JAVA), EN OTROS CASOS, SE HACE HINCAPIE EN EL DESARROLLO DE HERRAMIENTAS COMPLETAMENTE AUTOMATICAS QUE MINIMICEN LA INTERVENCION DEL USUARIO,EN ESTE PROYECTO, ABORDAMOS EL DESARROLLO DE APROXIMACIONES "AGILES" DE ESPECIFICACION, VERIFICACION Y DEPURACION PARA MEJORAR LA SEGURIDAD DEL SOFTWARE, EN PARTICULAR, BASAMOS NUESTROS DESARROLLOS EN LOS SIGUIENTES PUNTOS:- DISEÑAR METODOS CORRECTOS Y COMPLETOS PARA LAS CARACTERISTICAS CLAVE DE LOS LENGUAJES CONSIDERADOS, DEMOSTRAR FORMALMENTE SU CORRECCION Y DESARROLLAR PROTOTIPOS QUE LOS VALIDEN,- DISEÑAR VERSIONES "AGILES" DE LOS METODOS (POSIBLEMENTE INCORRECTAS Y/O INCOMPLETAS) PARA SUBCONJUNTOS REALISTAS DE LENGUAJES DE PROGRAMACION, DESARROLLAR Y/O APLICAR HERRAMIENTAS SOFTWARE ROBUSTAS,- DISEÑAR TECNICAS Y HERRAMIENTAS TOTALMENTE AUTOMATICAS SIEMPRE QUE SEA POSIBLE, DE FORMA QUE LOS CONOCIMIENTOS DEL USUARIO NO SEAN CRITICOS,EL PLAN DE TRABAJO DEL PROYECTO SE ESTRUCTURA EN LAS SIGUIENTES CUATRO LINEAS DE INVESTIGACION:* ESPECIFICACION Y VERIFICACION, SE CENTRA EN LA ESPECIFICACION DE SISTEMAS CONCURRENTES Y DISTRIBUIDOS COMPLEJOS COMO PROTOCOLOS DE REDES, WORKFLOWS, SERVICIOS WEB Y PROTOCOLOS DE COORDINACION,* ANALISIS DE TERMINACION Y QUASI-TERMINACION, NOS CENTRAMOS EN EXTENDER Y MEJORAR NUESTRAS TECNICAS PREVIAS PARA EL ANALISIS DE TERMINACION Y QUASI-TERMINACION DE NARROWING Y REESCRITURA, ADEMAS, PLANEAMOS DEFINIR VERSIONES "AGILES" PARA ANALIZAR LA TERMINACION DE UN LENGUAJE DE BAJO NIVEL COMO EL BYTECODE DE JAVA,* TRANSFORMACIONES CERTIFICADAS Y DEPURACION, CONSIDERAMOS EL DESARROLLO DE HERRAMIENTAS TOTALMENTE AUTOMATICAS (Y DEMOSTRABLEMENTE CORRECTAS) QUE NO REQUIERAN LA INTERVENCION DEL USUARIO, TAMBIEN CONSIDERAREMOS EL DISEÑO E IMPLEMENTACION DE UN DEPURADOR POTENTE Y FACIL DE USAR PARA PROGRAMAS JAVA CON ASERCIONES, ESTA LINEA DE INVESTIGACION ES UNA CONTINUACION NATURAL DE NUESTRAS INVESTIGACIONES PREVIAS EN EL MARCO DEL PROYECTO MERIT (REF, TIN2005-09207-C03-02), depuración de programas\verificación\seguridad del software\certificación\tecnologías declarativas\herramientas de transformación ver más
01/01/2008
UPV
125K€
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 2008-01-01
Presupuesto El presupuesto total del proyecto asciende a 125K€
Líder del proyecto
UNIVERSITAT POLITÈCNICA DE VALÈNCIA No se ha especificado una descripción o un objeto social para esta compañía.
Total investigadores 683