Information Technology Reference
In-Depth Information
1
CIRCUIT c3to1
{
2
1
CIRCUIT c1to3
{
2
outport
=
NODE
;
inport
=
NODE
;
sink
[
0
]=
outport
;
source
[
0
]=
inport
;
3
3
for (i
=
0
;
i
<
3
;
i
=
i
+
1)
{
for (i
=
0
;
i
<
3
;
i
=
i
+
1)
{
5
5
inport
[
i
]=
NODE
;
outport
[
i
]=
NODE
;
6
6
source
[
i
]=
inport
[
i
];
sink
[
i
]=
outport
[
i
];
7
7
}
}
8
8
TOPO(0)
={
TOPO(0)
={
10
10
new SYNC(inport
[
0
];
outport)
;
new SYNC(inport
;
outport
[
0
]
)
;
11
11
}
}
12
12
TOPO(1)
={
TOPO(1)
={
14
14
new SYNC(inport
[
1
];
outport)
;
new SYNC(inport
;
outport
[
1
]
)
;
15
15
}
}
16
16
TOPO(2)
={
TOPO(2)
={
18
18
new SYNC(inport
[
2
];
outport)
;
new SYNC(inport
;
outport
[
2
]
)
;
19
19
}
}
20
20
TOPO(3)
={
TOPO(3)
={
22
22
// unconnected
// unconnected
23
23
}
}
24
24
}
}
25
25
Fig. 11.
RSL script for a building block in the
P2PConnection
for the
peerLink
. From the RSL code one can also see how the reconfiguration
port becomes an additional interface port of the sub-circuits
c3to1
and
c1to3
and
how it can be accessed. The
P2PConnection
is composed out of two
peerLinks
,one
for the requests and one for the answers.
3.2 Analysis of the Model
Vereofy provides model checking for branching time properties via the
CTL
-like
logic
BTSL
[24] and the alternating-time logic
ASL
[23], for linear time properties
via
LTL
IO
[5], as well as bisimulation checking [9]. The three logics allow reasoning
about the coordination principles and the dataflow in the network, i.e., between
components, as well as the internal states of the components and component
interfaces.
BTSL
(Branching Time Stream Logic) is a
CTL
-like logic with path
quantifiers and formulas built by standard temporal operators, extended by spe-
cial modalities to specify regular properties for data stream prefixes.
LTL
IO
is
likewise an extended version of
LTL
adapted to the constraint automata setting,
where the atomic propositions are either state predicates or I/O-guards.
ASL
(Alternating Stream Logic) extends
BTSL
by means to allow reasoning about
compatibility and the existence (and absence) of strategies for (alliances of) com-
ponents. In this section we illustrate the type of properties expressible in
BTSL
,
