Skip to main content
SpringerLink
Log in

Cardinality of UDP Transmission Outcomes

  • Conference paper
  • First Online:
Book cover Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2015)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9409))

  • 584 Accesses

Abstract

This paper examines the cost of testing network applications using the User Datagram Protocol (UDP). Such applications must deal with packet loss, duplication, and reordering. Ideally, a UDP application should be tested against all possible outcomes of unreliable UDP transmissions. Their number, however, grows at least exponentially in the number of transmitted packets.

To estimate the cost of the exhaustive testing of UDP applications, we determine the number of UDP transmission outcomes analytically. Based on this combinatorial analysis, we derive a sound, complete, and optimal algorithm for generating outcomes of unreliable UDP transmissions. The algorithm is implemented in the net-iocache extension of the software model checker Java Pathfinder (JPF).

Experimental results confirm the consistency of the implementation with the analytical results. In addition, we found that JPF’s state matching reduces the explored state space significantly and ensures the practicability of the approach despite of its exponential complexity.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channels. Information and Computation 127(2), 91–101 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  2. Artho, C., Garoche, P.: Accurate centralization for applying model checking on networked applications. In: Proceedings of the 21st International Conference on Automated Software Engineering (ASE 2006). pp. 177–188. Tokyo, Japan (2006)

    Google Scholar 

  3. Artho, C., Leungwattanakit, W., Hagiya, M., Tanabe, Y.: Efficient model checking of networked applications. In: Paige, R.F., Meyer, B. (eds.) TOOLS EUROPE 2008. LNBIP, vol. 19, pp. 22–40. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  4. Bona, M.: Combinatorics of Permutations. CRC Press, second edition edn. (2012)

    Google Scholar 

  5. Droms, R.: Dynamic host configuration protocol. IETF RFC 2131 (1997). http://www.ietf.org/rfc/rfc2131 Accessed: 13th Feb 2015

  6. Durstenfeld, R.: Algorithm 235: Random permutation. Communications of the ACM 7(7), 420 (1964)

    Google Scholar 

  7. Farchi, E., Krasny, Y., Nir, Y.: Automatic simulation of network problems in UDP-based Java programs. In: Proceedings of the 18th International Parallel and Distributed Processing Symposium. IEEE (2004)

    Google Scholar 

  8. Fisher, R.A., Yates, F.: Statistical tables for biological, agricultural and medical research. Oliver & Boyd, London, 3rd edn, pp. 26–27 (1948)

    Google Scholar 

  9. Hall, M.: Combinatorial theory. Wiley (1986)

    Google Scholar 

  10. Havelund, K., Pressburger, T.: Model checking Java programs using Java PathFinder. International Journal on Software Tools for Technology Transfer 2(4), 366–381 (2000)

    Article  MATH  Google Scholar 

  11. Huitema, C.: Real time control protocol (RTCP) attribute in session description protocol (SDP). IETF RFC 3605 (2003). http://tools.ietf.org/html/rfc3605 Accessed: 13th Feb 2015

  12. Ives, F.M.: Permutation enumeration: four new permutation algorithms. Communications of the ACM 19(2), 68–72 (1976)

    Article  MATH  Google Scholar 

  13. Junqueira, F., Reed, B.: ZooKeeper: Distributed Process Coordination. O’Reilly (2013)

    Google Scholar 

  14. Leungwattanakit, W., Artho, C., Hagiya, M., Tanabe, Y., Yamamoto, M., Takahashi, K.: Modular software model checking for distributed systems. IEEE Transactions on Software Engineering 40(5), 483–501 (2014)

    Article  Google Scholar 

  15. Linux Foundation: Network emulation with netem. www.linuxfoundation.org/collaborate/workgroups/networking/netem (accessed on October 7, 2014

  16. Ma, L., Artho, C., Sato, H.: Analyzing distributed Java applications by automatic centralization. In: Proceedings of the 2nd IEEE Workshop on Tools in Process. IEEE, Kyoto, Japan (2013)

    Google Scholar 

  17. Mockapetris, P.: Domain names – implementation and specification. IETF RFC 1035 (1987). http://www.ietf.org/rfc/rfc1035 Accessed: 13th Feb 2015

  18. Narasiodeyar R., J.A.: Improvement in packet-reordering with limited re-sequencing buffers: An analysis. In: 2013 IEEE 38th Conference on Local Computer Networks (LCN), pp. 453–457. IEEE (2013)

    Google Scholar 

  19. Reinecke, P., Drager, M., Wolter, K.: Netemcg – IP packet-loss injection using a continuous-time Gilbert model. Tech. Rep. TR-B-11-05, Freie Universitt Berlin, Germany (2011)

    Google Scholar 

  20. Robertson, K., Miller, K., White, M., Tweedly, A.: Starburst multicast file transfer protocol (MFTP) specification. IETF-DRAFT (1998). http://tools.ietf.org/html/draft-miller-mftp-spec-03 Accessed: 12th Feb 2015

  21. Roskind, J.: QUIC: Multiplexed stream transport over UDP. Google working design document (2013)

    Google Scholar 

  22. Schulzrinne, H.: RTP: A transport protocol for real-time applications. IETF RFC 3550 (2003). http://tools.ietf.org/html/rfc3550 Accessed: 13th Feb 2015

  23. Sebih, N., Weitl, F., Artho, C., Hagiya, M., Yamamoto, M., Tanabe, Y.: Software model checking of UDP-based distributed applications. In: Proceedings of the Second International Symposium on Computing and Networking (CANDAR 2014). pp. 96–105. IEEE, Shizuoka, Japan (2014)

    Google Scholar 

  24. Sebih, N., Weitl, F., Artho, C., Hagiya, M., Yamamoto, M., Tanabe, Y.: Software model checking of UDP-based distributed applications. International Journal of Networking and Computing (IJNC) 5(2), 373–402 (2015)

    Article  Google Scholar 

  25. Shafiei, N., Mehlitz, P.C.: Extending JPF to verify distributed systems. ACM SIGSOFT Software Engineering Notes 39(1), 1–5 (2014)

    Article  Google Scholar 

  26. Sliwinski, J., Beben, A., Krawiec, P.: EmPath: tool to emulate packet transfer characteristics in IP network. In: Ricciato, F., Mellia, M., Biersack, E. (eds.) Proceedings of the Second International Workshop on Traffic Monitoring and Analysis (TMA 2010). LNCS, vol. 6003, pp. 46–58. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  27. Sollins, K.: The TFTP protocol (revision 2). IETF RFC 1350 (1992). http://tools.ietf.org/html/rfc1350 Accessed: 1th May 2015

  28. Stoller, S.D., Liu, Y.A.: Transformations for model checking distributed java programs. In: Dwyer, M.B. (ed.) Proceedings of the 8th International SPIN Workshop (SPIN 2001). LNCS, vol. 2057, p. 192. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  29. Visser, W., Havelund, K., Brat, G., Park, S., Lerda, F.: Model checking programs. Automated Software Engineering Journal 10(2), 203–232 (2003)

    Article  Google Scholar 

  30. Weitl, F., Sebih, N., Artho, C.: jpf-net-iocache v2 – source code repository. https://bitbucket.org/weitl/jpf-net-iocache Accessed: 15th Apr 2015

  31. Rathje, W., Richards, B.: A framework for model checking UDP network programs with Java Pathfinder. In: HILT 2014 Proceedings of the 2014 ACM SIGAda Annual Conference on High Integrity Language Technology (2014)

    Google Scholar 

  32. Zhang, M., Dusi, M., John, W., Chen, C.: Analysis of UDP traffic usage on Internet backbone links. In: Ninth Annual International Symposium on Applications and the Internet (SAINT 2009), pp. 280–281. IEEE (2009)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Chiba University, Chiba, Japan

    Franz Weitl & Mitsuharu Yamamoto

  2. AIST/RISEC, Amagasaki/tsukuba, Japan

    Cyrille Artho & Yoriyuki Yamagata

  3. The University of Tokyo, Tokyo, Japan

    Nazim Sebih & Masami Hagiya

  4. Tsurumi University, Yokohama, Japan

    Yoshinori Tanabe

Authors
  1. Franz Weitl
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Nazim Sebih
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Cyrille Artho
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Masami Hagiya
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Yoshinori Tanabe
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Yoriyuki Yamagata
    View author publications

    You can also search for this author in PubMed Google Scholar

  7. Mitsuharu Yamamoto
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Franz Weitl .

Editor information

Editors and Affiliations

  1. Nanjing University, Nanjing, Jiangsu, China

    Xuandong Li

  2. Birmingham City University, Birmingham, United Kingdom

    Zhiming Liu

  3. Uppsala University, Uppsala, Sweden

    Wang Yi

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Weitl, F. et al. (2015). Cardinality of UDP Transmission Outcomes. In: Li, X., Liu, Z., Yi, W. (eds) Dependable Software Engineering: Theories, Tools, and Applications. SETTA 2015. Lecture Notes in Computer Science(), vol 9409. Springer, Cham. https://doi.org/10.1007/978-3-319-25942-0_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-25942-0_8

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-25941-3

  • Online ISBN: 978-3-319-25942-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation