Java PathFinder (JPF) version 7 provides basic support for verifying the distributed Java applications. It can receive a distributed Java application as input that is perceived as multiple Java processes. However, JPF does account for communication between processes of the distributed application, and it thus cannot be used to verify any realistic distributed Java application. Applying JPF on distributed applications requires a model of inter-process communication (IPC) and process aware scheduling.
Model-checking distributed applications is nontrivial. Most existing model checkers can only be applied to single-process applications. One of the proposed techniques to model-check distributed Java applications is centralization, which maps separate processes of a distributed system into threads that are all executed by one process. Since every Java process provides a self-contained execution environment including an exclusive set of basic runtime resources, by applying centralization, parts that represent different processes share the same resources. In order to preserve the behavior of the original distributed system, one needs to ensure proper separation of types in absence of process boundaries enforced by the operating system. Most existing approaches use centralization at the system under test (SUT) level. These techniques modify the SUT code to separate types, and provide their own models of IPC mechanisms, which is conforming to the centralized SUT.
A major drawback of centralization at the SUT level is that they do not impose type separation to non-SUT code such as standard Java libraries. Therefore, different parts of the SUT representing different processes share the same standard classes, which may interrupt the correct behavior of the application. Moreover, it cannot support code that uses the Java reflection API or relies on native implementation. These problems are addressed by an alternative approach that performs centralization at the model checker level, requiring the model checker to directly support verification of multiple processes. JPF version 7 provides the basic building blocks for such a support. As an input, it can accept multiple Java processes.
The purpose of JPF-NAS is to provide these components. There are three key characteristics of JPF-NAS. First, it is the only existing IPC model that conforms to the multi-process support within JPF. Second, to mitigate the state space explosion problem, JPF-NAS uses a form of partial order reduction (POR) to reduce the state space of distributed systems under test (SUTs). Finally, JPF-NAS provides a functionality to inject network failures to the execution of distributed SUTs. Such failures are completely invisible from the system and cannot be detected by exercising all possible behaviors of the system.
JPF-NAS provides three main components: a Connection Manager that maintains a list of communication channels that are created along the current execution path and are back-trackable, a Scheduler that generates scheduling choices to capture different interleaving of processes, and a Failure Injector that injects failures occurring at the network layer upon certain process interactions. JPF-NAS is used as a runtime-configured JPF extension that allows for verifying Java processes that communicate with each other. It can be run through the normal JPF user interface. It can be run from the command line, from a Java-integrated development environment such as Eclipse and NetBeans, and from applications using a specialized JPF driver.
This work was done by Nastaran Shafiei of SGT Inc. for Ames Research Center. This software is available for use. To request a copy, please visit https://software.nasa.gov/software/ARC-17301-1