The Use of Model Transformation in the INESS Project - Formal Methods for Components and Objects - page 169

sequence described by ρ . The property φ describes that φ holds in some

state that can be reached by a sequence from ρ . To describe action sequences
concatenation and iteration can be used. A more elaborate description of the
modal μ -calculus and its semantics can be found in [5,8].

ρ

3 Specification of the Simple 2 × 2Switch

The 2 2 Switch case study consists of three separate cases that gradually

increase in diculty. These cases are referred to as the “Simplified Switch”,
the “Original Switch” [4] and the “Modified Switch”. In the specification of the
three cases, we follow the informal description from [6] as closely as possible. This
means that we introduce a single process for each of the four buffers. By means of
the advanced communication mechanisms offered in mCRL2, we describe their
non-trivial interaction. In this section, and in the sections to follow, we discuss
the way in which we have dealt with the modeling challenges posed by the case
studies.
The Simplified Switch contains two input FIFO buffers and two output FIFO
buffers. All buffers have a unique identity, w.r.t. the type of buffer, e.g. each
input or output buffer corresponds to a numerical value, and a finite capacity
for storing packets. All buffers have the same capacity.
Each packet consists of 32 bits. Packets enter the system via the input buffers
and depart the system via the output buffers. Packets are transferred from an
input buffer to one of the output buffers based on the first bit of the packet: If
the first bit of a packet is 0, it is routed to the output buffer with identity 0,
and otherwise it is routed to the output buffer with identity 1.
The packets may only be transferred if the relevant output buffer is not full.
A buffer operates per clock cycle and can do at most one operation, namely
receive a packet, send a packet, or nothing. Furthermore, we require maximum
throughput, e.g. a packet should be transferred if it has the ability to. Next to
that, if packets from different input buffers are available for transferral to the
same output buffer, transferral of the packet from input buffer 0 gets priority
over transferral of the packet from input buffer 1.

×

3.1 Bits and Packets

Thedatatypeofbitsconsistsoftwodifferentvalues.InmCRL2,thisisdefined
as:

sort Bit = struct zero | one ;

In the case study, packets consist of 32 bits. This implies that a single packet can
be represented by 2 32 different configurations. mCRL2 allows the description of
such a data type without any problems; e.g., by a structured sort that composes
32 bits by:

sort Packet = struct packet ( b 1 ,b 2 ,...,b 32 : Bit );