Outline for an operational semantics of PROMELA
Venkatesh Natarajan, Gerard J. Holzmann · DIMACS series in discrete mathematics and theoretical computer science · 1997
ABSTRACT. PROMELA is a high-level specification language for modeling interactions in distributed systems, and for expressing logical correctness requirements about such interactions. The model checker SPIN accepts specifications written in this language, and it can produce automated proofs for each type of property. SPIN either proves that a property is valid in the given system, or it generates a counter-example that shows that it is not. This paper contains the outline for an operationalsemantics definition of PROMELA. 1.