User-friendly GUI in software model checking

Model Checking is an automatic technique for verifying finite-state concurrent systems such as communication protocols and sequential circuit designs. It has a number of advantages over traditional approaches to this problem that are based on simulation, testing, and deductive reasoning. Model checking tools are, however, not widely introduced into industry, and one of the reasons is that they are tricky and difficult to use for engineers. In this paper, we extend the functions of Java PathFinder, a software model checker to verify executable Java bytecode programs, and propose a graphical user interface with a high degree of usability. Our GUI depicts the state transition graphs of not only a whole program but also each thread as a result of verification. Users can get much information through the GUI, for example, the internal states of a program and the correspondence relation between the graphs, with interactive mouse operation. One of the key features of our GUI is a variable-value-based graph abstraction that allows users to focus upon an aspect they are interested in. Our GUI also has an intuitively easy-to-use interface for users to input linear temporal logic (LTL) formulae as a program specification based on the Specification Pattern System.