|
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
|
Sin nacionalidad |
|
Tamaño de la entidad
|
Desconocido |
|
Fecha concesión
|
|