Tesis doctoral de Isabel Pita Andreu
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 seg
Datos académicos de la tesis doctoral «Técnicas de especificación formal de sistemas orientados a objetos basadas en lógica de reescritura«
- Título de la tesis: Técnicas de especificación formal de sistemas orientados a objetos basadas en lógica de reescritura
- Autor: Isabel Pita Andreu
- Universidad: Complutense de Madrid
- Fecha de lectura de la tesis: 24/03/2003
Dirección y tribunal
- Director de la tesis
- Narciso Martí Oliet
- Tribunal
- Presidente del tribunal: mario Rodríguez artalejo
- ernesto Pimentel sanchez (vocal)
- José Meseguer guaita (vocal)
- ambrosio Toval álvarez (vocal)