Para el análisis de sistemas reactivos y de tiempo real dos importantes enfoques formales se destacan: la verificación de modelos y el análisis deductivo basado en asistentes de pruebas. El primero se caracteriza por ser completamente automatizable pero presenta dificultades al tratar con sistemas con un gran número de estados o que tienen parámetros no acotados. El segundo permite tratar con sistemas arbitrarios pero requiere la interacción del usuario.

Este trabajo explora una metodología de trabajo que permita compatibilizar el uso de un verificador de modelos como Kronos y el asistente de pruebas Coq en el análisis de sistemas de tiempo real. Para ello formalizamos grafos (autómatas) temporizados y la lógica TCTL (y CTL) en el cálculo de construcciones inductivas y co-inductivas de Coq, a fin de disponer de lenguajes de especificación y análisis comunes a ambas herramientas. Los grafos permiten describir los sistemas, mientras que la lógica se usa para especificar los requerimientos temporales. Una parte importante del trabajo está dedicada a estudiar cómo razonar deductivamente en Coq sobre esta clase de sistemas –la utilidad de tipos inductivos y la necesidad de tipos co-inductivos– asumiendo inicialmente un modelo de tiempo discreto.