State -space tool: Understanding concurrent programs through state -space

We investigate the use of state-transition diagrams to facilitate understanding of the behavioral aspects of concurrent programs. The approach consists of developing an interactive tool to process Java source code with guidances from a user and displaying the subgraphs of state-space with corresponding source code and details on the selected states and transitions. Based on examples processed in our prototype State-Space Tool, we demonstrate that it is possible to overcome the program scalability and state-transition graph size, which have been a primary reason why state-transition diagrams have not been used in the past as means of understandability analysis. The tool makes it natural to answer functionality questions through investigation using respective reachability paths. The methodology consists of the following four stages. In the first stage, the State-Space Tool processes Java program files and locates all candidate events and predicate expressions containing the events. The interactive GUI tool helps user reduce data domain for state variables in the predicate expressions and respective operations. In the second stage, the tool generates state-machines from the reduced source code per each active thread. Based on the program simplification, unnecessary details such as non state variables are eliminated altogether. In the third stage, the tool constructs a state-space by exploring all possible interleaving of the designated events. We present an algorithm to capture Java concurrency and synchronization in a static data structure. Finally, the tool user composes queries and interactively submits them through GUI, and the state-space subgraphs are visualized. Using the proposed query language (SIL) the user defines groups of nodes and edges that reflect his interest. The user eliminates infeasible paths by inspecting those edges which are not resolved in the previous stages. The novelty of this research lies in: (i) providing methodology to process concurrent Java programs to construct state-space which exposes the temporal properties under analysis, (ii) providing intuitive state-space retrieval language to visualize subgraphs to enhance understanding of concurrent software through visualizing event interleaving, deadlocks, etc. To our knowledge, these have not been attained to date. We consider this research to be important to the concurrent program life cycle