Information Technology Reference
In-Depth Information
All three refinements are supported by the automatic refinement checker FDR
[3] which proves or refutes assertions of the form
P
M
Q
. FDR inputs processes
expressed in CSP
M
, which is now the
de facto
standard for machine-readable
CSP. CSP
M
expresses CSP by a small but powerful functional language, offering
constructs such as
lambda
and
let
expressions and supporting pattern matching
and currying. It also provides a number of predefined data types, including
Booleans, integers, sequences and sets, and allows user-defined data types. The
global event set is defined by the set of typed channel declarations of a CSP
M
script. The
-operator can be used to compute the set of events that complete
the set of given prefixes (e.g. channels). CSP
M
models can also be animated and
verified by LTL model checking using ProB [8].
{|
.
|}
3 The Transformation
T
In this section we present the transformation
T
that achieves the simulation
motivated in the Introduction.
T
models duration of events by splitting them.
Hidden transitions are exposed by introducing fresh events. The purpose of the
transformation is to put the transformed process
T
(
P
) into parallel with a con-
trol component that records the start and end events of every transition of the
original process
P
(including hidden events). The control component can then
record possible simultaneity in
T
and thus be used to compute possible concur-
rency in
P
.
Throughout this paper processes are expressed using the syntax
(
x
:
X
→
P
(
x
))
|
P
;
Q
|
P
Q
|
P
|
A
|
Q
|
P
\
A
|
P
Q
|
P
[
M
]
|
P
Q
for general choice, sequential composition, external choice, parallel composition,
hiding, internal choice, renaming and timeout respectively. Recall that general
choice includes the atomic processes and prefixing, by appropriate choice of
X
.
Renaming of event
x
to
y
in process
P
is written
P
[
x
y
], or more generally
P
[
M
]where
M
is a mapping from source events to target events. Recall that in-
terleaving (
←
|||
) is the special case of parallel composition without synchronization
|
∅
|
(
) in the interleaving semantics of CSP.
Let
s
,
sh
,
e
,
eh
be fresh channels relative to
Σ
P
. The transformation
T
is
defined as follows.
→
P
(
x
)) =
s
.
x
:
{
s
.
y
|
∈
}→
e
.
x
→
T
(
x
:
X
y
X
T
(
P
(
x
))
⊗
⊗
T
(
Q
)
,
⊗
⊗
T
(
P
Q
)=
T
(
P
)
for
=; and
=
T
(
P
|
A
|
Q
)=
T
(
P
)
|
{s.x ,e.x |x∈A}
|
T
(
Q
)
T
(
P
\
A
)=
T
(
P
)[
s
.
x
←
sh
.
x
,
e
.
x
←
eh
.
x
|
x
∈
A
]
T
(
P
Q
)=
sh
.
ic i
→
eh
.
ic i
→
(
T
(
P
)
T
(
Q
))
T
(
P
[
M
]) =
T
(
P
)[
s
.
x
←
s
.
y
,
e
.
x
←
e
.
y
|
(
x
,
y
)
∈
M
]
T
(
P
Q
)=
T
(
P
)
(
sh
.
to i
→
eh
.
to i
→
T
(
Q
))
Search WWH ::
Custom Search