Modeling and verifying NLSR protocol of NDN for CPS 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. The features of NDN, including name-based data and in-network caching, make it a promising Internet architecture for cyber-physical systems (CPSs). Named-Data Link State Routing (NLSR) protocol is the routing protocol for NDN, which is designed to disseminate link state advertisements (LSAs) to both build a network topology and distribute all the name prefixes to every node in the network. In this paper, we make the very first attempt to formally model and verify some fundamental properties of the NLSR protocol using model checker UPPAAL. We validate the NLSR protocol modeled into timed automata with simulator in UPPAAL. We verify our model with four fundamental properties (termination, reachability of Sync Interest, reachability of Sync Data, and digest synchronization). The first synchronization problem is found in a scenario with two nodes topology. We give the improved model that owns a valid result in digest synchronization verification. To capture more problems, we make the model to support the simulation of temporary network crash. The second synchronization problem is also exposed in two comparative scenarios. We also propose a mechanism implemented in our model, which has a valid result in digest synchronization verification. We hope that our study and preliminary results would help enhancing the adaptability and robustness of NLSR protocol.