Técnicas Formales para la Verificación y el Desarrollo de Programas Reactivos
Resumen del Plan de Trabajo:
La interacción cotidiana con sistemas basados en computadoras es hoy un hecho inevitable. Podemos encontrar microprocesadores en electrónica de consumo (ej.: TVs, reproductoras de video o CD), medios de transporte (ej.: aviones, autos, controladores de diversos tipos de tráfico), sistemas de comunicación, plantas industriales, redes de computadoras, equipos médicos, etc. El funcionamiento incorrecto de cualquiera de estos sistemas tiene una diversidad de consecuencias que varían desde una molestia en el usuario, hasta situaciones que pueden poner en peligro la vida humana, e inclusive, generar serias catástrofes. Para la mayoría de tales sistemas, es crucial que ellos provean un servicio correcto y eficiente.
Es la tarea de este proycto el estudiar y desarrollar técnicas que permitan obtener programas correctos y eficientes. La efectividad de tales técnicas sólo se logra con un enfoque formal, i.e., matemático. Más precisamente:
El objetivo de este proyecto es el desarrollo de técnicas formales y herramientas (semi-)automáticas basadas en estas, que permitan especificar, diseñar y analizar la corrección y confiabilidad de los sistemas.
El objetivo general se atacará desde tres puntos distintos. Por un lado se propone el estudio y desarrollo de técnicas que lleven a herramientas completamente automáticas (los denominados model checkers) con especial énfasis en los denominados cuantitativos que permiten cuantificar probabilisticamente la validez de una propiedad. Se estudiarán también los aspectos fundamentales de sistemas complejos donde factores continuos —como puede ser el tiempo, movimientos, y otros paraámetros como temperatura o presión— se describen mediante variables aleatorias. El tercer punto plantea una manipulación sintáctica de los progrmamas mediante la técnica de transformación de programas. Agregamos además un cuarto punto, ya menos relacionado pero que podría verse como un área de aplicación del model checking cuantitativo.
Participantes
| Pedro
R. D'Argenio (Director)
Javier Blanco (Co-Director) |
F. Matías
Cuenca Acuña
Nicolás Wolovick Damián Barsoti |
Renato
Cherini
Sergio Giro |