Software Model Checking of UDP-based Distributed Applications

Abstract

An extension to the software model checker Java Pathfinder for verifying networked applications using the User Datagram Protocol (UDP) is presented.

UDP maximizes performance by omitting flow control and connection handling. For instance, media-streaming services often use UDP to reduce delay and jitter. 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. 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.