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.
Keywords for this software
References in zbMATH (referenced in 2 articles )
Showing results 1 to 2 of 2.
- Donaldson, Alastair F.; Gay, Simon J.: Type inference and strong static type checking for Promela (2010)
- Donaldson, Alastair F.; Miller, Alice: Automatic symmetry detection for Promela (2008)