Los sistemas de tiempo-real son sistemas en los cuales el tiempo juega un rol fundamental. Ejemplos de estos sistemas son los controles automáticos de navegación de aviones, los protocolos de comunicación, los procesos industriales automatizados, cajeros automáticos, controladores de radar, etc. El carácter crítico, en más de un sentido, de esta clase de sistemas ha evidenciado la necesidad de proveer métodos formales para su especificación y posterior verificación. Además, su creciente complejidad y tamaño justifica el desarrollo de herramientas que ayuden a su concepción y que automaticen su verificación.
El objetivo de este proyecto está vinculado al desarrollo de herramientas para la verificación automática de sistemas de tiempo-real. Utilizaremos como marco de nuestro trabajo la herramienta KRONOS [BDMOTY98] (en la que uno de los autores ha trabajado desde 1992) estudiando métodos que permitan ampliar sus funcionalidades y mejorando algorítmicamente las técnicas utilizadas hasta el presente.