Information Technology Reference
In-Depth Information
#
include "c3to1.rsl"
1
#
include "c1to3.rsl"
2
4
CIRCUIT peerLink
{
5
// instantiation with port names including the reconf. ports:
first
=
new c3to1(A
[
0
],
A
[
1
],
A
[
2
],
6
here_is_reconf_port_first
;
C) with initial_topo
=
3
;
7
second
=
new c1to3(C
,
here_is_reconf_port_second
;
9
B
[
0
],
B
[
1
],
B
[
2
]
) with initial_topo
=
3
;
10
/*
12
defining the interface using
13
two differnt ways in accessing
14
the reconf_port of dynamic sub
-
circuits
15
*/
16
source
[
0
]=
first.RECONF_PORT
;
17
source
[
1
]=
here_is_reconf_port_second
;
18
// defining the rest of the interface
20
for (i
=
0
;
i
<
3
;
i
=
i
+
1)
{
21
source
[
i
+
2
]=
A
[
i
];
22
sink
[
i
]=
B
[
i
];
23
}
24
}
25
Fig. 12.
RSL script composing a peer link
ASL
and
LTL
IO
by providing some examples that can be checked with the help
of
Ve r eo fy
. For this, we make use of the following notations inside the formulas:
-
indicates that ports
A
and
B
are active and no other port is.
-
#
A
refers to the data item observed at port
A
.
-
step
indicates an arbitrary step with or without observable dataflow.
-
the operators ; (concatenation),
{
A
,
B
}
∗
+
(star), and
(plus) correspond to the
standard operators for regular languages.
1. Deadlock freedom, in the sense that on all paths there is always a next step,
can be formalized by means of the following
CTL
formula.
AG[EX[true]]
2. With
BTSL
we can formalize a condition stating the existence of a path
with specific regular form. A sequence of actions is specified by a regular ex-
pression, where the atoms are constraints on a single step of the observable
dataflow. This can e.g. be instrumented to check the conformance between
the behavioral interfaces and the RSL model. The following formula states
the existence of a path, where the first server registers, the second client
opens a session and sends a request for the data with
key0
, the data is trans-
ferred, and the connections closed. The formula also requires that the path
leads to a state where both the request and the release buffer are empty.
