Two formal approaches arise as the most used for the analysis of real time systems: model checking and deductive analysis based on proof assistants. The former is characterized by its fully automatization but it presents some difficulties when dealing with systems that involve a great number of states or unbound parameters. The latter, on the other hand, turns out to be appropriate for working with arbitrary systems, though user's interaction is required. This work explores a methodology that combines the use of a model checker like Kronos and the proof assistant Coq for the analysis of real time systems. We specially emphasize the analysis of the railroad crossing example, a case study considered a benchmark by different works in this field.

Para el análisis de sistemas de tiempo real se destacan dos enfoques formales: 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 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 que permite 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. Un especial énfasis es puesto en el análisis de un caso de estudio, considerado como benchmark en diferentes trabajos: el control de un paso a nivel de tren.