Resumen de Corrección de programas y redes de Petri de alto nivel

Fernando Tricas García , Francisco Javier Martínez Rodríguez

• La necesidad de utilizar técnicas formales para la especificación de programas concurrentes es fácilmente justificable debido a la complejidad inherente al diseño de este tipo de programas. Las redes de Petri son una herramienta bien conocida para el modelado y la validación de sistemas concurrentes, utilizándose principalmente para el estudio de la parte de control de los mismos. En este trabajo se propone el uso de las técnicas de demostración formal de la corrección de programas concurrentes descritos mediante redes de Petri de alto nivel aprovechando resultados de la teoría estructural de redes de Petri. Para esto, se utilizan las redes de Petri no solamente para representar la parte de control del programa, sino también los datos relevantes en los cálculos que éste realiza.