Modelling and Verification of CoAP over Routing Layer Using SPIN Model Checker

Many of the communication protocols developed for the resource constrained devices are rarely subjected to protocol verification. Design flaws like deadlocks, livelocks, non-progressive cycles etc. may come into view during the realization and can cause catastrophic effects in safety-critical applications. Formal specification of the protocol represented as a model helps to describe and analyse the conformability of the implementation to its specification and subsequently reveal design flaws, if any in the system. The formal model is subject to verification by inserting correctness and safety properties of the protocol and validating logical correctness using a model checking tool. All model checkers suffer from state explosion problem due to enormous states of the model being created. The key contribution of the present work is the introduction of a method to develop a compact verification model which is amenable to full state space search by abstracting the key elements of a protocol. Moreover, many protocol verification works presented in the existing literature consider only a single layer of a communication protocol. To correctly model the overall behaviour of a protocol, interactions between the layers have to be incorporated. The proposed method has been proven useful by considering verification of an application protocol, CoAP for constrained devices by abstracting out the aspects of the underlying routing protocol RPL. Reliable message exchanges among various entities are modeled and its safety and correctness properties were analysed and verified. The results obtained show that the model performs the full state space search by considering all possible routing paths and are free from design flaws. The method described has been implemented by building a validation model in PROMELA and the model is verified by using SPIN model checker. The methodology used in this paper can be used to verify any application layer protocol for constrained devices in IoT scenario that run on top of routing layer.