Applying Formal Methods To Gossiping Networkswith Mcrl And Groove

摘要

In this paper we explore the practical possibilities of using formal methods to analyze gossiping networks. In particular, we use uCRL and Groove to model the peer sampling service, and analyze it through a series of model transformations to CTMCs and finally MRMs. Our tools compute the expected value of various network quality indicators, such as average path lengths, over all possible system runs. Both transient and steady state analysis are supported. We compare our results with the simulation and emulation results found in [10].