A Novel Framework for Model Checking UDP Network Interactions

This poster presents the first Java Pathfinder extension to model realistic User Datagram Protocol (UDP) networking communications, which is used to verify a UDP network software simulator, RF. Java Pathfinder is a model checking software system developed by NASA and used frequently for verifying that concurrent software systems avoid deadlock states and other errors. It does not natively support network modeling. NetIOCache is a Java Pathfinder extension for verifying TCP/IP networks, but no similar UDP extensions currently exist. NetStub, a Java Pathfinder extension, can simulate UDP behavior as a collection of threads, but it does not simulate important and common UDP properties such as packet loss and reordering that are often necessary to simulate in order to verify a UDP network model. I present a novel extension to Java Pathfinder to allow modeling of realistic UDP communications that includes simulated packet loss and reordering. This extension is then used to verify RF for up to four network processes. The RF model is verified accurate (it never encounters deadlocks or uncaught Java exceptions)