Promela Reference -- Intro

Promela

Document Structure

Intro

INTRODUCTION
Five parts of the Promela language are discussed in separate sections of this manual. A sixt section gives a brief motivation for things that are intentionally outside the language. The sections are:

References to terms defined in this manual are linked to the corresponding manual page, e.g. send, len.

In the tradition of the Unix manuals, each manual page that follows this introduction contains some or all of the following defining elements.

All terms set in italic , such as name , const, and typename , refer to the grammar rules.

SEMANTICS
The semantics of the language is defined in terms of an operational model. The model contains one or more ``processes,'' zero or more ``variables,'' zero or more message ``channels,'' and a ``semantics engine'' that defines how the actions of the processes may be interleaved in time. The processes are defined by labeled transition systems, which are in turn derived from proctype declarations. Similarly, the domains of values that variables can hold are derived from variable type declarations.

The semantics engine executes the model in a step by step manner. In each step, one executable basic statement is selected at random. To determine if a statement is executable or not, one of the conditions that must be evaluated is the corresponding executability clause, as described in this manual. For the selected statement, the effect clause from the statement is then applied, as also described in this manual, and the current state of the process that contained the statement is updated. The semantics engine continues executing statements until no executable statements remain, which happens if either the number of active processes goes to zero, or when a valid or invalid end-state is reached.

Declarators, defined in Section 2, define the basic elements of the system. Control flow statements, defined in Section 3, affect only the structure of the underlying transition system. Basic statements, defined in Section 4, are the only language elements that define state changes. Smaller building blocks for the system, such as predefined variables and functions, are defined in Section 5.

Central to the operational semantics definition is the description of the semantics engine that defines when and how statements may be executed. Before giving the definition of this engine, we give a definition of the formal objects that this engine manipulates: variables, message channels, and processes. We also define what the main component of a transition and of a global system state are. Not defined here are more basic terms, such as sets , identifiers , integers , and Booleans .

In the remainder of this section we refer to the elements of a tuple with a dot notation. For instance, if v is a variable, then v.scope is its scope.

The scope of a variable either identifies all active processes (for globally declared variables) or one specific active process. For the purposes of this definition, we can assume that a positive integer identifies the pid (S.4) of one active process, and a negative integer identifies all active processes. The type of a variable determines its domain . For instance, a variable of type bit (see datatypes) has domain {0,1}.

A positive ch_id will be used to identify an active channel , while a negative number will identify a channel template from which more channels of the same type may be instantiated. Note that the definition of a channel does not contain a scope , like the definition of a variable. The reason is that a channel always has global scope. It can be created either globally or locally, by an active process, but its method of creation will not affect its scope in Promela, i.e., every channel is in principle accessible to every active process, by knowledge of the identifying ch_id .

We will refer to the elements of set lstates as the local states of a process (S.4). The integer values suffice to uniquely identify each state within the set, but hold no more information.

The elements prty and rv are used in cond and effect definitions to enforce the semantics of, respectively, the unless construct, and of synchronous message passing operations, see send.

The definitions S.1 to S.6 capture the minimal information that is needed to define the semantics of the Promela language in terms of an operational model, with processes defined as transition systems. The purpose of the definition of the semantics engine in the next subsection is to offer a mechanism for resolving questions about the interpretation of Promela constructs that is independent of the Spin tool.

OPERATIONAL MODEL, SEMANTICS ENGINE
The semantics engine executes the system, at least conceptually, in a stepwise manner: selecting and executing one basic statement at a time. At the highest level of abstraction, the behavior of this engine can be defined as follows.

Let E be a set of pairs { p,t }, with p a process, and t a transition. Let executable(s) be a function, yet to be defined, that returns a set of such pairs, one for each executable transitions in system state s . The semantics engine then performs as follows.

  1 while ((E = executable(s)) != {})
  2 {
  3 	for some {p,t} from E
  4 	{	s' = apply(t.effect, s)
  5 
  6 		if (handshake == 0)
  7 		{	p.curstate = t.target
  8 			s = s'
  9 		} else
 10 		{	# try to complete an rv handshake
 11 			E' = executable(s')
 12 			# if E' is {}, s remains unchanged
 13 
 14 			for some {p',t'} from E'
 15 			{	p.curstate = t.target
 16 				s = apply(t'.effect, s')
 17 				p'.curstate = t'.target
 18 			}
 19 			handshake = 0
 20 	}	}	
 21 }
 22 while (stutter) { s = s }	/* the 'stutter' extension */
As long as there are executable transitions (corresponding to the basic statements of Promela), the semantics engine will select one of them at random and execute it.

To verify liveness properties with Spin, we must be able to treat finite executions as special cases of infinite executions. The standard way of doing so is to define a stutter extension of finite executions, where the final state is repeated ad infinitum. The semantics engine above uses the system variable stutter to determine if the stuttering rule is in effect. Only the verification system can change this variable. More on verification, which is strictly seen outside the semantics definition, follows at the end of these notes.

The function apply() applies the effect of the selected transition to the system state, possibly modifying system and local variables, the contents of channels, or even the values of exclusive and handshake , as defined in the effect clauses from atomic, and send, respectively. If no rendezvous offer was made (line 6), the current state of the process that executed the transition is updated (line 7), and the global state change takes effect by an update of the system state itself (line 8). If a rendezvous offer was made in the last transition, it cannot result in a global state change unless the offer can also be accepted (cf. send). On line 11 the transitions that have now become executable are selected. The definition of the function executable() below guarantees that this set can only contain accepting transitions for the given offer. If there are none, the global state change is declined, and execution proceeds with the selection of a new executable candidate transition from the original set E . If the offer can be matched, the global state change takes effect. The current states of both processes are now updated from source to target state (where the two may, of course, be equal).

The main part of the semantics definition is in the definition of what precisely constitutes an executable transition. One part will be clear: in the current system state the executability clause t.cond must be satisfied. But there is more.

The following specification of the function executable() resolves these issues. To avoid confusion, the state variables timeout, else and exclusive are set in bold. These variables are the only ones that can be modified within this function, as part of the selection process.

  1 Set
  2 executable(State s)
  3 {	new Set E
  4 	new Set e
  5 
  6 	E = {}
  7 	timeout = False
  8 AllProcs:
  9 	for each active process p
 10 	{	if (exclusive == 0
 11 		or  exclusive == p.pid)
 12 		{	for u from high to low	# priority ('unless')
 13 			{	e = {};  else = False
 14 OneProc:			for each transition t in p.trans
 15 				{	if (t.source == p.curstate
 16 					and t.prty == u
 17 					and (handshake == 0
 18 					or   handshake == t.rv)
 19 					and  eval(t.cond) == True)
 20 					{	add {p,t} to set e
 21 				}	}
 22 				if (e != {})
 23 				{	add all elements of e to set E
 24 					break	# on to next process
 25 				} else if (else == False)
 26				{	else = True
 27					goto OneProc
 28				} # or else lower the priority
 29 	}	}	}
 30 
 31 	if (E == {} and exclusive != 0)
 32 	{	exclusive = 0
 33 		goto AllProcs
 34 	}
 35 	if (E == {} and timeout == False)
 36 	{	timeout = True
 37 		goto AllProcs
 38 	}
 39 
 40 	return E	# defining the set of executable transitions
 41 }
For a transition to be added to the set of executable transitions it has to pass a number of tests.

If no transitions are found to be executable with the default value False for system variable else, the transitions of the current process are checked again, this time with else equal to True (line 26-27). If no transitions are executable in any process, the value of system variable timeout is changed to True and the entire selection process is repeated (line 32-35). The new value of timeout will stick for just one step (line 7), but it can cause any number of transitions in any number of processes to become executable in the current global system state. The syntax of Promela prohibits the use of both else and timeout within a single condition statement.

Note that the semantics engine does not establish the validity or invalidity of correctness requirements.

INTERPRETING PROMELA SEMANTICS
The basic objects that are manipulated by the semantics engine we have defined above are, of course, intended to correspond to the basic objects of a Promela specification. Much of the language, however, merely provides a convenient mechanism for dealing with the underlying objects. Section 1 of this manual, for instance, describes some ``pseudo'' language features, or meta-terms, that are translated into Promela proper by preprocessors. Section 2 defines the Promela syntax for declaration of variables, processes, and channels. Section 3 defines how Promela's control-flow constructs correspond to the underlying transition relations. An if statement, for instance, merely defines how multiple transitions can exit from the same local process state. The semantics engine does not have to know anything about if , do , break , or goto ; it merely deals with local states and transitions.

Some Promela constructs cannot be translated away. The semantics model is defined in such a way that these primitive constructs correspond directly to the transitions as defined in S.5. We call these Promela constructs basic statements . Section 4 defines the transition elements for each basic statement in the language. Section 5 of this manual, together with the grammar definition, defines the remaining Promela syntax rules for the elements of a basic statement.

THREE EXAMPLES
Consider the following Promela system.

chan x = [0] of { bit };
chan y = [0] of { bit };
active proctype A() { x?0 unless y!0 }
active proctype B() { y?0 unless x!0 }
Only one of two possible rendezvous handshakes can take place. Do the semantics rules tell us which one? If so, can the same rules also resolve the following, very similar, situation?
chan x = [0] of { bit };
chan y = [0] of { bit };
active proctype A() { x!0 unless y!0 }
active proctype B() { y?0 unless x?0 }
And, finally, what should we expect to happen in this case.
chan x = [0] of { bit };
chan y = [0] of { bit };
active proctype A() { x!0 unless y?0 }
active proctype B() { y!0 unless x?0 }
Each of these cases can be hard to resolve without guidance from a semantics definition. The semantics rules for handling rendezvous communication and for handling unless statements seem to conflict here. This is what we know.

We are now ready to resolve the semantics questions for each of the three cases.

In the first example , according to the priority rule enforced by the unless operator, two statements will be executable in the initial state: x!0 and y!0 . Either one could be selected for execution. If the first is executed, we enter a rendezvous offer, with handshake set to the ch_id of channel x . In the intermediate global state s' then reached (line 11-18 in the main execution loop of the semantics engine), only one statement can be added to set E' , namely x?0 . The final successor state will have handshake == 0 and both processes in their final state. Alternatively, y!0 could be selected for execution, with an analogous result.

In the second example , only one statement is executable in the initial system state: y!0 , and only the corresponding handshake can take place.

In the third example , the first two statements considered, at the highest priority, are both unexecutable. One priority level lower, though, two statements become executable: x!0 and y!0 , and the resulting two system executions are again analogous to those from the first example.

NOTES ON VERIFICATION
The addition of a verification option does not affect the semantics of a Promela model as it is defined here. Note, for instance, that the semantics engine does not include any special mention or interpretation of end states, accepting states, non-progress states, or assertions, and it does not include a definition for the semantics of a never claim. The reason is that these language elements have no formal semantics within the model: they cannot be used to define any part of the behavior of a model.

Assertions, special labels, and never claims are used for making meta statements about the semantics of a model. The verifier determines how such meta statements are to be interpreted.

When the verifier checks for safety properties, it is interested in cases where an assert statement can fail, or in the presence of finite executions with a final state that violate some proper termination condition (e.g., with all processes in a valid end-state, and all message channels empty). The predefined system variable stutter, used in the definition of the semantics engine on line 22, is set to False in this case, and any mechanism can be in principle used to generate the executions of the system, in search of the violations.

When the verifier checks for liveness properties, it is interested in the presence of infinite executions that either contain finitely many traversals of user-defined progress states, or infinitely many traversals of user-defined accept states. The predefined system variable stutter, used in the definition of the semantics engine on line 22, is set to True in this case, and, again, any mechanism can be used to generate the infinite executions, as long as it conforms to the semantics as defined before.

THE NEVER CLAIM
For purposes of verification it is not necessary that indeed all finite or infinite executions that comply with the formal semantics are also generated. In fact, the verifier Spin will make every effort to avoid generating all possible executions, and instead concentrate its efforts on a minimal set of executions that could possibly produce counter-examples. This is where the never claim comes in: the never claim does not define new semantics, but is used to identify that part of the existing semantics that violates an independently stated correctness criterion.

The interpretation of the never claim by the verifier in the context of the semantics engine is as follows. Note that the purpose of the claim is to suppress the inspection of executions that could not possibly lead to a counter-example. To accomplish this, the verifier will reject some valid executions as soon as possible. The evaluation whether an execution should be rejected or continued can happen in two places: at line 2 of the semantics engine, and at line 22.

  1 while ((E = executable(s)) != {})
 *2 {	if (check_fails()) Stop;
  3 	for some {p,t} from E
    . . .
 21 }
*22 while (stutter) { s = s; if (check_fails()) Stop; }
The check is implemented in Spin as a check to see if the never claim automaton can execute at least one more transition. When the claim is generated from an LTL formula, all its transitions are condition statements, formalizing atomic propositions on the global system state. Only infinite executions that are consistent with the formal semantics of the model and with the constraint expressed by the never claim can now be generated.

With or without a constraint provided by a never claim, a verifier hunting for violations of liveness properties can check infinite executions for those that constitute counter-examples to a correctness property. The precise method that the verifier uses to recognize and report those infinite executions is of course critical to the verification process, but irrelevant to the Promela semantics definition given here.


Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage
(Page Updated: 28 November 2004)