Maude como marco semántico ejecutable

Tesis doctoral de Alberto Verdejo

Dirigida por Narciso Martí Oliet

Resumen

La lógica de reescritura, propuesta por José Meseguer en 1990 como marco de unificación de modelos de computación concurrente, es una lógica para razonar sobre sistemas concurrentes con estado que evolucionan por medio de transiciones. Desde su definición, se ha propuesto a la lógica de reescritura como marco lógico y semántico en el cual poder expresar de forma natural otras muchas lógicas, lenguajes y modelos de computación. Además, la lógica de reescritura es ejecutable utilizando el lenguaje multiparadigma Maude cuyos módulos son teorías en la lógica de reescritura.

El objetivo principal de esta tesis es extender la idea de la lógica de reescritura y Maude como marco semántico a la idea de marco semántico ejecutable. Este objetivo se ha abordado desde diferentes puntos de vista.

En primer lugar, presentamos representaciones ejecutables de semánticas operacionales estructurales. En concreto, hemos estudiado dos implementaciones diferentes de la semántica de CCS y su utilización para implementar la lógica modal de Hennessy-Milner; hemos realizado una implementación de una semántica simbólica para LOTOS incluyendo especificaciones de tipos de datos en ACT ONE que son traducidos a módulos Maude y de una herramienta que permite al usuario ejecutar directamente sus especificaciones LOTOS; y hemos utilizado las mismas técnicas para implementar otros tipos de semánticas operacionales de lenguajes funcionales e imperativos sencillos, incluyendo tanto semánticas de evaluación (o paso largo) como semánticas de computación (o paso corto).

En segundo lugar, hemos querido contribuir al desarrollo de una metodología propuesta recientemente por Denker, Meseguer y Talcott para la especificación y análisis de sistemas basada en una jerarquía de métodos incrementalmente más fuertes, especificando y analizando tres descripciones ejecutables del protocolo de elección de líder dentro de la especificación del bus multimedia en serie IEEE 1394 (conocido como ``FireWire''). En dos de estas descripciones hacemos especial énfasis en los aspectos relacionados con el tiempo, esenciales para este protocolo.

Por último, hemos abordado la dotación de semántica formal a lenguajes de la web semántica, mediante la traducción del lenguaje de descripción de recursos web RDF (Resource Description Framework) a Maude y su integración con Mobile Maude, una extensión de Maude para permitir cómputos móviles.

tesis.pdf (1.6M)

Código Maude

Capítulo 2

2.2.1   PATH.maude Contiene el módulo PATH y los ejemplos de reducción.
2.2.2 A-TRANSITION-SYSTEM.maude   Contiene un sistema de transiciones mediante reescrituras.
SORTING.maude Contiene el módulo de ordenación de vectores de enteros.
2.2.4 META-MODULES.maude Contiene un módulo funcional y un módulo de sistema metarepresentados, y ejemplos de reducciones al metanivel.
2.2.5 STRATEGY.maude Contiene el lenguaje de estrategias descrito en esta sección, y ejemplos de reducción.
2.2.6 DUPLICATE-TEN.maude Contiene un ejemplo de utilización del LOOP-MODE.
2.3.1 ACCNT.fm Contiene módulos orientados a objetos con la clase Accnt y su subclase SavAccnt.
2.3.2 PRG-PARAM.fm Contiene ejemplos de módulos paramétricos en Full Maude.
2.3.3 META-NAT.fm Contiene ejemplos de reducciones al metanivel utilizando Full Maude.
2.4 PATH.maude2 Contiene el módulo PATH en Maude 2.0.
META-NAT.maude2 Contiene un módulo metarepresentado con la nueva sintaxis al metanivel de Maude 2.0, y ejemplos de reducciones al metanivel con las nuevas operaciones de descenso.

Capítulo 3

3.3   eval-exp4-jdgm.maude   Contiene la representación de la semántica de evaluación del lenguaje Exp4 siguiendo el enfoque de reglas de inferencia como reescrituras.
3.4   eval-exp4-crl.maude2 Contiene la representación en Maude 2.0 de la semántica de evaluación del lenguaje Exp4 siguiendo el enfoque de transiciones como reescrituras, y los ejemplos de ejecución.

Capítulo 4

CCS1.fm   Contiene las representaciones de la semántica de CCS y de la lógica modal de Hennessy-Milner siguiendo el enfoque de reglas de inferencia como reescrituras, y la estrategia definida al metanivel que las hace ejecutables.
testsCCS1.fm   Contiene los ejemplos de ejecución de este capítulo.
CCS-Isabelle.thy   Contiene las teorías de Isabelle que representan la semántica de CCS y de la lógica modal de Hennessy-Milner.

Capítulo 5

CCS2.maude2   Contiene la representación de la semántica de CCS siguiendo el enfoque de transiciones como reescrituras y la representación ecuacional de la lógica modal de Hennessy-Milner.
testsCCS2.maude2   Contiene los ejemplos de ejecución de este capítulo.

Capítulo 6

6.1.1   fpl-eval-cbv.maude2   Contiene la semántica de evaluación de Fpl con llamada por valor.
   fpl-eval-cbv-NAT.maude2   Contiene la semántica de evaluación de Fpl con llamada por valor utilizando los números naturales predefinidos de Maude.
   fpl-eval-cbn.maude2   Contiene la semántica de evaluación de Fpl con llamada por nombre.
6.1.2   fpl-comp.maude2   Contiene la semántica de computación de Fpl.
   fpl-comp-sinsust.maude2   Contiene la semántica de computación de Fpl en la versión en la cual no son necesarias las sustituciones sintácticas.
6.1.3   fpl-abstract-machine.maude2   Contiene la semántica de Fpl basada en una máquina abstracta.
6.2.1   whilel-eval.maude2   Contiene la semántica de evaluación del lenguaje WhileL.
6.2.2   whilel-comp.maude2   Contiene la semántica de computación del lenguaje WhileL.
6.2.2   guardl.maude2   Contiene la semántica de computación del lenguaje GuardL.
6.3   miniML.maude2   Contiene la semántica de evaluación del lenguaje Mini-ML.

Capítulo 7

   LOTOS.maude2   Contiene la representación de la semántica simbólica de Full LOTOS, la traducción de módulos de ACT ONE a Maude, y la implementación de la herramienta para la ejecución de especificaciones Full LOTOS.
7.5.6   testsLOTOS.lotos   Contiene un ejemplo de especificación Full LOTOS y comandos para su ejecución en nuestra herramienta.

Capítulo 8

firewireSync.fm   Contiene la representación del protocolo de elección de líder con comunicación síncrona, la estrategia de exploración exhaustiva de estados, y ejemplos de ejecución.
timedFirewire1.fm   Contiene la primera representación con comunicación asíncrona, la estrategia de exploración exhaustiva de estados, y ejemplos de ejecución.
timedFirewire2.fm   Contiene la primera representación con comunicación asíncrona, la estrategia de exploración exhaustiva de estados, y ejemplos de ejecución.
firewireSync.fm2   Contiene la primera especificación en Full Maude 2.0.
timedFirewire1.fm2   Contiene la segunda especificación en Full Maude 2.0.
timedFirewire2.fm2   Contiene la tercera especificación en Full Maude 2.0.

Capítulo 9

RDF-translation.fm   Contiene la implementación de la traducción de RDF a módulos orientados a objetos en Maude.
RDF-printers.mm   Contiene el código Mobile Maude del ejemplo de las impresoras.