Type inference and strong static type checking for Promela

The SPIN model checker and its specification language Promela have been used extensively in industry and academia to check logical properties of distributed algorithms and protocols. Model checking with SPIN involves reasoning system via an abstract Promela specification, thus the technique depends critically on the soundness of this specification. Promela includes a rich set of data types including first-class channels, but the language syntax restricts the declaration of channel types so that it is not generally possible to deduce the complete type of a channel directly from its declaration. We present the design and implementation of ETCH, an enhanced type checker for Promela, which uses constraint-based type inference to perform strong type checking of Promela specifications, allowing static detection of errors that SPIN would not detect until simulation/verification time, or that SPIN may miss completely. We discuss theoretical and practical problems associated with designi...

• Type: Journal
• Year: 2010
• Where: SCP
• Authors: Alastair F. Donaldson, Simon J. Gay
• Keywords: Checking, Promela, SCP 2010, Spin