Statistical Model Checking of Opportunistic Network Protocols

ABSTRACT

Simulations and test bed experiments have been the mainstay for analysis of routing algorithms in computer networks. In isolation, these approaches are not amenable to more detailed analyses. For example, it is difficult to check protocols against intricate properties specified as statements in a formal logic. It is therefore natural to turn to the rich and mature theory of model checking for the purpose. Indeed, model checking tools and techniques have been applied in the past for analyzing a variety of deterministic and stochastic systems.

In this paper, we use statistical model checking to analyze properties and performance of opportunistic network routing protocols. While previous works have largely focused on model checking specific protocols (e.g. in wireless mesh networks), we explore the possibility of generic analysis by linking a statistical model checker with a discrete event simulator for opportunistic networks. This allows statistical model checking of several opportunistic network protocols. We illustrate the approach through a comparison of various protocols against several model checking queries.

References

1. L. Pelusi, A. Passarella, and M. Conti. Opportunistic networking: data forwarding in disconnected mobile ad hoc networks. Communications Magazine, IEEE, 44(11):134--141, November 2006.
2. Sushant Jain, Kevin Fall, and Rabin Patra. Routing in a delay tolerant network. In Proc. of the 2004 Conf. on Applications, Technologies, Architectures, and Protocols for Computer Communications, SIGCOMM '04, pages 145--158, New York, NY, USA, 2004. ACM.
3. Chung-Ming Huang, Kun chan Lan, and Chang-Zhou Tsai. A survey of opportunistic networks. In Advanced Information Networking and Applications - Workshops, 2008. AINAW 2008. 22nd Intl. Conf. on, pages 1672--1677, March 2008.
4. Ling-Jyh Chen, Chen-Hung Yu, Tony Sun, Yung-Chih Chen, and Hao-hua Chu. A hybrid routing approach for opportunistic networks. In Proc. of the 2006 SIGCOMM Workshop on Challenged Networks, CHANTS '06, pages 213--220, New York, NY, USA, 2006. ACM.
5. Chiara Boldrini, M. Conti, and A. Passarella. Impact of social mobility on routing protocols for opportunistic networks. In World of Wireless, Mobile and Multimedia Networks, 2007. WoWMoM 2007. IEEE Intl. Symposium on a, pages 1--6, June 2007.
6. Mingjun Xiao, Jie Wu, and Liusheng Huang. Community-aware opportunistic routing in mobile social networks. IEEE Transactions on Computers, 63(7):1682--1695, 2014.
7. Waldir Moreira, Manuel de Souza, Paulo Mendes, and Susana Sargento. Study on the effect of network dynamics on opportunistic routing. In Xiang-Yang Li, Symeon Papavassiliou, and Stefan Ruehrup, editors, Ad-hoc, Mobile, and Wireless Networks, volume 7363 of Lecture Notes in Computer Science, pages 98--111. Springer Berlin Heidelberg, 2012.
8. Jerzy Martyna. Performance modeling of opportunistic networks. In Andrzej Kwiecie, Piotr Gaj, and Piotr Stera, editors, Computer Networks, volume 370 of Communications in Computer and Information Science, pages 240--251. Springer Berlin Heidelberg, 2013.
9. S.K. Dhurandher, D.K. Sharma, I. Woungang, and Han-Chieh Chao. Performance evaluation of various routing protocols in opportunistic networks. In GLOBECOM Workshops (GC Wkshps), 2011 IEEE, pages 1067--1071, Dec 2011.
10. Ari Keränen, Jörg Ott, and Teemu Kärkkäinen. The ONE simulator for DTN protocol evaluation. In Proc. of the 2nd Intl. Conf. on Simulation Tools and Techniques for Communications, Networks and Systems, SimuTools 2009, Rome, Italy, March 2-6, 2009, page 55, 2009.
11. Zhongliang Zhao, Björn Mosler, and Torsten Braun. Performance evaluation of opportunistic routing protocols: A framework-based approach using omnet++. In Proc. of the 7th Latin American Networking Conf., LANC '12, pages 28--35, New York, NY, USA, 2012. ACM.
12. Fredrik Bjurefors. Measurements in Opportunistic Networks. Licentiate thesis, Department of Information Technology, Uppsala University, March 2012.
13. Luca Bortolussi, Vashti Galpin, and Jane Hillston. Hybrid performance modelling of opportunistic networks. In Proc. 10th Workshop on Quantitative Aspects of Programming Languages and Systems, QAPL 2012, Tallinn, Estonia, 31 March and 1 April 2012., pages 106--121, 2012.
14. Tracy Camp, Jeff Boleng, and Vanessa Davies. A survey of mobility models for ad hoc network research. Wireless Communications and Mobile Computing, 2(5):483--502, 2002.
15. Peter Höfner and Annabelle McIver. Statistical model checking of wireless mesh routing protocols. In NASA Formal Methods, 5th Intl. Symposium, NFM 2013, Moffett Field, CA, USA, May 14-16, 2013. Proc., pages 322--336, 2013.
16. Christel Baier and Joost-Pieter Katoen. Principles of Model Checking (Representation and Mind Series). The MIT Press, 2008.
17. Hans Hansson and Bengt Jonsson. A logic for reasoning about time and reliability. Formal Asp. Comput., 6(5):512--535, 1994.
18. Adnan Aziz, Kumud Sanwal, Vigyan Singhal, and Robert K. Brayton. Verifying continuous time markov chains. In Computer Aided Verification, 8th Intl. Conf., CAV '96, New Brunswick, NJ, USA, July 31 - August 3, 1996, Proc., pages 269--276, 1996.
19. Håkan L. S. Younes, Marta Z. Kwiatkowska, Gethin Norman, and David Parker. Numerical vs. statistical probabilistic model checking: An empirical study. In Tools and Algorithms for the Construction and Analysis of Systems, 10th Intl. Conf., TACAS 2004, Held as Part of the Joint European Conf.s on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proc., pages 46--60, 2004.
20. Peter Höfner and Maryam Kamali. Quantitative analysis of AODV and its variants on dynamic topologies using statistical model checking. In Formal Modeling and Analysis of Timed Systems - 11th Intl. Conf., FORMATS 2013, Buenos Aires, Argentina, August 29-31, 2013. Proc., pages 121--136, 2013.
21. Stefano Sebastio and Andrea Vandin. Multivesta: statistical model checking for discrete event simulators. In 7th Intl. Conf. on Performance Evaluation Methodologies and Tools, ValueTools '13, Torino, Italy, December 10-12, 2013, pages 310--315, 2013.
22. Koushik Sen, Mahesh Viswanathan, and Gul A. Agha. VESTA: A statistical model-checker and analyzer for probabilistic systems. In Second Intl. Conf. on the Quantitative Evaluation of Systems (QEST 2005), 19--22 September 2005, Torino, Italy, pages 251--252, 2005.
23. Gul A. Agha, José Meseguer, and Koushik Sen. Pmaude: Rewrite-based specification language for probabilistic object systems. Electr. Notes Theor. Comput. Sci., 153(2):213--239, 2006.
24. Håkan L. S. Younes and Reid G. Simmons. Probabilistic verification of discrete event systems using acceptance sampling. In Computer Aided Verification, 14th Intl. Conf., CAV 2002, Copenhagen, Denmark, July 27-31, 2002, Proc., pages 223--235, 2002.
25. Koushik Sen, Mahesh Viswanathan, and Gul Agha. On statistical model checking of stochastic systems. In Computer Aided Verification, 17th Intl. Conf., CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005, Proc., pages 266--280, 2005.
26. Axel Legay, Benot Delahaye, and Saddek Bensalem. Statistical model checking: An overview. In Howard Barringer, Ylies Falcone, Bernd Finkbeiner, Klaus Havelund, Insup Lee, Gordon Pace, Grigore Rou, Oleg Sokolsky, and Nikolai Tillmann, editors, Runtime Verification, volume 6418 of Lecture Notes in Computer Science, pages 122--135. Springer Berlin Heidelberg, 2010.
27. Musab AlTurki and José Meseguer. Pvesta: A parallel statistical model checking and quantitative analysis tool. In Algebra and Coalgebra in Computer Science - 4th Intl. Conf., CALCO 2011, Winchester, UK, August 30 - September 2, 2011. Proc., pages 386--392, 2011.

Index Terms

• General and reference

  • Cross-computing tools and techniques

    • Verification

• Networks

  • Network protocols

• Software and its engineering

  • Software creation and management

    • Software development process management

    • Software verification and validation

      • Formal software verification

  • Software organization and properties

    • Software functional properties

      • Formal methods

        • Software verification

• Theory of computation

  • Semantics and reasoning

    • Program reasoning

      • Program verification