The language allows for the dynamic creation of concurrent processes to model, for example, distributed systems.
In PROMELA models, communication via message channels can be defined to be synchronous (i.e., rendezvous), or asynchronous (i.e., buffered).
An implementation verified with Isabelle/HOL is also available, as part of the Computer Aided Verification of Automata (CAVA) project.
PROMELA is a process-modeling language whose intended use is to verify the logic of parallel systems.
Given a program in PROMELA, Spin can verify the model for correctness by performing random or iterative simulations of the modeled system's execution, or it can generate a C program that performs a fast exhaustive verification of the system state space.
During simulations and verifications, SPIN checks for the absence of deadlocks, unspecified receptions, and unexecutable code.
The verifier can also be used to prove the correctness of system invariants and it can find non-progress execution cycles.
Processes are global objects that represent the concurrent entities of the distributed system.
Atomic sequences can be an important tool in reducing the complexity of verification models.
Note that atomic sequences restrict the amount of interleaving that is allowed in a distributed system.
Intractable models can be made tractable by labeling all manipulations of local variables with atomic sequences.
The statement: receives the message, retrieves it from the head of the channel, and stores it in the variable msg.
Using the relative values of two variables a and b, for example, one can write: The selection structure contains two execution sequences, each preceded by a double colon.
(Opposite, the occam programming language would stop or not be able to proceed on no executable guards.)
To jump at the end of the program, for example, a dummy statement skip is useful: it is a place-holder that is always executable and has no effect.
If, however, the condition does not necessarily hold, the statement will produce an error during verifications with SPIN.
A PROMELA typedef definition can be used to introduce a new name for a list of data objects of predefined or earlier defined types.
If the keyword is present, an instance of that proctype will be active in the initial system state.
Example: The semantics of executability provides the basic means in Promela for modeling process synchronizations.
However, when Spin's simulator visualizes possible non-verified communication patterns, it may use a random generator to resolve the "non-deterministic" choice.