Observatorio de I+D+i UPM

Memorias de investigación
Proyecto de I+D+i:
ValIdación y Verificación de Aplicaciones Concurrentes (VIVAC)
Año:2013
Áreas de investigación
  • Lenguaje de programación
Datos
Descripción
La concurrencia y la distribucio?n se han convertido en aspectos fundamentales de gran parte de las aplicaciones in- forma?ticas actuales. Indiscutiblemente, Internet y la amplia disponibilidad de multi-procesadores influyen de forma radical en el tipo de aplicaciones que se desarrollan. Asi? pues, las aplicaciones software esta?ndar tienen que tratar con aspectos distribuidos tales como fallos y retrasos en la transmisio?n por red. Adema?s, los fabricantes de chips esta?n apostando por los disen?os de procesador multi-core como forma de mejorar el rendimiento en los ordenadores de mesa, de empresa y en los procesadores mo?viles. Esta corriente ha trai?do un intere?s renovado en desarrollar te?cnicas que ayuden a comprender, analizar y verificar el comportamiento de los programas concurrentes y distribuidos. La fi- nalidad gene?rica del proyecto VIVAC es contribuir al desarrollo de nuevas tecnologi?as para la validacio?n y verificacio?n de aplicaciones software concurrentes que permitan construir software ma?s fiable y de mayor calidad. En te?rminos generales, el proyecto contribuira? al acercamiento de las te?cnicas de ana?lisis y validacio?n, en especial de los me?todos basados en interpretacio?n abstracta, a las necesidades actuales de los lenguajes de programacio?n concurrentes y su proceso de desarrollo del software. Es bien conocido que razonar sobre aplicaciones concurrentes es mucho ma?s complejo que hacerlo sobre aplica- ciones secuenciales debido a las posibles interacciones entre tareas: las tareas pueden suspender su ejecucio?n, en- trelazarse con la ejecucio?n de otra tarea y despue?s reanudar la ejecucio?n. Durante estas interacciones los datos com- partidos a menudo se modifican, y esto puede llevar a situaciones de bloqueo, carreras de datos, no terminacio?n, consumo infinito de recursos, etc. En el proyecto VIVAC nos centraremos, principalmente, en dos te?cnicas comple- mentarias que, adema?s, se pueden usar conjuntamente para garantizar que el producto cumple con sus especifica- ciones o requisitos y que tiene el comportamiento esperado: Por un lado, la verificacio?n es un proceso de garanti?a de calidad, que permitira? asegurar que los programas cumplen ciertas propiedades con total seguridad. En este sentido, desarrollaremos nuevas te?cnicas que infieren propiedades avanzadas sobre los programas concurrentes. Dichas pro- piedades incluira?n, entre otras, la terminacio?n, el consumo finito de recursos, y la ausencia de carreras de datos entre tareas. Por otro lado, la validacio?n es un proceso de control de calidad, cuya intencio?n es comprobar (o chequear) que el producto cumple ciertas propiedades con el objetivo de predecir errores que pueden llevar a situaciones en las que no se cumplen los requisitos. La parte de validacio?n se centrara? en gran medida en la generacio?n de casos de prueba que garanticen un cierto recubrimiento del co?digo, sobre los que se validara? su correcto funcionamiento para las especificaciones dadas. Este ambicioso objetivo se concreta, a su vez, en el desarrollo de nuevas herramientas y en- tornos que den soporte automatizado a la especificacio?n, ana?lisis, validacio?n y verificacio?n de sistemas concurrentes, todo ello con una rigurosa base formal.
Internacional
No
Tipo de proyecto
Proyectos y convenios en convocatorias públicas competitivas
Entidad financiadora
Ministerio de Economía y Competitividad
Nacionalidad Entidad
ESPAÑA
Tamaño de la entidad
Desconocido
Fecha concesión
01/01/2013
Esta actividad pertenece a memorias de investigación
Participantes
  • Participante: Guillermo Roman Diez (UPM)
  • Participante: Laura Bozzelli (UPM)
  • Participante: Md. Abu Naser Masud (UPM)
  • Participante: Raul Gutierrez Gil (UPM)
  • Director: Alvaro German Puebla Sanchez (UPM)
  • Participante: José Miguel Rojas Siles (UPM)
  • Codirector: Elvira Albert (Universidad Complutense de Madrid)
  • Participante: Damiano Zanardini (UPM)
  • Participante: Samir Genaim (Universidad Complutense de Madrid)
  • Participante: Puri Arenas (Universidad Complutense de Madrid)
  • Participante: Jesús Correas (Universidad Complutense de Madrid)
  • Participante: Miguél Gómez Zamalloa (Universidad Complutense de Madrid)
Grupos de investigación, Departamentos, Centros e Institutos de I+D+i relacionados
  • Creador: Departamento: Inteligencia Artificial
S2i 2021 Observatorio de investigación @ UPM con la colaboración del Consejo Social UPM
Cofinanciación del MINECO en el marco del Programa INNCIDE 2011 (OTR-2011-0236)
Cofinanciación del MINECO en el marco del Programa INNPACTO (IPT-020000-2010-22)