Aleksandar S. Dimovski

Office: 4D04

Email: adim@itu.dk

Phone: +45 7652 2412

 

 

 

GAMECHECKER: Verification Tool Based On Game Semantics and CSP

 

 

 

 


  Home

  Research

  Publications

  CV





 

Tool:

Installation File Examples Documentation
gamecheck.jar Examples-GC.zip gamechecker.pdf

Please see the documentation for installation instructions and how to get started with the tool.

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 an executable jar file from the web page. It needs JDK 1.4.2 (or later) version. Enter the gamechecker home directory and run the tool.

java -jar gamecheck.jar java

or

./gamecheck

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.