Quantitative Verification of Zeroconf Protocol Based on Stochastic Games

Zeroconf protocol provides a solution to automatic IP address configuration. This paper focuses on quantitative performance analysis of zeroconf protocol. The analysis process contains two phrases: model construction and property verification. Since there exists competition relation among the hosts and their behaviors exhibit stochastic features, it is natural to model zeroconf protocol as turn-based stochastic game. Due to the absence of some necessary details of the original protocol, this paper also makes some assumptions about the model. The successful configuration probability and time cost are the most important concern of this protocol. This paper verifies maximum and minimum successful and unsuccessful configuration probabilities within certain periods. On the other hand, this paper also considers time cost to reach successful configuration. Experiments are performed with the tool PRISM-game which is for modeling and verification of stochastic games. Experimental results show that when the number of host is no more than 40,000, the performance of this protocol tends to be stable and when N is greater than 40,000, both the expected time cost for successful configuration and conflict probability will grow prominently.