Tesis doctoral de José Alberto Verdejo López
La lógica de resscritura, 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ántica 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
Datos académicos de la tesis doctoral «Maude como marco semántico ejecutable«
- Título de la tesis: Maude como marco semántico ejecutable
- Autor: José Alberto Verdejo López
- 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: Frutos escrig david de
- Fernando Orejas valdés (vocal)
- José Meseguer guaita (vocal)
- Francisco Javier Duran muñoz (vocal)