Técnicas de especificación formal de sistemas orientados a objetos basadas en lógica de reescritura

Abstract

Las técnicas de especificación formal de sistemas concurrentes pueden agruparse en general en dos niveles; en el primero se incluyen las técnicas consistentes en el desarrollo de modelos formales del sistema y en el segundo las técnicas que realizan la especificación del sistema mediante la definición de propiedades abstractas del mismo. El objetivo de esta tesis es proponer una metodología de especificación de sistemas que cubra ambos niveles de especificación mediante el uso de un marco matemático uniforme, proporcionado por la lógica de reescritura y su implementación vía el metalenguaje Maude. La especificación en el primer nivel se realizará directamente en el propio lenguaje Maude, mientras que para realizar la especificación de segundo nivel definiremos una lógica modal para probar propiedades de sistemas especificados en Maude, en la cual las transiciones definidas por las reglas de reescritura se capturan como acciones en la lógica. La lógica definida puede utilizarse además mediante la definición de la interfaz apropiada para probar propiedades específicas en otras lógicas temporales o modales. En la tesis se estudian en primer lugar las especificaciones en el lenguaje Maude. Mediante el desarrollo de una especificación de un modelo orientado a objetos para redes de telecomunicación de banda ancha se muestra el poder del lenguaje para especificar este tipo de sistemas y en particular la relación de herencia, la relación del contenido y las relaciones explícitas de grupo (ser-miembro-de, cliente-servidor, ..). Se estudia el uso de la reflexión en el control de un proceso de modificación de características de la red. En este sentido se combinan ideas del campo de la reflexión lógica con ideas provenientes del campo de la reflexión orientada a objetos mediante el uso de un mediador, un metaobjeto que vive en el metanivel y que tiene acceso a la configuración de la red para su gestión. En segundo lugar se procede a la definición de la lógica modal Verificación Logic for Rewriting Logic (VLRL). La principal característica de esta lógica es que proporciona dos modalidades, una de ellas una modalidad de acción que permite capturar las reglas de reescritura como acciones de la lógica, y la otra modalidad espacial que permite definir propiedades sobre partes del sistema y relacionarlas con propiedades del sistema completo así como definir propiedades sobre acciones realizadas en partes del sistema. La lógica VLRL permite además probar propiedades definidas en otras lógicas modales o temporales mediante la definición de la interfaz apropiada. Se muestra el uso de la lógica en la prueba de propiedades de seguridad de varios sistemas orientados a objetos: un protocolo de exclusión mutua, el sistema del mundo de los bloques y el sistema Mobile Maude como modelo de movilidad de objetos entre procesos. Por último se muestra otro medio de probar propiedades de sistemas especificados en lógica de reescritura mediante un ejemplo en el que se realiza una prueba semi-formal por inducción de propiedades de seguridad y vivacidad del protocolo para la elección de líder del bus en serie multimedia IEEE 1394