JPF in its basic form is a state exploring Java virtual machine (JVM) which can systematically explore all potential executions of Java code. There are many different ways to explore the executions. For example, JPF can use different search strategies such as breadth-first search (BFS) and depth-first search (DFS). Consider a Java code that gives rise to the following state space diagram.

If we run JPF with the search strategy BFS, the states are explored in the following order: s0, s1, s2, s3, s4; with DFS, the order is : s0, s1, s3, s4, s2.

JPF also contains a search strategy which is called random search (RS). The strategy will start with the initial state (s0 in our example) and follow one path of the execution until there is no next state and then it continues its search from the initial state. Two possible paths explored by RS are: s0, s2 and s0, s1, s_3.

Task 1. Develop a Java app that prints output. When checking the Java app by JPF with DFS the output should be different from the output for BFS.

Task 2. Verify your program using JPF with BFS, DFS. To do that, you need to create an application properties file (.jpf file) for your Java app developed in Task 1. Configure the search property to be gov.nasa.jpf.search.heuristic.BFSHeuristic or gov.nasa.jpf.search.heuristic.DFSHeuristic.

Task 3. Generate the state space diagram for BFS and DFS. To do this you need to set the listener to StateSpaceDot.

Task 4. Verify your program using RS. RS can explore several random executions and in JPF you have the freedom to set the maximum number of executions you would like RS to explore. Firstly, set your search strategy to gov.nasa.jpf.search.RandomSearch. Secondly, set the search.RandomSearch.path_limit property to be any integer larger than 0. Compare the resulting state space diagrams.