ETCH

Overview

ETCH is a stand-alone type checker for Promela, the modelling language used as input to the SPIN model checker. Before verification of a Promela model, SPIN checks that the syntax of the model is correct, but performs only limited type checking. In particular, SPIN does not guarantee static detection of mismatched message arguments in Promela specifications that use dynamic channel passing. This is because the types of channels are only partially specified in Promela.

ETCH extends the type checking capabilities of SPIN, using type reconstruction to recover missing channel type information, allowing strong static type checking. Thus ETCH can detect type errors in Promela specifications which are not detected by SPIN until verification time, and in some cases errors that SPIN misses altogether. This allows for more rapid development of Promela code, and increased confidence in verification models used with SPIN.

The tool supports recursive types which may arise in a Promela model, and includes an algorithm to present recursive type names in a minimal form.

ETCH is implemented using the SableCC parser generation framework.

Downloading and Using ETCH

ETCH version 1.0. ETCH is written in Java and should be fully portable; the archive contains a JAR file and usage notes.

Source code for Etch is also available as part of the symmetrytools git repository. Look at README_ETCH.txt in that repository for instructions on how to build Etch from source.

Citing ETCH

If you use ETCH in your work and wish to cite it, please either refer to our a SPIN 2005 tool paper, or our more recent a Science of Computer Programming journal paper.

Feedback

For questions relating to the use of ETCH, and to report any bugs in the tool (or interesting bugs found using the tool!), please email Alastair Donaldson (address above).