Modeling class loaders in Java PathFinder version 7

Abstract

The class loading mechanism is one of the essential components of the Java runtime environment. Java class loading is performed on-demand, allows multiple, user extensible class loaders, and can associate a separate type namespace with each class loader. Previous versions of the Java Pathfinder (JPF) model checker only provided a single, hardcoded class loading mechanism. As one of the cornerstones of the upcoming JPF version 7 (JPF v7), we have implemented a standard Java conforming class loader infrastructure. Our implementation does not only support different class loaders and type namespaces, but also allows explicit instantiation of multiple bootstrap class loaders which is essential for model checking of distributed applications - the primary motivation for our work. With the new class loading mechanism, such applications can be mapped to threads using different bootstrap class loaders, thus effectively separating all static fields between application threads. In addition, the JPF v7 class loading is considered to be the basis for future verification of Java security properties.