Statistical Model Checking of Opportunistic Network Protocols

Simulations and test bed experiments have been the mainstay for analysis of routing algorithms in computer networks. In isolation, these approaches are not amenable to more detailed analyses. For example, it is difficult to check protocols against intricate properties specified as statements in a formal logic. It is therefore natural to turn to the rich and mature theory of model checking for the purpose. Indeed, model checking tools and techniques have been applied in the past for analyzing a variety of deterministic and stochastic systems. In this paper, we use statistical model checking to analyze properties and performance of opportunistic network routing protocols. While previous works have largely focused on model checking specific protocols (e.g. in wireless mesh networks), we explore the possibility of generic analysis by linking a statistical model checker with a discrete event simulator for opportunistic networks. This allows statistical model checking of several opportunistic network protocols. We illustrate the approach through a comparison of various protocols against several model checking queries.