Promela
Encyclopedia
PROMELA is a verification
modeling language
. 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). PROMELA models can be analyzed with the SPIN model checker
, to verify that the modeled system produces the desired behavior.
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. Finally, it supports the verification of linear time temporal constraints; either with Promela never-claims or by directly formulating the constraints in temporal logic. 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.
The names bit and bool are synonyms for a single bit of information. A byte is an unsigned quantity that can store a value between 0 and 255. shorts and ints are signed quantities that differ only in the range of values they can hold.
Variables can also be declared as arrays. For example, the declaration:
int x [10];
declares an array of 10 integers that can be accessed in array subscript expressions like:
x[0] = x[1] + x[2];
But the arrays can not be ennumerated on creation, so they must be initialised as follows:
int x[3];
x[0] = 1;
x[1] = 2;
x[2] = 3;
The index to an array can be any expression that determines a unique integer value. The effect of an index outside the range is undefined. Multi-dimensional arrays can be defined indirectly with the help of the typedef construct (see below).
proctype A
{
byte state;
state = 3;
}
The proctype definition only declares process behavior, it does not execute it. Initially, in the PROMELA model, just one process will be executed: a process of type init, that must be declared explicitly in every PROMELA specification.
New processes can be spawned using the run statement, which takes an argument consisting of the name of a proctype, from which a process is then instantiated. The run operator can be used in the body of the proctype definitions, not only in the initial process. This allows for dynamic creation of processes in PROMELA.
An executing process disappears when it terminates—that is, when it reaches the end of the body in the proctype definition, and all child processes that it started have terminated.
A proctype may also be active (below).
atomic
{
statements;
}
It is a runtime error if any statement, other than the first statement, blocks in an atomic sequence. Atomic sequences can be an important tool in reducing the complexity of verification models. Note that atomic sequences restricts 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.
chan qname = [16] of {short}
This declares a buffered channel that can store up to 16 messages of type short (capacity is 16 here).
The statement:
qname ! expr;
sends the value of the expression expr to the channel with name qname, that is, it appends the value to the tail of the channel.
The statement:
qname ? msg;
receives the message, retrieves it from the head of the channel, and stores it in the variable msg. The channels pass messages in first-in-first-out order.
A rendezvous port can be declared as a message channel with the store length zero. For example, the following:
chan port = [0] of {byte}
defines a rendezvous port that can pass messages of type byte. Message interactions via such rendezvous ports are by definition synchronous, i.e. sender or receiver (the one that arrives first at the channel) will block for the contender that arrives second (receiver or sender).
When a buffered channel has been filled to its capacity (sending is "capacity" number of outputs ahead of receiving inputs), the default behavior of the channel is to become synchronous, and the sender will block on the next sending. Observe that there is no common message buffer shared between channels. Increasing complexity, as compared to using a channel as unidirectional and point to point, it is possible to share channels between multiple receivers or multiple senders, and to merge independent data-streams into a single shared channel. From this follows that a single channel may also be used for bidirectional communication.
if
:: (a != b) -> option1
:: (a b) -> option2
fi
The selection structure contains two execution sequences, each preceded by a double colon. One sequence from the list will be executed. A sequence can be selected only if its first statement is executable. The first statement of a control sequence is called a guard
.
In the example above, the guards are mutually exclusive, but they need not be. If more than one guard is executable, one of the corresponding sequences is selected non-deterministically. If all guards are unexecutable the process will block until one of them can be selected. (Opposite, the occam
programming language would stop or not be able to proceed on no executable guards.)
if
:: (A true) -> option1;
:: (B
:: else ->; fallthrough_option;
fi
The consequence of the non-deterministic choice is that, in the example above, if A is true, both choices may be taken. In "traditional" programming, one would understand an if - if - else structure sequentially. Here, the if - double colon - double colon must be understood as "any one being ready" and if none is ready, only then would the else be taken.
if
:: value = 3;
:: value = 4;
fi
In the example above, value is non-deterministically given the value 3 or 4.
There are two pseudo-statements that can be used as guards: the timeout statement and the else statement. The timeout statement models a special condition that allows a process to abort the waiting for a condition that may never become true. The else statement can be used as the initial statement of the last option sequence in a selection or iteration statement. The else is only executable if all other options in the same selection are not executable. Also, the else may not be used together with channels.
do
:: count = count + 1
:: a = b + 2
:: (count 0) -> break
od
describes a repetition structure in PROMELA. Only one option can be selected at a time. After the option completes, the execution of the structure is repeated. The normal way to terminate the repetition structure is with a break statement. It transfers the control to the instruction that immediately follows the repetition structure.
do
:: count = count + 1
:: a = b + 2
:: (count 0) -> goto done
od
done:
skip;
The goto in this example jumps to a label named done. A label can only appear before a statement. If we might want 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.
in PROMELA that needs a little explanation is the assert statement. Statements of the form:
assert(any_boolean_condition)
are always executable. If a boolean condition specified holds, the statement has no effect. If, however, the condition does not necessarily hold, the statement will produce an error during verifications with Spin
.
typedef MyStruct
{
short Field1;
byte Field2;
};
The access to the fields declared in a typedef construction is done in the same manner as in C programming language. For example:
MyStruct x;
x.Field1 = 1;
is a valid PROMELA sequence that assigns to the field Field1 of the variable x the value 1.
active proctype A { ... }
active [4] proctype B { ... }
mtype = {M_UP, M_DW};
chan Chan_data_down = [0] of {mtype};
chan Chan_data_up = [0] of {mtype};
proctype P1 (chan Chan_data_in; Chan_data_out)
{
do
:: Chan_data_in ? M_UP -> skip;
:: Chan_data_out ! M_DW -> skip;
od;
};
proctype P2 (chan Chan_data_in; Chan_data_out)
{
do
:: Chan_data_in ? M_DW -> skip;
:: Chan_data_out ! M_UP -> skip;
od;
};
init
{
atomic
{
run P1 (Chan_data_down, Chan_data_up);
run P2 (Chan_data_up, Chan_data_down);
}
}
In the example, the two processes P1 and P2 have non-deterministic choices of (1) input from the other or (2) output to the other. Two rendezvous handshakes are possible, or executable, and one of them is chosen. This repeats forever. Therefore this model will not deadlock.
When Spin
analyzes a model like the above, it will verify the choices with a non-deterministic
algorithm, where all executable choices will be explored. However, when Spin's simulator visualizes possible non verified communication patterns, it may use a random
generator to resolve the "non-deterministic" choice. Therefore the simulator may fail to show a bad execution (in the example there is no bad trail). This illustrates a difference between verification and simulation.
active assert atomic bit
bool break byte chan
d_step D_proctype do else
empty enabled fi full
goto hidden if init
int len mtype nempty
never nfull od of
pc_value printf priority proctype
provided run short skip
timeout typedef unless unsigned
xr xs
Formal verification
In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics .- Usage :Formal verification can be...
modeling language
Modeling language
A modeling language is any artificial language that can be used to express information or knowledge or systems in a structure that is defined by a consistent set of rules...
. The language allows for the dynamic creation of concurrent
Concurrency (computer science)
In computer science, concurrency is a property of systems in which several computations are executing simultaneously, and potentially interacting with each other...
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). PROMELA models can be analyzed with the SPIN model checker
SPIN model checker
SPIN is a general tool for verifying the correctness of distributed software models in a rigorous and mostly automated fashion. It was written by Gerard J. Holzmann and others in the original Unix group of the Computing Sciences Research Center at Bell Labs, beginning in 1980...
, to verify that the modeled system produces the desired behavior.
Introduction
PROMELA is a process modeling language whose intended use is to verify the logic of parallel systems. Given a program in PROMELA, SpinSPIN model checker
SPIN is a general tool for verifying the correctness of distributed software models in a rigorous and mostly automated fashion. It was written by Gerard J. Holzmann and others in the original Unix group of the Computing Sciences Research Center at Bell Labs, beginning in 1980...
can verify the model for correctness by performing random or iterative simulations of the modeled system's execution, or it can generate a C
C (programming language)
C is a general-purpose computer programming language developed between 1969 and 1973 by Dennis Ritchie at the Bell Telephone Laboratories for use with the Unix operating system....
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. Finally, it supports the verification of linear time temporal constraints; either with Promela never-claims or by directly formulating the constraints in temporal logic. 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.
Data Types
The basic data types used in PROMELA are presented in the table below. The sizes in bits are given for a PC i386/Linux machine.| Name | Size (bits) | Usage | Range |
|---|---|---|---|
| bit | 1 | unsigned | 0..1 |
| bool | 1 | unsigned | 0..1 |
| byte | 8 | unsigned | 0..255 |
| mtype | 8 | unsigned | 0..255 |
| short | 16 | signed | -215..215 - 1 |
| int | 32 | signed | -231..231 - 1 |
The names bit and bool are synonyms for a single bit of information. A byte is an unsigned quantity that can store a value between 0 and 255. shorts and ints are signed quantities that differ only in the range of values they can hold.
Variables can also be declared as arrays. For example, the declaration:
int x [10];
declares an array of 10 integers that can be accessed in array subscript expressions like:
x[0] = x[1] + x[2];
But the arrays can not be ennumerated on creation, so they must be initialised as follows:
int x[3];
x[0] = 1;
x[1] = 2;
x[2] = 3;
The index to an array can be any expression that determines a unique integer value. The effect of an index outside the range is undefined. Multi-dimensional arrays can be defined indirectly with the help of the typedef construct (see below).
Processes
The state of a variable or of a message channel can only be changed or inspected by processes. The behavior of a process is defined by a proctype declaration. For example, the following declares a process type A with one variable state:proctype A
{
byte state;
state = 3;
}
The proctype definition only declares process behavior, it does not execute it. Initially, in the PROMELA model, just one process will be executed: a process of type init, that must be declared explicitly in every PROMELA specification.
New processes can be spawned using the run statement, which takes an argument consisting of the name of a proctype, from which a process is then instantiated. The run operator can be used in the body of the proctype definitions, not only in the initial process. This allows for dynamic creation of processes in PROMELA.
An executing process disappears when it terminates—that is, when it reaches the end of the body in the proctype definition, and all child processes that it started have terminated.
A proctype may also be active (below).
The Atomic Construct
By prefixing a sequence of statements enclosed in curly braces with the keyword atomic the user can indicate that the sequence is to be executed as one indivisible unit, non-interleaved with any other processes.atomic
{
statements;
}
It is a runtime error if any statement, other than the first statement, blocks in an atomic sequence. Atomic sequences can be an important tool in reducing the complexity of verification models. Note that atomic sequences restricts 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.
Message Passing
Message channels are used to model the transfer of data from one process to another. They are declared either locally or globally, for instance as follows:chan qname = [16] of {short}
This declares a buffered channel that can store up to 16 messages of type short (capacity is 16 here).
The statement:
qname ! expr;
sends the value of the expression expr to the channel with name qname, that is, it appends the value to the tail of the channel.
The statement:
qname ? msg;
receives the message, retrieves it from the head of the channel, and stores it in the variable msg. The channels pass messages in first-in-first-out order.
A rendezvous port can be declared as a message channel with the store length zero. For example, the following:
chan port = [0] of {byte}
defines a rendezvous port that can pass messages of type byte. Message interactions via such rendezvous ports are by definition synchronous, i.e. sender or receiver (the one that arrives first at the channel) will block for the contender that arrives second (receiver or sender).
When a buffered channel has been filled to its capacity (sending is "capacity" number of outputs ahead of receiving inputs), the default behavior of the channel is to become synchronous, and the sender will block on the next sending. Observe that there is no common message buffer shared between channels. Increasing complexity, as compared to using a channel as unidirectional and point to point, it is possible to share channels between multiple receivers or multiple senders, and to merge independent data-streams into a single shared channel. From this follows that a single channel may also be used for bidirectional communication.
Control Flow Constructs
There are three control flow constructs in PROMELA. They are the case selection, the repetition and the unconditional jump.Case Selection
The simplest construct is the selection structure. Using the relative values of two variables a and b, for example we can write:if
:: (a != b) -> option1
:: (a b) -> option2
fi
The selection structure contains two execution sequences, each preceded by a double colon. One sequence from the list will be executed. A sequence can be selected only if its first statement is executable. The first statement of a control sequence is called a guard
Guard (computing)
In computer programming, a guard is a boolean expression that must evaluate to true if the program execution is to continue in the branch in question. The term is used at least in Haskell, Clean, Erlang, occam, Promela, OCaml and Scala programming languages. In Mathematica, guards are called...
.
In the example above, the guards are mutually exclusive, but they need not be. If more than one guard is executable, one of the corresponding sequences is selected non-deterministically. If all guards are unexecutable the process will block until one of them can be selected. (Opposite, the occam
Occam (programming language)
occam is a concurrent programming language that builds on the Communicating Sequential Processes process algebra, and shares many of its features. It is named after William of Ockham of Occam's Razor fame....
programming language would stop or not be able to proceed on no executable guards.)
if
:: (A true) -> option1;
:: (B
true) -> option2; /* May arrive here also if A
true */:: else ->; fallthrough_option;
fi
The consequence of the non-deterministic choice is that, in the example above, if A is true, both choices may be taken. In "traditional" programming, one would understand an if - if - else structure sequentially. Here, the if - double colon - double colon must be understood as "any one being ready" and if none is ready, only then would the else be taken.
if
:: value = 3;
:: value = 4;
fi
In the example above, value is non-deterministically given the value 3 or 4.
There are two pseudo-statements that can be used as guards: the timeout statement and the else statement. The timeout statement models a special condition that allows a process to abort the waiting for a condition that may never become true. The else statement can be used as the initial statement of the last option sequence in a selection or iteration statement. The else is only executable if all other options in the same selection are not executable. Also, the else may not be used together with channels.
Repetition (Loop)
A logical extension of the selection structure is the repetition structure. For example:do
:: count = count + 1
:: a = b + 2
:: (count 0) -> break
od
describes a repetition structure in PROMELA. Only one option can be selected at a time. After the option completes, the execution of the structure is repeated. The normal way to terminate the repetition structure is with a break statement. It transfers the control to the instruction that immediately follows the repetition structure.
Unconditional Jumps
Another way to break a loop is the goto statement. For example, we can modify the example above as follows:do
:: count = count + 1
:: a = b + 2
:: (count 0) -> goto done
od
done:
skip;
The goto in this example jumps to a label named done. A label can only appear before a statement. If we might want 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.
Assertions
An important language constructLanguage construct
A language construct is a syntactically allowable part of a program that may be formed from one or more lexical tokens in accordance with the rules of a programming language....
in PROMELA that needs a little explanation is the assert statement. Statements of the form:
assert(any_boolean_condition)
are always executable. If a boolean condition specified holds, the statement has no effect. If, however, the condition does not necessarily hold, the statement will produce an error during verifications with Spin
SPIN model checker
SPIN is a general tool for verifying the correctness of distributed software models in a rigorous and mostly automated fashion. It was written by Gerard J. Holzmann and others in the original Unix group of the Computing Sciences Research Center at Bell Labs, beginning in 1980...
.
Complex Data Structures
A PROMELA typedef definition can be used to introduce a new name for a list of data objects of predefined or earlier defined types. The new type name can be used to declare and instantiate new data objects, which can be used in any context in an obvious way:typedef MyStruct
{
short Field1;
byte Field2;
};
The access to the fields declared in a typedef construction is done in the same manner as in C programming language. For example:
MyStruct x;
x.Field1 = 1;
is a valid PROMELA sequence that assigns to the field Field1 of the variable x the value 1.
Active Proctypes
The active keyword that can be prefixed to any proctype definition. If the keyword is present, an instance of that proctype will be active in the initial system state. Multiple instantiations of that proctype can be specified with an optional array suffix of the keyword. Example:active proctype A { ... }
active [4] proctype B { ... }
Executability
The semantics of executability provides the basic means in Promela for modeling process synchronizations.mtype = {M_UP, M_DW};
chan Chan_data_down = [0] of {mtype};
chan Chan_data_up = [0] of {mtype};
proctype P1 (chan Chan_data_in; Chan_data_out)
{
do
:: Chan_data_in ? M_UP -> skip;
:: Chan_data_out ! M_DW -> skip;
od;
};
proctype P2 (chan Chan_data_in; Chan_data_out)
{
do
:: Chan_data_in ? M_DW -> skip;
:: Chan_data_out ! M_UP -> skip;
od;
};
init
{
atomic
{
run P1 (Chan_data_down, Chan_data_up);
run P2 (Chan_data_up, Chan_data_down);
}
}
In the example, the two processes P1 and P2 have non-deterministic choices of (1) input from the other or (2) output to the other. Two rendezvous handshakes are possible, or executable, and one of them is chosen. This repeats forever. Therefore this model will not deadlock.
When Spin
SPIN model checker
SPIN is a general tool for verifying the correctness of distributed software models in a rigorous and mostly automated fashion. It was written by Gerard J. Holzmann and others in the original Unix group of the Computing Sciences Research Center at Bell Labs, beginning in 1980...
analyzes a model like the above, it will verify the choices with a non-deterministic
Nondeterministic algorithm
In computer science, a nondeterministic algorithm is an algorithm that can exhibit different behaviors on different runs, as opposed to a deterministic algorithm. There are several ways an algorithm may behave differently from run to run. A concurrent algorithm can perform differently on different...
algorithm, where all executable choices will be explored. However, when Spin's simulator visualizes possible non verified communication patterns, it may use a random
Randomness
Randomness has somewhat differing meanings as used in various fields. It also has common meanings which are connected to the notion of predictability of events....
generator to resolve the "non-deterministic" choice. Therefore the simulator may fail to show a bad execution (in the example there is no bad trail). This illustrates a difference between verification and simulation.
Keywords
The following identifiers are reserved for use as keywords.active assert atomic bit
bool break byte chan
d_step D_proctype do else
empty enabled fi full
goto hidden if init
int len mtype nempty
never nfull od of
pc_value printf priority proctype
provided run short skip
timeout typedef unless unsigned
xr xs