Modeling and Verification of NLSR Protocol Using UPPAAL

Named Data Networking (NDN) is a new promising architecture of information-centric networking, which supports multicast of data and adopts the publish/subscribe model in the network. NDN could not reuse the existing routing protocols designed for the IP architecture due to their fundamental difference of design. As a result, the Named-data Link State Routing (NLSR) protocol has been proposed for NDN. At the heart of the NLSR protocol is to disseminate Link State Advertisements (LSAs) to both build a network topology and distribute all the name prefixes to every node in the network. Each router stores the latest version of the LSAs in a Link State Database (LSDB). In this paper, we make the very first attempt to formally model and verify a few fundamental properties of the NLSR protocol using UPPAAL, a model checker for modeling and verifying real-time systems as networks of timed-automata. We validate our model by running the simulator in UPPAAL and verify crucial properties of the protocol under simple yet non-trivial test configurations differing in network topologies and message exchanging scenarios. We capture two situations that may risk synchronization failures and discuss some countermeasures. We also testify the proposal by verifying the revised model with addressing the design issues. We hope that our study and preliminary results would help enhancing the adaptability and robustness of NLSR protocol.