Information Technology Reference
In-Depth Information
Fig. 4.
Micro model - example of a possible Track Layout for the scenario
2.2 PROMELA
PROMELA [7] is a process-based language, used by the SPIN model-checker [6]
for the specification of models. It is possible to define properties using LTL
(Linear Temporal Logic) formulas, and verify if the formulas are true for a given
specification.
The language has a
C-like
syntax and constructs for receiving and sending
messages similar to the ones found in CSP (Communication Sequential Pro-
cesses) [5]. Processes in PROMELA can be created statically or dynamically
(
proctype
keyword). There is a special process, called
init
, used to initialize
a specification. Processes can exchange information through message channels
(
chan
keyword) or global variables (variables declared outside the scope of the
processes). Message channels can be asynchronous (the buffer of the message
channel can have
0). Message channels are typed, in
the sense that one has to explicitly declare the types of variables a channel might
receive. As well, PROMELA offers several functions used to check, for example,
if a channel is not full (
nfull(channel)
), not empty (
nempty(channel)
), empty
(
empty(channel)
), and others [7].
In PROMELA, nondeterminism is modeled in condition (
if ... fi
) or repeti-
tion (
do ... od
) structures. The entries of condition and repetition structures are
composed of guarded commands. Once the condition of a guarded command is
not satisfied, the entry is blocked, possibly blocking the process that contains it.
This blocking occurs until the condition is satisfied. In condition and repetition
structures, nondeterminism occurs when several entries have their conditions
satisfied. In this case, one of the possible paths is chosen in a nondeterministic
way. It is possible to define atomic structures (
atomic
N
messages, being
N>
) for a specification,
i.e.
, a sequence of statements that must be executed without interleaving with
the execution of statements of other processes. However, if there are guarded
commands inside an atomic structure and they are not satisfied, the structure
will lose its atomicity characteristic and will interleave its statements with other
processes. We can define enumeration types in PROMELA (
mtype
keyword).
One can insert assertions in a PROMELA specification. An assertion statement
evaluates an expression (
assert(expression)
) to true or false, each time the state-
ment is executed. If the expression evaluates to false, an error is generated and
the verification procedure stops. Finally, the language provides a special boolean
{
...
}
