Modelagem e análise formal de algumas funcionalidades de um protocolo de transporte através das redes de Petri

Abstract

This dissertation presents an approaching for studying, modeling and makes some analysis about functionalities of association of SCTP transport protocol. This protocol has been developed in the last five years by IETF. This protocol achieved a high level of efficiency and it has been considered a probable substitute for TCP and ideal to work with IPv6. The modeling and analysis are developed using a mathematical formalism called Petri nets, which is a tool employed in parallel and concurrent systems and its study is an important part of this work. Some computer implementation of Petri nets formalism called PAREDE and Design/CPN are used. These were chosen because they implement extensions of the Petri net basic theory and make possible its modeling, considering time and color properties, besides implement methods of formal analysis. The SCTP protocol models developed using Petri nets, provide some essential details to perform a functional behavior analysis and specific properties, like absence of deadlocks, synchronization, and correct sequences of messages, besides the SCTP official specification checking of consistency, the RFC2960.