jSpin is a graphical user interface for the Spin model checker that is used for verifying concurrent and distributed programs. It is an alternative to the XSpin GUI and was developed primarily for pedagogical purposes. jSpin is written in Java, because the Java platform is both portable and widely in computer science education. The user interface of jSpin is simple and consists of a single window with menus, a toolbar and three adjustable text areas. Spin option strings are automatically supplied and the Spin output is filtered and presented in a tabular form. All aspects of jSpin are configurable: some at compile time, some at initialization through a configuration file and some at runtime.

Here is a screenshot of jSpin. It shows a scenario in which concurrently incrementing a global variable 20 times can produce a final value of 2! The output has been filtered to remove the variables i and finished and the statement that increments i.

EUI is an adaptation of jSpin for the Erigone Model Checker.

SpinSpider is a postprocessor for the Spin debugging output that creates a description of the complete state transition diagram in the dot graphics language. SpinSpider has been integrated into jSpin, although it can be run from the command line as a standalone tool. The functionality of SpinSpider is directly available within the Erigone model checker and can be invoked from EUI.

The fsm format used at the Technische Universiteit Eindhoven is supported on an experimental basis. Optionally, you may wish to use iDot to incrementally display the dot graphs. SpinSpider can also display the Promela source program as a set of automata.

Here are three examples of state diagrams generated by SpinSpider with computations emphasized in red:

• The third attempt at solving the critical section problem. A computation leading to deadlock is emphasized.
• The fourth attempt at solving the critical section problem. A computation leading to starvation is emphasized.
• A program with a loop that does not terminate unless weak fairness is specified.

For information on Spin, refer to:

• M. Ben-Ari. Principles of the Spin Model Checker, Springer, 2008.
• M. Ben-Ari. Principles of Concurrent and Distributed Programming, Addison-Wesley, 2005.
• M. Ben-Ari. Spin reference card (PDF) (LaTeX).
• Gerard J. Holzmann. The Spin Model Checker: Primer and Reference Manual, Addison-Wesley, 2004.

jSpin, SpinSpider and EUI are copyrighted under the GNU General Public License.

Download from Google Code project jspin.

Last update 29 September 2009.