Description: |
Spin is a popular model checker, ie a software tool for automatically verify that a system (given as a program text in the procedural language Promela which has constructs for a.o. message passing and shared variable concurrency) satisfies a property (given as a linear time temporal logic formula). Spin itself is a command line tool that runs n just about everything. Its most elaborate current interface is graphical yet arcane and written in Tcl/Tk. This is both ugly and unacceptable for Mac users. The aim of this thesis project is to radically redesign a GUI for Spin using a modern GUI libraries such as Cocoa on Mac OS X, incorporating graph layout algorithms from the graphviz project. (The Tcl/Tk interface xspin has an option to use graphviz to display the Büchi automata related to the program text. CocoaSpin should be at least as good.) |
