The Adelaide Refinement Checker

Introduction

The Adelaide Refinement Checker (ARC) is a Communicating Sequential Processes (CSP) model checking environment. CSP scripts consist of definitions, including those of processes and assertion statements where assertion statements define properties of processes or relationships between processes. With ARC CSP scripts can be edited, parsed, type checked, viewed, checked for data independent types and finally model checked.

The functionality of ARC has been restricted to editing, parsing, type checking and exploration of CSP scripts.

Installing  ARC

ARC  is written in the Java 2 language and requires either the Java runtime environment (JRE) or the Java software development kit (SDK) to be installed on the machine on which it is to run. Either Java environment can be obtained from the following web site: http://www.javasoft.com/j2se/*

If Java is already installed on your machine please ascertain that you have the correct version installed by entering java -version in a command or terminal window. The version information returned should be greater than version 1.2.

ARC is available in two compressed forms: a zip file for PCs and a tar, gzip file for Unix machines. To be able to run ARC decompress the downloaded file into an empty directory. Once decompressed you will find a Java jar file and a directory of example CSP scripts.

To start ARC first ensure that your current directory contains the arc.jar file. Then in a terminal window enter:

java -jar arc.jar

When ARC successfully starts a splash screen will appear. This will be followed by ARC window appearing. Please note that the command line above may be appended with the name of a CSP script.

Downloading ARC with example scripts

Click here for the Unix version

Click here for the PC version


Last updated September 9, 2002 by Robert Esser