Information Technology Reference
In-Depth Information
From a modelling point of view, we do not object to such a representation or
see any diculty to write it down in an mCRL2 specification. Unfortunately,
for a formal analysis with tools that require an explicit state space generation
such as model-checking tools, this has an apparent drawback. It gives rise to 2
32
different potential contents for each position in each of the considered buffers.
This number is usually too big to be handled by current state-of-the-art model-
checking tools. For that reason we require an appropriate abstraction.
Investigation shows that only two types of data packets are relevant for the
Simplified Switch. First, those data packets for which the first bit of the packet
is 0, and second, those data packets for which the first bit is 1. According to the
first bit, packets are respectively routed to output buffer 0 or to output buffer
1. For this reason, we choose to abstract from the irrelevant bits of a packet, by
only modeling the first bit. Consequently, the structure of a packet is redefined
as:
sort
Packet
=
struct
packet
(
b
1
:
Bit
);
To route packets, we require a function that assigns a destination to a given
packet. So, we define a mapping
dest
that expresses the relation between the
data within the packet and the output buffer to which the packet is to be routed.
map
dest
:
Packet
;
eqn
dest
(
packet
(
zero
)) = 0;
dest
(
packet
(
one
)) = 1;
→
N
3.2
Capacity of the Buffers
The system consists of four queues. Each buffer has the same capacity
cap
,which
is assumed to be at least 1. In order to specify the case study without referring
to an explicitly defined value we introduce the following constant.
map
cap
:
Pos
;
By means of an equation we may assign a specific value to this mapping. This
is necessary for state space generation and simulation of the specification. This
way changing the capacity, if desired, needs to be done in one place only.
eqn
cap
=3;
3.3
Information Exchange between the Processes
To observe packets that enter and leave the 2
2-switch, two parameterized ac-
tions are introduced, namely one for adding an element to an input buffer (
enter
)
and another one for removing an element from an output buffer (
leave
). The first
data parameter refers to the identity of an input buffer (for
enter
-actions) or an
output buffer (in case of
leave
-actions). The second data parameter is used to
represent the actual data for the packet itself.
×
