Extending JPF to verify distributed systems

This paper presents our work on model checking distributed applications. We refer to distributed applications as a collection of communicating processes, regardless of their physical locations and the communication means. Our work targets applications written in Java. It relies on the multiprocess support included in Java Pathfinder (JPF) version 7 which allow for verifying the bytecode of distributed applications. The basic support for distributed applications in JPF does not account for communication between processes. In this work, we address this limitation. The work is implemented as a JPF extension which models inter- process communication (IPC) mechanisms. It uses a form of partial order reduction (POR) to explore all possible executions of a distributed Java application. Moreover, our approach provides a functionality to check the given distributed application against possible network failures which can occur at the operating system or the hardware layer.