Alastair F. Donaldson and Simon J. Gay
Glasgow University

Title: Enhanced Type Checking for the SPIN Model Checker

Abstract: We present ETCH, an enhanced type checking tool for the Promela
language.  This tool uses standard type checking in conjunction with
constraint-based type inference to detect type errors in Promela models
which cannot currently be detected by SPIN before verification or
simulation.  ETCH allows for more rapid development of Promela code, and
increased confidence in verification models used with SPIN.