Resumen de Abstract interpretation techniques for the verification of timed systems
Robert Clarisó Viladrosa
En muchos sistemas, la corrección se puede decidir comparando las respuestas a eventos del entorno con las descritas en la especificación, En otros dominios, la corrección no sólo depende de qué respuestas se produzcan, sino también de cuando. La especificación de estos sistemas, llamados sistemas temporizados, contiene información temporal como los retardos de las acciones internas y sucesos del entorno. Este concepto se puede generalizar en sistemas temporizados paramétricos, donde parte de la información temporal en la especificación es un parámetro del sistema. Verificar un sistema con parámetros consiste en determinar el conjunto de valores aceptables para estos parámetros que garantizan un funcionamiento correcto. Sin embargo, muchas versiones de este problema de verificación son computacionalmente costosas o incluso indecidibles.
Una clase importante de sistemas temporizados son los circuitos temporizados, un estilo de diseño orientado a construir circuitos de alta velocidad.
Un circuito temporizado consigue un buen rendimiento, pero su corrección sólo esta garantizada si los retardos de sus puertas y cables satisfacen un conjunto de restricciones de tiempo. Por otro lado, los diseñadores de un circuito temporizado tienen algún control sobre esos retardos. Formalizar el circuito cómo un sistema temporizado paramétrico permite retrasar la elección de esos retardos hasta después de verificar. Entonces, los retardos pueden seleccionarse acorde con las restricciones impuestas por la verificación, evitando decisiones conservadores a priori. Una buena elección de retardos puede mejorar la eficiencia de un circuito, p.ej., reduciendo su latencia.
Esta tesis estudia la verificación de sistemas temporizados paramétricos, con atención especial al dominio de los circuitos temporizados. Los métodos propuestos se basan en la teoría de interpretación abstracta, un método general para el análisis estático usad
