The Community for Technology Leaders
2014 Second International Symposium on Computing and Networking (CANDAR) (2014)
Shizuoka, Japan
Dec. 10, 2014 to Dec. 12, 2014
ISBN: 978-1-4799-4152-0
pp: 96-105
We extend exhaustive verification of networked applications to applications using the User Datagram Protocol (UDP). UDP maximizes performance by omitting flow control and connection handling. High-performance services often offer a UDP mode in which they handle connections internally for optimal throughput. However, because UDP is unreliable (packets are subject to loss, duplication, and reordering), verification of UDP-based applications becomes an issue. Even though unreliable behavior occurs only rarely during testing, it often appears in a production environment due to a larger number of concurrent network accesses. Our tool systematically tests UDP-based applications by producing packet loss, duplication, and reordering for each packet. It is built on top of net-Rio cache for the Java Path Finder model checker. We have evaluated the performance of our tool in a multi-threaded client/server application and detected incorrectly handled packet duplicates in a file transfer client.
Java, Model checking, Software, Protocols, Systematics, Sockets, Packet loss

N. Sebih, F. Weitl, C. Artho, M. Hagiya, Y. Tanabe and M. Yamamoto, "Software Model Checking of UDP-based Distributed Applications," 2014 Second International Symposium on Computing and Networking (CANDAR), Shizuoka, Japan, 2014, pp. 96-105.
162 ms
(Ver 3.3 (11022016))