Especificación y análisis de sistemas de tiempo real en teoría de tipos. Caso de estudio : the railroad crossing example

Abstract

Para el análisis de sistemas reactivos y de tiempo real dos importantes enfoques formales se destacan: la verificación de modelos, o model checking, y el análisis deductivo basado en asistentes de pruebas. El primero se caracteriza por la automaticidad pero presenta dificultades al tratar con sistemas que involucran un gran número de estados o donde se tienen parámetros variables, no acotados. El segundo permite tratar con sistemas que involucran un gran número de estados o donde se tienen parámetros variables, 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 Kromos 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. 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 ("the railroad corssing example"). Este problema es utilizado para evaluar y validar algunas de las formalizaciones propuestas.