On Designing Provably Correct DODAG Formation Criteria for the IPv6 Routing Protocol for Low-Power and Lossy Networks (RPL)
Agnieszka Paszkowska, Konrad Iwanicki · 2018
Apart from being standardized, an important industrial advantage of the IPv6 Routing Protocol for Low-Power and Lossy Networks (RPL) is the possibilities of completely adapting its route formation criteria. Through largely open routing metrics and route selection delegated to so-called objective functions, RPL's adopters are free to customize the protocol to individual applications, even ones with peculiar requirements. However, these possibilities also pose a major reliability risk: it is not clear whether a given combination of routing metrics, objective function, and RPL's remaining configuration parameters ensures that the resulting routes will be formed correctly when the routing metric values change dynamically. We study this problem here to derive conditions for routing metrics and objective functions under which routing path construction and maintenance can be proved correct. We start with a case study, based on an industrial deployment, that motivates the considered problem. We then formally model and analyze the dynamic behavior of RPL's route formation process in abstraction from particular objective functions and routing metrics. We derive conditions under which this process is provably correct. Finally, we attempt to translate these theoretical conditions into practical guidelines that can be utilized by RPL's adopters who aim at reliable systems.