[Home]   [Research]   [Tools]   [Publications]   [CV]    [Photo Gallery]    [Links]
 
 
                               
GAMECHECKER: A Model Checking Tool Based On Game Semantics and CSP
 
                                             
Version Installation File Examples Documentation
1.0

gamechecker.tar.gz

 Examples.tar.gz gamechecker.pdf
 
Please see the documentation for installation instructions and how to get started with the tool.
 
 
    
Introduction
   

The aim of this tool is checking safety properties such as assertion violations or array-out-of-bounds errors of open programs. The tool implements a Data-Abstraction Refinement Procedure to check for reachability of a specified move (abort) in the game model of a program. The tool compiles an abstracted program into a CSP process whose traces set is exactly the game model of the program. The result process is then verified using CSP model checker - FDR. If no counter-example is found by FDR, the tool reports that the program is safe. If a genuine (deterministic) counter-example is found, the tool outputs the error trace. Otherwise, it uses the nondeterminism of the trace to refine the abstract program.
   
 
  
Download and Installation
     

The tool can be downloaded as a tar.gz file from the web page. It needs JDK 1.4.2 (or later) version.

Unzip and untar the downloaded file.

      tar   xvfz   gamechecker.tar.gz 

Enter the gamechecker directory and run the tool.

      java   -jar   gamechecker.jar 

or 

     ./gamechecker  

The tool also requires the FDR model checker to operate correctly. Note that in order for our tool to use FDR, the executable for FDR must be in your current path.

 

FDR is a product by Formal Systems (Europe) Ltd. It can be downloaded without charge for academic use from their web page http://www.fsel.com. It is available for several architectures and operating systems.

     
 
    
Tutorial Introduction
   
Graphical User Interface
The inputs are an open program, and a property given by an error move whose reachability in the program model will be checked. The default error move is abort. The result pane shows all iteration steps in the procedure, including all reported nondeterministic unsafe plays and applied refinements. In the end, if the procedure terminates, it is reported whether the term is safe or unsafe. In the latter case, a genuine unsafe play is returned. The tool allows the user to choose which variant of Abstraction Refinement Procedure will be applied, the one which is guaranteed to terminate if the term is unsafe or the simpler one which analyses only the shortest nondeterministic unsafe play and which might diverge for unsafe terms. Both procedures might not terminate for safe terms.
    
Examples
A few examples come with the installation file. They illustrate the distinctive features of our method and help the user to get used to the language syntax. See the documentation file for some simple examples.