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 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. |
