Modeling the UPnP-UP protocol using Coloured Petri Nets

UPnP defines an architecture for pervasive peer-to-peer network connectivity of intelligent appliances, wireless devices, and PCs of all form factors and platforms. It is designed to support zero-configuration, ldquoinvisiblerdquo networking, and automatic discovery for a breadth of device categories from a wide range of vendors. UPnP-UP is an extension of the UPnP protocol that provides support to customized services in UPnP networks. This paper presents the modeling of the UPnP-UP protocol using Coloured Petri Nets (CPN). CPN have a graphical representation and a well-defined semantics allowing formal analysis and verification of systems.