Promela

While Promela can generally be seen as a fairly standard imperative programming language, it does have some novel features. It is a non-deterministic, multi-process, language, incorporating Dijkstra's guarded commands and Hoare's communication channels. In particular, this communication via channels can be defined to be synchronous (i.e. rendezvous) or asynchronous (i.e. buffered).

Crucially for many contemporary applications, Promela also allows for the dynamic creation of concurrent processes and communication channels.

(Fisher 2011, 144 chap.5 part.5.3.1)

Channels and Communication

Channels are unidirectional structures that exist between two processes (they were characterized in various algebraic approaches such as CCS and CSP)… For example if a channel exists between C₁ and C₂, then C₁ can send a message to C₂ down this channel:

(Fisher 2011, 152 chap.5 part.5.3.1)

References:

Fisher, Michael. 2011. An Introduction to Practical Formal Methods Using Temporal Logic. John Wiley & Sons.

Backlinks:

SPIN