Composición en lógica de reescritura

Abstract

En pocas palabras, esta tesis muestra que la especificación y la verificación composicionales son posibles en lógica de reescritura y en Maude, si se las enriquece con extensiones apropiadas. La modularidad y la composicionalidad son aspectos clave de la informática práctica y teórica. La lógica de reescritura ha demostrado ser una herramienta valiosa para el modelado de sistemas (más bien llamado especificación en este contexto) pero, hasta ahora, no permitía una verdadera modularidad. Nuestro objetivo, por tanto, es hacer que la especificación y la verificación por componentes sean posibles en lógica de reescritura e incorporar las ideas resultantes en Maude (un lenguaje y un sistema basado en lógica de reescritura) para hacerlas útiles en la práctica. Definimos una variante de los sistemas de reescritura que llamamos igualitarios. Ese adjetivo hace referencia a que tratamos igual a los estados y a las transiciones. Propuestas similares se han demostrado convenientes para modelar sistemas y para escribir propiedades temporales; nosotros mostramos que también permite una definición flexible de la composición de sistemas. También definimos una correspondiente variante de las estructuras de transiciones, que usamos como semántica. La sincronización entre componentes se basa en los valores que ciertas funciones toman en los diferentes estados y transiciones de cada sistema. Llamamos propiedades a estas funciones, que no necesitan ser booleanas, sino que pueden ser de cualquier tipo. Las variables compartidas y el intercambio de mensajes no son usados como primitivas para sincronización, aunque pueden ser simulados. La composición de dos sistemas, S1 y S2, lleva como parámetro adicional un conjunto de criterios de sincronización. Cada criterio es un par formado por una propiedad de S1 y otra de S2. La interpretación es que los sistemas S1 y S2 pueden evolucionar de cualquier manera que ellos elijan siempre que los valores de las propiedades, cada una en su sistema, sean iguales durante toda la ejecución. No hay puntos de sincronización especiales: la igualdad entre propiedades debe mantenerse en todo momento. Así, la definición de las propiedades en cada sistema y los criterios de sincronización determinan el resultado de la composición. Una operación que llamamos split traduce un sistema de escritura igualitario y compuesto a uno equivalente que es estándar y monolítico. Y otra operación con el mismo nombre traduce sistemas de transición igualitarios a otros estándar. Demostramos que hay una relación, dada por la operación split, entre la semántica habitual para sistemas de reescritura (dada por estructuras de Kripke) y nuestra semántica para sistemas de reescritura igualitarios (dada por estructuras de transiciones igualitarias). En lo que respecta a la verificación, mostramos cómo la simulación y la abstracción pueden ser realizadas por componentes, y adaptamos la técnica asume/garantiza a nuestras propuestas. Esto proporciona posibles maneras de mitigar el problema de la explosión de estados. La operación split es también útil aquí: sobre una especificación composicional se puede llevar a cabo una verificación composicional pero también, alternativamente, se puede efectuar verificación monolítica sobre el resultado de aplicarle el split. Proponemos extensiones a la sintaxis de Maude para definir propiedades, sincronización y el resto de nuestras construcciones teóricas. Hemos desarrollado un prototipo de software que genera código Maude estándar cuando se le alimenta con una especificación composicional escrita con nuestra sintaxis extendida. Es, por tanto, una implementación de la operación split. De esta manera, las herramientas de análisis que forman parte del sistema Maude pueden ser usadas. Una discusión de los detalles interesantes de la implementación y unos cuantos ejemplos completan el texto.