Software Engineering Development:- PROMELA

Promela :- Verification Modelling Language.

PROMELA models can be analyzed with the SPIN model checker, to verify that the modeled system produces the desired behavior.

It Consist:
1)Processes,
2)Message channels,
3)Variables

Promela language have following behavior
1) Atomic
Introduces a sequence of statements that is to be executed indivisibly.

2)Interleaving
In the interleaving of process executions, no other process can execute statements from the moment that the first statement of an atomic sequence is executed, until the last one has completed.

3)Blocking
If any statement within the atomic sequence blocks, the atomicity is lost, and other processes are allowed to execute arbitrarily many statements.
When the blocked statement becomes executable again, the execution of the atomic sequence can be resumed