Evaluation of model checkers SPIN AND UPPAAL for testing wireless sensor network routing protocols

Abstract

Formal modeling and verification has been under consid-erable attraction of researchers these days. Using formal methods one can find bugs and hidden errors in different systems, codes and protocols. As formal models can detect worst case scenarios which are not possible in computer simulations and other testing techniques, they are often employed by researchers to detect flaws in security protocols. A lot of hidden errors have been detected in encryption techniques and secure routing protocols by analyzing them using formal modeling and verification. Although many tools have been developed to perform formal verification; but SPIN and UP-PAAL are most frequently used by researchers to demonstrate some previously unreported weaknesses. This paper analyzes these two model checkers in terms of learning time, ease of use and their features of modeling and verification. We later annotate our findings by applying these tools against a wire-less sensor network routing protocol. We claim that our paper can help future researchers to decide which formal modeling tool is best in a particular scenario thus saving a lot of time in decision making.