Desde especificaciones lógicas de intervalos a autómatas de propiedaduna construcción tableau para su aplicación en comprobación de modelos on-the-fly

Zusammenfassung

Este trabajo constituye el punto de partida para la verificación automática de sistemas mediante comprobación de modelos on-the-fly, especificando los requisitos o propiedades temporales que el sistema debe cumplir con fórmulas de una lógica de intervalos, que nos permite razonar a nivel de intervalos de tiempo en lugar de instantes, Las lógicas temporales de intervalos permiten especificar formalmente los requisitos o propiedades temporales de sistemas complejos, como son los sistemas reactivos, en general, y los concurrentes, en particular, en cuyo estudio y análisis se centra nuestro interés. La ventaja de este tipo de lógicas, frente a las lógicas temporales tradicionales, es que permiten establecer de forma sucinta el contexto temporal en el que ciertos requisitos deben aplicarse, haciendo posible una especificación más concisa y comprensible de las propiedades a verificar, especialmente de aquéllas más complejas. Uno de los objetivos actuales de la comunidad científica consiste en intentar que las técnicas de especificación formal sean más fáciles de entender para un grupo cada vez más amplio de personas que tienen responsabilidad en el proceso de desarrollo de software. Una posible manera de alcanzar dicho objetivo sería adoptar un lenguaje de descripción basado en una lógica temporal que soporte una representación gráfica semánticamente equivalente a las de sus fórmulas textuales. Hemos adoptado la lógica temporal de intervalos denomindada Future Interval Logic (FIL), ya que esta lógica cuenta con una representación gráfica muy natural e intuitiva, que hace que las especificaciones sean más fáciles de desarrollar y de comprender, incluso para aquellas personas involucradas en el desarrollo de software que no tengan una buena formación matemático-lógica. Por tanto, constituye la base sobre la que se pueden construir herramientas software amigables para el razonamiento formal acerca de las