Promela Formalization

RenĂ© Neumann đŸ“§

May 28, 2014

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


We present an executable formalization of the language Promela, the description language for models of the model checker SPIN. This formalization is part of the work for a completely verified model checker (CAVA), but also serves as a useful (and executable!) description of the semantics of the language itself, something that is currently missing. The formalization uses three steps: It takes an abstract syntax tree generated from an SML parser, removes syntactic sugar and enriches it with type information. This further gets translated into a transition system, on which the semantic engine (read: successor function) operates.


BSD License


Session Promela