UPnP (Universal Plug and Play) is an industry standardization initiative undertaken by the UPnP Forum to ``enable simple and robust connectivity among stand-alone devices and PCs from different vendors''. Typical environments for UPnP technology are homes and offices where devices communicate with wireless communication. In these networks topology changes happen frequently and UPnP should contain facilities to efficiently and robustly deal with this. To that end, Philips has proposed a liveness protocol for the quick detection which devices are still on the network, and which are not. The protocol should, however, not overload the devices by flooding them with messages. Several stochastic phenomena play an important role for the liveness protocol, such as message loss, random delays, and random behaviour of devices joining and leaving the network.
Since the summer of 2003 we are using MoDeST for the formal description and analysis of the liveness protocol. Although this work has not yet been completed, it is interesting to report that some undesired phenomena in the liveness protocol have been discovered by discrete-event simulation of the MoDeST specification (using the Motor-Möbius interface). In particular, it has been shown that under certain circumstances, the system may reach an undesired equilibrium where certain control points check devices in a fast way whereas others have a rather low frequency of checking, and the system is not able to recover from this situation .
Henrik Bohnenkamp 2004-05-06