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

Content Provider	Semantic Scholar
Author	Andreu, Pita Isabel, María
Copyright Year	2012
Abstract	Las tecnicas de especificacion formal de sistemas concurrentes pueden agruparse en general en dos niveles; en el primero se incluyen las tecnicas consistentes en el desarrollo de modelos formales del sistema y en el segundo las tecnicas que realizan la especificacion del sistema mediante la definicion de propiedades abstractas del mismo. El objetivo de esta tesis es proponer una metodologia de especificacion de sistemas que cubra ambos niveles de especificacion mediante el uso de un marco matematico uniforme, proporcionado por la logica de reescritura y su implementacion via el metalenguaje Maude. La especificacion en el primer nivel se realizara directamente en el propio lenguaje Maude, mientras que para realizar la especificacion de segundo nivel definiremos una logica 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 logica. La logica definida puede utilizarse ademas mediante la definicion de la interfaz apropiada para probar propiedades especificas en otras logicas temporales o modales. En la tesis se estudian en primer lugar las especificaciones en el lenguaje Maude. Mediante el desarrollo de una especificacion de un modelo orientado a objetos para redes de telecomunicacion de banda ancha se muestra el poder del lenguaje para especificar este tipo de sistemas y en particular la relacion de herencia, la relacion del contenido y las relaciones explicitas de grupo (ser-miembro-de, cliente-servidor, ..). Se estudia el uso de la reflexion en el control de un proceso de modificacion de caracteristicas de la red. En este sentido se combinan ideas del campo de la reflexion logica con ideas provenientes del campo de la reflexion orientada a objetos mediante el uso de un mediador, un metaobjeto que vive en el metanivel y que tiene acceso a la configuracion de la red para su gestion. En segundo lugar se procede a la definicion de la logica modal Verificacion Logic for Rewriting Logic (VLRL). La principal caracteristica de esta logica es que proporciona dos modalidades, una de ellas una modalidad de accion que permite capturar las reglas de reescritura como acciones de la logica, y la otra modalidad espacial que permite definir propiedades sobre partes del sistema y relacionarlas con propiedades del sistema completo asi como definir propiedades sobre acciones realizadas en partes del sistema. La logica VLRL permite ademas probar propiedades definidas en otras logicas modales o temporales mediante la definicion de la interfaz apropiada. Se muestra el uso de la logica en la prueba de propiedades de seguridad de varios sistemas orientados a objetos: un protocolo de exclusion mutua, el sistema del mundo de los bloques y el sistema Mobile Maude como modelo de movilidad de objetos entre procesos. Por ultimo se muestra otro medio de probar propiedades de sistemas especificados en logica de reescritura mediante un ejemplo en el que se realiza una prueba semi-formal por induccion de propiedades de seguridad y vivacidad del protocolo para la eleccion de lider del bus en serie multimedia IEEE 1394
File Format	PDF HTM / HTML
Alternate Webpage(s)	http://exordio.qfb.umich.mx/archivos%20PDF%20de%20trabajo%20UMSNH/Leer%20escribir%20PDF%202014/Tesis%20espa%C3%B1olas%202012/tesis%20dos/ucm-t26375.pdf
Alternate Webpage(s)	http://exordio.qfb.umich.mx/archivos%20PDF%20de%20trabajo%20UMSNH/tesis/tesis%20dos/ucm-t26375.pdf
Language	English
Access Restriction	Open
Content Type	Text
Resource Type	Article