Distributed model checking with Java PathFinder custom listeners
Aaron Wynn Davis · Texas ScholarWorks (Texas Digital Library) · 2017
The goal of this project was to investigate a distributed testing system based on the Java PathFinder (JPF) model checker. A key objective in doing this was to increase the size of the state space which could be explored in a given time by spreading the test load across multiple instances of JPF while eliminating duplication among the execution paths tested by each instance. The advantage of this approach is that one of the JPF instances may locate an error earlier than it would have been found using the standard JPF model checker. The capability of JPF to use custom listeners was utilized to support this and avoid the need for changes to the JPF Core source code. A custom listener was developed as well as a Java server application which was used to manage the paths taken by each instance of JPF, prevent duplication of effort among the JPF instances and consolidate the results from the testing into a single report. The result was an increase in the state space which was tested with some tests either completing successfully or finding errors using a decreased number of transitions when compared with running a single instance of JPF. The number of states which were explored was also increased. However, it was also found that due to the increase in processing overhead required for the instances of JPF to communicate with the server unfortunately there was no improvement in the overall execution time and in many cases the execution time was increased when compared with running a single instance of JPF. It was also observed that the rate at which the execution time increased as more JPF instances were added was low.