Sciweavers

Share
SCP
2010

Type inference and strong static type checking for Promela

9 years 4 months ago
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...
Alastair F. Donaldson, Simon J. Gay
Added 30 Jan 2011
Updated 30 Jan 2011
Type Journal
Year 2010
Where SCP
Authors Alastair F. Donaldson, Simon J. Gay
Comments (0)
books