Cardinality of UDP Transmission Outcomes

Cardinality of UDP Transmission Outcomes
复制标题

UDP 传输结果的基数

DOI:
10.1007/978-3-319-25942-0_8
复制
发表时间:
2015
期刊:
Proc 1st International Symposium on Dependable Software Engineering: Theories, Tools, and Applications
影响因子:
--
通讯作者:
Mitsuharu Yamamoto
Mitsuharu Yamamoto
中科院分区:
--
文献类型:
--
作者:
Franz Weitl;Nazim Sebih;Cyrille Artho;Masami Hagiya;Yoshinori Tanabe;Yoriyuki Yamagata;Mitsuharu Yamamoto

文献摘要

相似文献

本文研究了使用用户数据报协议(UDP)测试网络应用程序的成本。这样的应用程序必须处理丢包、复制和重新排序问题。理想情况下,UDP应用程序应该针对不可靠的UDP传输的所有可能结果进行测试。为了估计对UDP应用进行穷举测试的成本,我们解析地确定了UDP传输结果的数量。基于这种组合分析,我们推导出了一个合理、完整和最优的算法来生成不可靠的UDP传输结果。该算法在软件模型检查器Java Path Finder(JPF)的Net-iocache扩展中实现,实验结果与分析结果一致。此外,我们还发现JPF的状态匹配算法虽然具有指数级的复杂度,但大大减少了搜索到的状态空间,保证了算法的实用性。
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.