Information Technology Reference
In-Depth Information
x
:
D
P
P
::=
α
P
+
P
P
·
P
c
→
P
P
P
∂
B
(
P
)
τ
B
(
P
)
Γ
V
(
P
)
X
(
d
)
α
::=
τ
a
(
d
)
α
|
α
The small
indicates a choice between symbols in the expression of the BNF. In
this syntax
α
denotes a multi-action. A multi-action consists of actions combined
by the big
. The empty multi-action is denoted by
τ
.Anaction
a
(
d
) consists
of an action name
a
and possibility a data parameter vector
d
(the syntax of
which is left unspecified). A multi-action represents the simultaneous execution
of the constituent actions.
Processes are denoted by
P
. For processes, + denotes non-deterministic choice,
i.e., a choice between behaviors,
|
·
denotes sequential composition, i.e., a process
followed by another process. The conditional operator, written as
c
→
p
, denotes
that if
c
data expression of sort
holds, then process
P
is executed. The non-
deterministic choice among processes is denoted by
x
:
D
P
,where
x
is a variable
of sort
D
and
P
is a process expression in which the variable
x
may occur. The
parallel composition of processes is represented by
operator, that denotes the
concurrent execution of both processes. The operator
∂
B
blocks all actions from
set
B
of action names, i.e., prevents the occurrence of the specified actions.
The operator
τ
B
replaces all occurrences of actions from
B
by
τ
.
Γ
V
applies the
communications described by the set
V
to a process. A communication in the
set
V
is of the form
a
1
B
a
. Application of
Γ
V
to a process means
that any occurrence of the multi-action
a
1
(
d
)
| ··· |
a
n
→
a
n
(
d
) is replaced by
a
(
d
),
for any
d
.
X
(
d
) is a reference to a process definition of the form
X
(
x
)=
P
, i.e.,
the process
X
(
d
) behaves as prescribed by
P
with
x
replaced by
d
.
The semantics associated with an mCRL2 process, as used in the mCRL2 tool
set, is a transition system where the transitions are labelled by multi-actions.
A more elaborate description of the syntax and (timed) semantics are given
in [9,10].
| ··· |
2.2
Modal
µ
-Calculus
Modal
μ
-calculus formulae are used to describe behavioral properties. These
properties are verified against a behavioral model described in mCRL2. In this
paper, requirements are specified in a variant of the modal
μ
-calculus extended
with regular expressions [8] and data. The restricted fragment of the modal
μ
-calculus used, is as follows:
φ
::=
false
φ
⇒
φ
φ
∧
φ
[
ρ
]
φ
ρ
φ
∀
x
:
D
φ
c
ρ
∗
ρ
::=
α
ρ
·
ρ
α
::=
a
(
d
)
¬
α
α
|
α
true
In this syntax,
φ
represents a property,
ρ
represents a set of sequences of actions
and
α
represents the absence or presence of a multi-action. An arbitrary multi-
action is denoted by
true
. The property
false
holds for no model. The property
[
ρ
]
φ
states the property that
φ
holds in all states that can be reached by a
