# 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{https://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.