Resumen de Introducción de métodos formales aplicados al diseño de sistemas electrónicos basados en vhdl
Serafín Olcoz Yanguas 
En el primer capitulo de esta tesis se ha presentado el estado del arte del diseño electronico y se ha puesto especial enfasis en la tendencia a su automatizacion y al uso de estandares. Esta tendencia lleva a emplear como medio de diseño los denominados lenguajes de descripcion de hardware, que tambien van camino de la estandarizacion. En particular destaca el lenguaje VHDL, al que esta integramente dedicado el segundo capitulo. Este capitulo muestra su semantica operacional en base no solo a su ejecucion por medio de un simulador, sino definiendo un modelo intermedio basado en procesos comunicantes que puede ser ejecutado directamente por un ordenador. Este modelo se ha formalizado empleando para ello redes de Petri coloreadas. En el tercer capitulo de esta tesis se ha justificado la eleccion de este modelo formal, asi como se han descrito todos y cada uno de los aspectos que son necesarios para la ejecucion de una descripcion VHDL. Tanto es asi que, si se animase la representacion en CPNs de una determinada descripcion VHDL, se podrian obtener los mismos resultados que los que ofreceria un simulador VHDL. A este fin se ha dedicado el tercer capitulo, que culmina presentando la representacion completa en CPNs de un ejemplo sencillo en VHDL. Sin embargo, el esfuerzo por obtener un modelo formal de una descripcion VHDL no era unicamente la posibilidad de simulacion sobre un soporte formal, sino que es el uso de dicho soporte formal para la aplicacion de tecnicas formales de analisis que pueden complementar a la simulacion VHDL y que tambien tienden un puente hacia la aplicacion de tecnicas que permitan la verificacion formal de un diseño. Por ello, el cuarto y ultimo capitulo de esta tesis presenta la extension de un framework para herramientas basadas en VHDL, de modo que se puedan integrar las herramientas que posibiliten la aplicacion de las tecnicas formales al diseño electronico. Como muestra de su viabilidad, este capitulo presenta el analisis de descripciones VHDL en las que, por medio de la aplicacion de las tecnicas de analisis propias de las redes de Petri, se detectan y se corrigen (siempre en terminos de VHDL) los errores que dichas descripciones presentan. Con el desarrollo del modelo formal de VHDL en redes de Petri, este trabajo ha tendido un puente entre dos mundos, el de los diseñadores de sistemas electronicos basados en VHDL y el de quienes desarrollan tecnicas de analisis para redes de Petri, cuya utilizacion se augura muy fructifera para ambos.
