Análisis y verificación del Protocolo para la Reservación de Recursos (RSVP), usando Redes Coloreadas de Petri

Abstract

Redefine y valida la especificación de servicio para Protocolo de Reservación de Recursos (RSVP) destinados a soportar aplicaciones multimedia en tiempo real en la internet. Extiende el nuevo modelo para incluir cambios en la reservación de recursos usando Redes Coloreadas de Petri (CPN), que permite no solamente su aplicación a una versión limitada de RSPV, sino también su implementación en otros protocolos con funcionalidades similares. Ha generado un código en ML que incluye algoritmo de grafos SCC o grafos, en general sin ciclos.