Tesis:
Diseño formal orientado a hardware de sistemas telemáticos: De LOTOS a VHDL
- Autor: MARIN LOPEZ, Andrés
- Título: Diseño formal orientado a hardware de sistemas telemáticos: De LOTOS a VHDL
- Fecha: 1996
- Materia: CIENCIAS TECNOLÓGICAS. Teseo;TECNOLOGÍA DE ORDENADORES. Teseo;DISEÑO LÓGICO. Teseo
- Escuela: E.T.S. DE INGENIEROS DE TELECOMUNICACION
- Departamentos: INGENIERIA DE SISTEMAS TELEMATICOS
- Acceso electrónico:
- Director/a 1º: DELGADO KLOOS, Carlos
- Resumen: En esta tesis se propone el uso de una metodología basada en los lenguajes LOTOS y VHDL y en herramientas de diseño automáticas para el diseño de sistemas telemáticos y aplicaciones orientadas a control. La metodología propone realizar especificaciones mediante refinamientos sucesivos. Dichas especificaciones han de ser validadas con respecto a una especificación formal de requisitos del sistema. Las implementaciones en VHDL sintetizable se obtienen por traducción automática. La traducción se demuestra que es correcta siempre de forma que no es preciso verificarla en cada diseño. A partir de esta descripción VHDL se utilizan las herramientas de síntesis automáticas. En el desarrollo de esta tesis se describe la traducción de LOTOS a VHDL y la demostración formal de que es correcta. Debido al gran número de demostraciones intermedias que comporta esta demostración, se decide implementar las semánticas de ambos lenguajes, de la traducción y de la función de correspondencia de estados VHDL a estados LOTOS en un lenguaje funcional de evaluación perezoso llamado Gofer. Todas las demostraciones son automatizables en Gofer