Abstract

The Universal Plug and Play (UPnP) standard is used by a number of companies including Apple, Microsoft, Philips and Sun for communication purposes in highly dynamic domains such as home and business environ- ments. As an improvement to this standard, Philips proposed the liveness protocol that is used to keep track of the status and current reachability of devices in such environments. This protocol has recently been designed and proposed for standardization.

Although initial simulation studies at Philips provide some evidence that the protocol works as intended, several issues still remain unclear. These unclarities are about functionality, timing and reliability. The protocol also has many parameters which influence its overall performance. A good choice for such parameters needs to be determined.

The goal of this assignment is to use modeling techniques to get more insight into the behavior of the protocol. This includes using the traditional tools SPIN and UPAAL, but also the new MoDeST tool, currently under development at the FMT group of the University of Twente. Möbius, a tool-set adopted by for example NASA and Motorola, is used to run simulations of MoDeST specifications.

By analyzing the liveness protocol using these modeling tools, we found unclarities in the protocol description, gained insight into the impact of different parameter values and revealed some weaknesses of the protocol, in particular a fairness problem. This will all be addressed in this report. On top of this, we designed improvements to the liveness protocol using the modeling tools at hand, to overcome these weaknesses.