A GUI for model checkers
System validation, the process of checking the correctness of specifications, designs and products, is an important technique to guarantee the safety and quality of a system. There are several validation techniques, such as peer reviewing, simulation, formal verification, and model checking, etc.
Given a finite-state model of a system and a property stated in some appropriate logical formalism, model checking technique can systematically check the validity of this property. Nowadays, model checking is becoming a general and popular approach and is applied in areas like hardware verification and software engineering. Due to its success in several projects and the high degree of support from tools, there are many model checkers available now. From the view of graphical user interface (GUI), some model checkers are primitive, such as TLC  which is used to validate a system written in TLA+ specifications , which are highly abstract and give the user a compete view of the system; and some do have a good graphical user interface, such as UPPAAL  which lets the user validate a system through a GUI, which provides the user more convenience and gives the user a more direct and clearer view of the system, especially in the process of simulation it can help the user understand how the system runs. Another model checker that has a GUI is Xspin  which is the graphical interface of Spin , a popular open source model checker, which can be used for the formal verification of distributed software systems. Xspin runs independently from Spin and helps by generating the proper Spin commands based on menu selection.
Is it possible to develop a GUI for the TLC model checker? How to design this GUI? What problems will be encountered? The goal of the literature survey is to find answers to these questions.
The purpose of the final part of the project is to develop the graphical interface of the TLC model checker (the GTLA system) according to the design from the literature survey. The TLA+ user can use the GTLA system to validate a system written in TLA+ specifications through a graphical user interface.
This report consists of two parts. The first part is the literature survey, which will discuss the concepts of model checking and introduce three model checkers: TLC, UPPAAL and Xspin; additionally, if it is good to make specifications executable and how to animate specifications will be discussed; finally, a case study, GUI design for the TLC model checker will be presented. The second part is the final thesis, which will introduce how the GTLA system is designed and implemented; the testing result, conclusion and future work will be given at last.
This report has been written as the results of the literature survey and the final thesis, two parts of the graduation at Delft Computer Science, Delft University of Technology.