Model checking of strategy-controlled systems in rewriting logic

Resumen

En la ingenería informática, los métodos formales son técnicas matemáticamente rigurosas y en parte automatizables para desarrollar y verificar el correcto funcionamiento de sistemas hardware y software. Habitualmente restringidos al análisis de sistemas críticos, su aplicación se ha popularizado con el avance de las técnicas y se ha extendido también a otras disciplinas. Una verificación formal automatizada necesita lenguajes precisos y expresivos para describir el funcionamiento del sistema y sus propiedades en cuestión, junto con algoritmos que comprueben o ayuden a comprobar si estas se satisfacen. La lógica de reescritura, propuesta por Meseguer en 1992 como un marco unificado para especificar sistemas concurrentes, es un ejemplo de ello. Los estados del sistema se modelan como términos en una lógica ecuacional y los cambios de estado se describen mediante reglas que reescriben esos términos. Las especificaciones en lógica de reescritura no son meros modelos abstractos, sino que son ejecutables y analizables en lenguajes de especificación como Maude. Una ejecución es una sucesión de pasos de reescritura independientes, en los que una regla cualquiera se aplica en una posición cualquiera del término obtenido en el paso anterior. Esa localidad espacial y temporal es lo que confiere el carácter no determinista y concurrente del modelo. Sin embargo, en ocasiones es conveniente considerar solo algunas de las posibles ejecuciones del sistema limitando la aplicación de las reglas, bien sea por eficiencia o para expresar restricciones con valor semántico propio. El recurso fundamental para expresar esas restricciones sin alterar el sistema de reglas y estados son las estrategias de reescritura. Las estrategias son un concepto omnipresente en la informática desde sus orígenes. En la lógica de reescritura, estas se han expresado tradicionalmente en el propio lenguaje debido a su caracter reflexivo. Sin embargo, para facilitar su uso se propuso un lenguaje de estrategias propio para Maude en la línea de otros lenguajes del momento como ELAN y Stratego. Incluido como un nivel superior de especificación en Maude, permite desagregar la lógica del sistema de su control. En la primera parte de esta tesis se ha finalizado la implementación de este lenguaje, se han estudiado múltiples extensiones del mismo y se ha aplicado a la especificación formal de diversos ejemplos relacionados con lenguajes de programación, protocolos de comunicación, juegos, modelos computacionales y biológicos, etc. La comprobación de modelos es una técnica de verificación basada en el análisis exhaustivo de las ejecuciones del modelo, esencialmente representado como un máquina de estados y transiciones etiquetados con diversas proposiciones atómicas. En base a ellas se expresan las propiedades de su comportamiento que se quieren comprobar, habitualmente mediante lógicas temporales. En este contexto es natural considerar estrategias que restrinjan las ejecuciones del modelo y plantearse cómo esto afecta a la satisfacción de las propiedades deseadas. En esta tesis hemos estudiado el problema de la comprobación de modelos para sistemas controlados por estrategias y en particular para aquellos controlados por el lenguaje de estrategias de Maude. Su intérprete dispone de un comprobador de modelos integrado para sistemas de reescritura y propiedades en lógica temporal lineal, que hemos extendido para tener en cuenta las restricciones de las estrategias. Además hemos desarrollado conexiones con comprobadores externos para verificar propiedades en otras lógicas temporales como CTL* y el mu-cálculo y calcular propiedades cuantitativas en sistemas probabilísticos. Finalmente, todo ello ha sido utilizado para comprobar propiedades interesantes en diversos ejemplos especificados con estrategias.