Composition in Rewriting Logic

Abstract

In short, this thesis shows that compositional specification and verification are doable in rewriting logic and in Maude if they are enriched with appropriate extensions. Modularity and compositionality are key features in computer science and engineering. Rewriting logic has proven to be a valuable tool for system modeling (or specification, as it is usually called in this context) but, up to make compositional specification and verification possible in rewriting logic, and to incorporate the resulting ideas into Maude (a language and system based on rewriting logic) so as to make them usable in practice...

En pocas palabras, este 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...