Etch: An Enhanced Type Checking Tool for Promela

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. Since the utility of model checking depends heavily on the correctness of the model being verified, our tool is a significant contribution.

• Type: Conference
• Year: 2005
• Where: SPIN
• Authors: Alastair F. Donaldson, Simon J. Gay
• Keywords: SPIN 2005, Standard Type Checking, Theoretical Computer Science, Type Checking, Type Checking Tool