2014 Second International Symposium on Computing and Networking (CANDAR) (2014)
Dec. 10, 2014 to Dec. 12, 2014
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.