Software model checking for Internet Protocols with Java']Java Pathfinder

Java is one of the most popular languages used to build complex and distributed systems. The existence of high-level libraries and middleware makes it now easy to develop applications for enterprise information systems. Unfortunately, implementing distributed software is always an error-prone task. Thus, middleware and application protocols must guarantee different functional and non-functional properties, which has been the field usually covered by tools based on formal methods. However, analyzing software is still a huge challenge for these tools, and only a few can deal with software complexity. One such tool is the Java Pathfinder model checker (JPF). This paper presents a new approach to the verification of Java systems which communicate through Internet Sockets. Our approach assumes that almost all the middleware and network libraries used in Java rely on the protocols available at the TCP/IP transport layer. Therefore, we have extended JPF, now allowing developers to verify not only single multi-threaded programs but also fully distributed Socket-based software.