Teoría y Herramientas para la Construcción de Software Crítico

Los sistemas críticos están presentes en una cantidad creciente de ámbitos de aplicación incluyendo la industria electrónica, el control industrial, la robótica, la industria aeronáutica y aerospacial, la bio-ingeniería, la medicina, etc. Se trata, en general, de aplicaciones de software que sostienen los productos y procesos de las industrias modernas e infraestructuras estratégicas. Por ende, una falla en estos sistemas puede poner en riesgo vidas humanas o implicar graves perdidas económicas. Es vital capturar precisamente sus requerimientos y asegurar que sean estrictamente cumplidos.

Un camino prometedor para facilitar la construcción y el análisis riguroso de este tipo de sistemas es la verificación asistida por computadora (CAV). La misma ha sido un área de investigación de intensa actividad en ciencias de la computación durante los últimos diez años y se ha convertido en un puente de fertilización de ideas entre esta disciplina y las ingenierías involucradas en el desarrollo de sistemas complejos. Una línea especialmente exitosa dentro de la CAV ha sido el modelchecking, en particular como asistencia al desarrollo de circuitos y protocolos.

En este trabajo se plantea el desarrollo teórico, diseño, implementación e integración de herramientas originales que constituyan componentes para un análisis automático de aspectos de control y tiempo real de software. Particularmente, se intentará atacar las limitaciones de usabilidad y escalabilidad de técnicas basadas en modelchecking para el desarrollo de software complejo como el descripto.

Este proyecto fue financiado por el FONCYT (ANPCyT). Comenzó en el 2006 y se extendió por tres años.

Equipos participantes

Grupo Responsable