Java/PROSEGA: Extensión de CPN Tools para la generación de lenguajes de autómatas y la reducción de grafos de estado a máquinas de estado finito.

Abstract

Las Redes de Petri Coloreadas son un lenguaje gráfico que permite modelar de una manera formal sistemas concurrentes a eventos discretos. Las Redes de Petri Coloreadas proveen una técnica poderosa de análisis mediante Grafos de Estado. En particular, CPN Tools es una de las herramientas, utilizadas por diversos investigadores y otros proyectos, para la construcción de Redes de Petri Coloreadas y el análisis de sistemas mediante Grafos de Estado. Este trabajo desarrolla, dentro de CPN Tools, un software denominado Java/PROSEGA que se encarga de reducir, a partir de algoritmos ya conocidos, los Grafos de Estado de los modelos CPN a Máquinas de Estado Finito, de manera de proveer un entorno para el análisis de sistemas concurrentes. Además, el software provee funcionalidades para la generación del lenguaje de autómatas, y también permite realizar comparaciones entre autómatas utilizando funciones de diferencia. Adicionalmente, este trabajo contempla un estudio sobre las técnicas formales en las cuales se basa el software Java/PROSEGA, así como también realiza un estudio sobre las herramientas de software utilizadas, para llevar a cabo dichas tareas de reducción de autómatas y generación del lenguaje. Para llevar a cabo las pruebas sobre el software, se utiliza como caso de estudio un trabajo de verificación del protocolo de comunicación IEEE 802.16, específicamente su proceso de gestión de conexiones a nivel de capa MAC.