Estrategias para el guiado y la monitorización de la ejecución de sistema en maude

Resumen

Durante la ejecución de un sistema de reescritura es posible llegar a situaciones en las que nos encontramos con diferentes reglas aplicables a un determinado término o diferentes formas de aplicar una determinada regla. Ello hace que sea necesario disponer de estrategias para decidir cómo proceder en la aplicación de las reglas del sistema durante el proceso de reescritura. Hay diferentes alternativas, desde estrategias predefinidas que ya están asociadas a determinados comandos con los que ejecutar el sistema hasta el uso de lenguajes de estrategias con los que especificar cómo controlar la ejecución de un determinado sistema. Maude es un lenguaje basado en lógica de reescritura que soporta adecuadamente las características reflexivas de dicha lógica. Ello proporciona un mecanismo muy potente para controlar el proceso de reescritura y facilita el desarrollo de nuevas estrategias. En esta tesis proponemos nuevas estrategias en Maude con dos objetivos diferentes: ¿ El guiado de la ejecución del sistema mediante estrategias declarativas, garantizando as! que se cumplen determinadas propiedades. ¿ La monítorización de especificaciones de modelos de sistemas orientados a objetos, comprobando si se cumplen determinadas propiedades. El uso de estrategias declarativas facilita el control de la ejecución del sistema en situaciones en las que se desea que una determinada especificación cumpla ciertas propiedades. En dichas situaciones seria posible usar un enroque procedural, actuando sobre la especificación del sistema y modificándola para asegurar que dichas propiedades se cumplen durante la ejecución, o bien usar un enfoque declarativo como ei que proponemos, especificando las propiedades deseadas mediantes fórmulas en alguna lógica adecuada y confiando en que la estrategia declarativa se encargará de controlar la forma de ejecutar el sistema, garantizando así que siempre se cumplirán las propiedades deseadas. Un enfoque declarativo como el propuesto puede simplificar ei diseño del sistema, mejorar su medularidad y facilitar la reutilización y modificación de las especificaciones. El uso de estrategias para controlar las ejecución puede facilitar el desarrollo de herramientas para monitorizar contratos en sistemas orientados a objetos. Pensamos que Maude puede ser un buen candidato como lenguaje en el que obtener un prototipo ejecutable del modelo de un sistema orientado a objetos y que el uso de estrategias para controlar la ejecución puede facilitar la monítorización de los contratos que se imponen en dicho modelo. De esta forma sería posible detectar violaciones de los contratos durante la ejecución del prototipo del modelo, localizando posibles errores en el modelo del sistema, antes de proceder a su implementación final. Proponemos una estrategia genérica para monítorización, que podrá ser utilizada para monitorizar contratos expresados en diferentes formalismos y que hemos aplicado para obtener una herramienta de monítorización de contratos expresados en lenguaje OCL sobre modelos de sistemas descritos en UML. Ei desarrollo de esta herramienta ha requerido disponer de soporte para el lenguaje OCL en Maude, por lo que también se ha desarrollado mOdCL, un evaluador de expresiones OCL para Maude.