PROMELA is a verification modeling language. It provides a way for making abstractions of distributed systems. The intended use of the Spin analyzer is to verify fractions of process behavior, that are considered suspect. A complete verification is therefore typically performed in a series of steps, with the construction of increasingly detailed PROMELA models. Each model can be verified with Spin under different types of assumptions about the environment. Once the correctness of a model has been established with Spin, that fact can be used in the construction and verification of all subsequent models.
PROMELA programs consist of processes, message channels, and variables. Processes are global objects that represent the concurrent entities of the distributed system. Message channels and variables can be declared either globally or locally within a process. Processes specify behavior, channels and global variables define the environment in which the processes run.