Promela (PROtocol MEta LAnguage) is the input language to the SPIN verification system, developed at Bell Labs by Gerard Holzmann et al.

Promela is a nondeterministic guarded command language, in idea proposed in 1975 by Dijkstra. It is nondeterministic in the sense that a "selection" or "switch" operation is allowed to have multiple true options, ANY of which can be selected as a valid path of execution. It is guarded in the sense that operations are controlled by "guard statements", that is, boolean expressions which are "disabled" (or "sleep") until they become true. Some of its syntax is borrowed from CSP; it also has many C-like features (including use of the cpp pre-processor to handle compile-time constants and macros), making it relatively easy for a systems hacker like myself to pick up.

Promela includes the notion of parallel processes, instances of process classes, synchronous message passing, asynchronous (finite buffer) message passing, queue manipulation, global and local variables, inline functions, a complete set of logical operators, and pear tree sized partridges.

All of this makes Promela naturally well-suited for writing models of state machines and models of stateful applications, especially communication and synchronization protocols. These models are executable (in that they can randomly produce an instance of a valid execution), and are also pliable to formal methods analysis and verification of properties like graceful termination, progress, and general properties expressed using linear temporal logic.

Log in or register to write something here or to contact authors.