Testing methodology for an ad hoc routing protocol

ABSTRACT

Ad hoc protocols, Testing, Verification, Model checking, PLTL, SPIN, Simulations. In this paper, we define a model of an ad hoc routing protocol, i.e. the OLSR (Optimized Link-State Routing) protocol. This model handles novel constraints related to such networks and issues new challenges to treat these constraints. In the network community, the practice is based on simulation models that allow to perform performance measures but no formal methods are used. We propose to promote the use of formal description techniques such as the promela and SDL languages that are both well accepted in the community of communication protocols. Until now, few works exist that handle the formal description of ad hoc networks, this network has as a main feature the absence of infrastructure. So, conformance testing and verification need to be revisited in order to bridge the gap between these new protocols and formal methods. In order to test and verify such protocols we need first to dispose of a formal model of what we want to verify and test. This is what we propose herein

REFERENCES

• 1: Information Technology, Open Systems Interconnection, Conformance Testing Methodology and Framework- Part 3: Tree and Tabular Combined Notation, ISO/IEC 9646-3, Part 1:Test Realisation, ISO/IEC 9646-4.
• 2: The network simulator. http://www.isi.edu/nsnam/ns, 2004.
• 3: The opnet modeler. http://www.opnet.com/products/modeler/home.html, 2005.
• 4: B. Algayres, Y. Lejeune, and F. Hugonnet. Goal: Observing sdl behaviors with geode. In The Proceedings of SDL'95, pages 223--230. Elsevier, 1995.
• 5: Roscoe A.W. A Classical Mind, Essays in Honour of C.A.R. Hoare, chapter Model-Checking CSP. Prentice Hall, 1994.
• 6: César Viho , S. Barbin , Lénaick Tanguy, Towards a Formal Framework for Interoperability Testing, Proceedings of the IFIP TC6/WG6.1 - 21st International Conference on Formal Techniques for Networked and Distributed Systems, p.53-68, August 28-31, 2001
• 7: Cédric Besse , Ana R. Cavalli , Myungchul Kim , Fatiha Zaïdi, Automated Generation of Interoperability Tests, Proceedings of the IFIP 14th International Conference on Testing Communicating Systems XIV, p.169, March 19-22, 2002
• 8: A. Cavalli, A. Mederreg, and F. Zaïdi. Application of formal testing methodology to wireless telephony networks. In 2nd International Information and Telecommunications TEchnologies Symposium, I2TS'2003, Florianopolis, Brazil, october 2003.
• 9: A. Cavalli, A. Mederreg, F. Zaïdi, P. Combes, W. Monin, R. Castanet, M. MacKaya, and P. Laurencot. A Multi-Services and Multi-Protocol Validation Platform - Experimentations Results. In The 16th IFIP TESTCOM, pages 17--32, Oxford, march 2004. Lectures Notes in Computer Science.
• 10: Ana R. Cavalli , David Lee , Christian Rinderknecht , Fatiha Zaïdi, Hit-or-Jump: An algorithm for embedded testing with applications to IN services, Proceedings of the IFIP TC6 WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE XII) and Protocol Specification, Testing and Verification (PSTV XIX), p.41-56, October 05-08, 1999
• 11: R. de Renesse and Aghvami A.H. Formal verification of ad hoc routing protocols using spin model checker. In Proceedings of IEEE MELECON'04, Croatia, May 2004.
• 12: O. Dubuisson. ASN.1. Springer, 1999.
• 13: Karthikeyan Bhargavan , Carl A. Gunter , Moonjoo Kim , Insup Lee , Davor Obradovic , Oleg Sokolsky , Mahesh Viswanathan, Verisim: Formal analysis of network simulations, Proceedings of the 2000 ACM SIGSOFT international symposium on Software testing and analysis, p.2-13, August 21-24, 2000, Portland, Oregon, United States
• 14: Gerard J. Holzmann, Design and validation of computer protocols, Prentice-Hall, Inc., Upper Saddle River, NJ, 1990
• 15: G.J. Holzmann. SPIN Model Checker. Addison-Wesley, 2003.
• 16: Zakkiudin I. Towards a game theoretic understanding of ad-hoc routing. In ENTCS, volume 119, pages 67--92. ENTCS, 2005.
• 17: ITU-T. Recommandation Z.100: CCITT Specification and Description Language (SDL). Technical report, ITU-T, 1999.
• 18: Bhargavan K., Obradovic D., and Gunter G. Formal verification of standards for distance vector routing protocols. Technical report, University of Pennsylvania, 1999.
• 19: Doldi L. Validation of Telecom Systems with SDL. John Wiley and Sons, May 2003.
• 20: D. Lee and M. Yannakakis. Principles and Methods of Testing Finite State Machines - a Survey. In The Proceedings of IEEE, volume 84, pages 1090--1123, August 1996.
• 21: Vadim Okun, Paul E. Black, and Yaacov Yesha. Testing with model checker: Insuring fault visibility. In Proceedings of 2002 WSEAS International Conference on System Science, pages 1351--1356, Rio de Janeiro, Brazil, October 2002.
• 22: S. Bradner, Key words for use in RFCs to Indicate Requirement Levels, RFC Editor, 1997
• 23: Lin T., Midkiff S., and Park J. A framework for wireless ad hoc routing protocols. In Proc. of IEEE Wireless Communications and Networking Conf. (WCNC), 2003.
• 24: T. Clausen , P. Jacquet, Optimized Link State Routing Protocol (OLSR), RFC Editor, 2003
• 25: Glässer U. and Q-P. Gu. Formal description and analysis of a distributed location service for mobile ad hoc networks. Technical report, Fraser University, 2003.
• 26: R.G. de Vries and J. Tretmans. On-the-fly conformance testing using spin. In Fourth Workshop on Automata Theoretic Verification with the Spin Model Checker, ENST 98 S 002, pages 115--128, Paris, France, November 2, 1998.
• 27: Irfan Zakiuddin, Michael Goldsmith, Paul Whittaker, and Paul H. B. Gardiner. A methodology for model-checking ad-hoc networks. In Proc. of SPIN 2003, pages 181--196, Protland, OR, USA, 2003.

INDEX TERMS

Primary Classification:
  C. Computer Systems Organization
  C.2 COMPUTER-COMMUNICATION NETWORKS
      C.2.2 Network Protocols
          Subjects: Routing protocols

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques

  I. Computing Methodologies
  I.6 SIMULATION AND MODELING
      I.6.4 Model Validation and Analysis

General Terms:
Design, Reliability, Verification

Keywords:
PLTL, SPIN, ad hoc network protocols, model checking, simulations, testing, verification