Promela Formalization

Title:	Promela Formalization
Author:	René Neumann (rene /dot/ neumann /at/ in /dot/ tum /dot/ de)
Submission date:	2014-05-28
Abstract:	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.
BibTeX:	@article{Promela-AFP, author = {René Neumann}, title = {Promela Formalization}, journal = {Archive of Formal Proofs}, month = may, year = 2014, note = {\url{http://isa-afp.org/entries/Promela.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	CAVA_Automata, LTL
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.