Title
Cardinality of UDP Transmission Outcomes.
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.
Year
DOI
Venue
2015
10.1007/978-3-319-25942-0_8
SETTA
Keywords
DocType
Volume
User datagram protocol, Software model checking, Java Pathfinder, Combinatorial analysis
Conference
9409
ISSN
Citations 
PageRank 
0302-9743
0
0.34
References 
Authors
16
7
Name
Order
Citations
PageRank
Franz Weitl1295.70
Nazim Sebih200.68
Cyrille Artho358844.46
Masami Hagiya4649102.85
Yoshinori Tanabe512413.96
Yoriyuki Yamagata6207.28
Mitsuharu Yamamoto79111.09