Tesis doctoral de Andres Marin Lopez
En esta tesis se propone el uso de una metodología basada en los lenguajes lotos y vhdl y en herramientas de diseño automaticas para el diseño de sistemas tellematicas y aplicaciones orientadas a control. La metodología propone realizar especificaciones mediante refinamientos sucesivos. Dichas especificaciones han de ser validadas con respecto a una especificacion formal de requisitos del sistema. Las implementaciones en vhdl sintetizable se obtienen por traduccion automatica. La traduccion se demuestra que es correcta siempre de forma que no es preciso verificarla en cada diseño. A partir de esta descripcion vhdl se utilizan las herramientas de sintesis automaticas. en el desarrollo de esta tesis se describe la traduccion de lotos a vhdl y la demostracion formal de que es correcta. Debido al gran numero de demostraciones intermedias que comporta esta demostracion, se decide implementar las semanticas de ambos lenguajes, de la traduccion y de la funcion de correspondencia de estados vhdl a estados lotos en un lenguaje funcional de evaluacion perezoso llamado gofer. Todas las demostraciones son automatizables en gofer.
Datos académicos de la tesis doctoral «Diseño formal orientado a hardware de sistemas telematicos: de lotos a vhdl.«
- Título de la tesis: Diseño formal orientado a hardware de sistemas telematicos: de lotos a vhdl.
- Autor: Andres Marin Lopez
- Universidad: Politécnica de Madrid
- Fecha de lectura de la tesis: 01/01/1996
Dirección y tribunal
- Director de la tesis
- Carlos Delgado Kloos
- Tribunal
- Presidente del tribunal: Miguel Moro Tomas De
- Jaime Ruz Jose (vocal)
- Roman Hermida Correa (vocal)
- Eugenio Villar Bonet (vocal)