SmartAHS Components For Simulating Communication
Abstract
This document describes SHIFT models for Automated Highway System (AHS)
communication components. These components must model the following layers
of the open systems interconnection (OSI) reference: physical layer, media
access control layer, logical link layer, network layer and transport layer.
The functionalities of those layers have been adapted to AHS communication
needs.
1. Modeling communication with SHIFT
Communication in the Smart-AHS introduces a major problem. We want to interface
the communication domain with the vehicle domain, but to simulate communication,
the time unit required is around 
;
using this time unit to simulate vehicle traffic implies an extremely long
simulation time. A way to solve this problem is to simulate the system
(vehicle + communication) with a ``reasonable'' step in terms of simulation
last and to aggregate the communication in this new unit. With this technique,
the communication will not be modeled at the bit level, but at the message
level. This solution is restrictive in the sense that it does not allow
to observe efficiency and protocol delays. Nonetheless knowing the characteristics
of a protocol (delay, throughput, etc.), we can model what happens during
each time unit.
In this document, we focus on the message level approach, and we describe
SHIFT components to simulate communication at the physical layer, at the
media access control (MAC) layer and at the Logical Link Control (LLC)
Layer. Other layers are not implemented yet. Note that modeling the communication
at the bit level has also many interesting features, and should be done
in the future.
2. Communication Components
2.1 Message
The Message type model messages being sent between users. It must
be sub-typed to describe each N-Protocol Data Unit (i.e. the data format
at the level N).
The messageType output specifies whether the message is a supervisory
frame ($S) or an information one ($I). The connectionType output
gives information about the type of the connection: unicast, broadcast,
multi-cast. The SHIFT description of the Message type is given below:
type Message
{
output symbol messageType;
output symbol connectionType;
}
2.2 Physical Layer
The physical layer implements an unreliable link on which bits are transmitted.
A link consists of a transmitter, a receiver, and a medium over which signals
are propagated. The Transmitter type is an interface to model the
communication transmitter, and the Receiver type is an interface
to model the communication receiver. Medium properties, such as the capacity
and the transmission rate, are modeled in a component called monitor.
Other medium properties, such as propagation error, co-channel and channel
interference, can be described in the Receiver. The monitor
type also models the connection (both for point-to-point and for multi-cast
channel) and the medium access control protocol (in the case of multi-cast
channel).
2.2.1 Transmitter interface
The interface for the Transmitter type allows to model transmitters
for point to point, broadcast and multi-cast communication.
To send a unicast message, the higher layer must synchronize with the
MAC_ready_point event and it must provide the receiverIn
and messageIn inputs.
In the case of broadcast communication, the higher layer must synchronize
with the MAC_ready_broad event, and it must provide the messageIn
input .
In the case of multi-cast communication, the higher layer must synchronize
with the MAC_ready_multi event, and it must provide the receiversIn
and messageIn inputs.
The receiver (or receivers) output refers to the destination(s)
of the message and the message output is the message to send.
When transmitting a unicast message, the transmitter issues the MAC_data_point
event. The receivers belonging to the same network as the transmitter synchronize
with the transmitter's MAC_data_point event and they check if they
are the destination of the message (i.e. if they are equal to the receiver
output of the transmitter).
When transmitting a multicast message, the transmitter issues the MAC_data_multi
event. The receivers belonging to the same network as the transmitter synchronize
with the transmitter's MAC_data_multi event and they check if they
are the destinations of the message (i.e. if they belong to the receivers
output of the transmitter).
When transmitting a broad-cast message, the transmitter issues the
MAC_data_broad event. The receivers belonging to the same network
synchronize with the transmitter's MAC_data_broad event.
After the message is sent with unicast communication, the transmitter
issues the MAC_confirm_point event. In the case of multi-cast communication,
the transmitter issues the event MAC_confirm_multi or, in the case
of broadcast communication it issues the MAC_confirm_broad event.
The SHIFT description of the interface of the Transmitter type
is given below:
type Transmitter
{
output Receiver receiver; // Destination of the transmitted message.
set(Receiver) receivers; // Destinations of the transmitted message.
Message message; // Message being transmitted.
input Receiver receiverIn; // One receiver specified for
// unicast communication.
set(Receiver) receiversIn; // A set of receivers specified
// for multi-cast communication.
Message messageIn; // Message to be transmitted.
export
closed MAC_confirm_point, // Issued when a unicast message
// has been transmitted.
MAC_confirm_multi, // Issued when a multi-cast message
// has been transmitted.
MAC_confirm_broad; // Issued when a broadcast
// message has been transmitted.
open MAC_ready_point, // Issued when the transmitter is ready
// to transmit a unicast message.
MAC_ready_multi, // Issued when the transmitter is ready
// to transmit a multi-cast message.
MAC_ready_broad, // Issued when the transmitter is ready
// to transmit a broadcast message.
MAC_data_point, // Issued when transmitting a unicast message.
MAC_data_multi, // Issued when transmitting a multi-cast message.
MAC_data_broad, // Issued when transmitting a broadcast message.
exiting;
discrete init;
transition
all -> exit {exiting}; // Each subtype of Transmitter must have
} // this transition.
2.2.2 Receiver interface for a perfect channel
The interface for the Receiver type allows to model receivers for
point to point, broadcast and multi-cast communication.
The Receiver type describes a perfect channel. It must be sub-typed
in order to model errors, due to propagation, co-channel and channel interference.
The transmitter output refers to the transmitter that sent out
the message and the message output contains the message that was
sent.
The TxNetwork input is the set of transmitters that are involved
in the same network. Note that this set can be connected to the set of
transmitters which is defined in the Monitor type. In this way the
user won't have to update this variable when a transmitter leaves or joins
the network.
To receive a unicast message, the receiver must synchronize with the
MAC_data_point event of one of the transmitters in the TxNetwork
variable.
To receive a broadcast message, the receiver must synchronize with
the MAC_data_broad event of one of the transmitters in the TxNetwork
variable.
To receive a multi-cast message, the receiver must synchronize with
the MAC_data_multi event of one of the transmitters in the TxNetwork
variable.
If the receiver is the destination of the transmitted message, it issues
the MAC_indication_point event (for unicast communication), the
MAC_indication_multi event (for multi-cast communication) or the
MAC_indication_broad event (for broadcast communication).
The SHIFT description of the interface for the Receiver type
is given below:
type Receiver
{
output Transmitter transmitter; // transmitter of the received message.
Message message; // received message.
input set(Transmitter) TxNetwork; // transmitters involved in the same network.
export MAC_indication_point, // Issued when a unicast message
// has been received.
MAC_indication_broad, // Issued when a broadcast message
// has been received.
MAC_indication_multi, // Issued when a multi-cast message
// has been received.
exiting;
discrete
init;
transition
init -> exit {exiting};
}
2.2.3 Receiver interface for an imperfect channel
A subtype of the Receiver type has been implemented to model channel
errors (due to propagation and co-channel and channel interference).
For unicast communication, when the receiver issues the MAC_indication_point
event, it also issues a message status event (error_free_frame or
error_frame).
For multi-cast communication, the receiver issues the event MAC_indication_multi,
only if the message arrives error free, otherwise, the receiver deletes
the message.
For broadcast communication, the receiver issues the event MAC_indication_broad,
only if the message arrives error free, otherwise, the receiver deletes
the message.
The probability to estimate the percentage of wrong messages is stored
in a global variable called ErrorTransmission. It has to be set
when the simulation begins.
The SHIFT description for the Receiver interface is given below:
type ErrReceiver : Receiver
{
export error_free_frame, // Issued when the message is error
free.
error_frame;
// Issued when the message is not error free.
discrete
init;
transition
init -> exit {exiting};
}
global number ErrorTransmission := 0;
2.2.4 Interface for the Monitor
The Monitor works as a centralized component and there is one for
each network. It models some physical layer and some MAC layer functionalities.
On one hand, the Monitor is a representation of a set of users
adopting the same physical medium; it models channel properties and keeps
track of the transmitters sharing the channel. The Monitor also
models the connection type (point to point or broadcast channel).
On the other hand, communication is not simulated in real time, instead
we aggregate many transmissions in a time unit, called slot, the length
of which is defined at the beginning of the simulation. For each slot,
a centralized algorithm (defined in the Monitor) decides which transmitters
are allowed to transmit. Since point-to-point and multi-access channel
are different from each other, Monitor has to be subclassed in order
to manage the two cases.
For a point-to-point connection, the number of allowed exchanges in
the next slot is a function of channel capacity, of transmission rate and
of packet length. For a broadcast channel, the number of allowed exchanges
is also function of the throughput of the media access function.
The MAC layer functionality of the Monitor are discussed, in
more details, in the MAC layer section. The SHIFT description of the interface
for the Monitor type is given below:
type Monitor
{
output
set(Transmitter) transmitters
:= {};
number PacketLenght
:= L;
number Efficiency
:= a; // Propagation and detection delay.
number DataRate
:= C; // Data rate in Kbps.
number TransmissionTime
:= Ts; // Transmission time in sec.
number Throughput;
// Effective throughput of the system.
number TheoriticalThroughput;
// Theoretical throughput of the system.
}
global number slot := 1;
// Unit of the aggregate step
// in sec ( shift step must be smaller).
2.3 Data Link Layer
Networks can be divided into two categories: those using point-to-point
connections and those using a broadcast or multi-access channel (that is
when the same communication link is shared between several users). In the
case of point-to-point connection, the main task of the Data Link Layer
is to provide to the higher layer a virtual error free packet link. In
the case of broadcast channel, the Data Link Layer is split into two sub-layers,
the media access control sub-layer (MAC) and the Logical Link Control sub-layer
(LLC). The purpose of the MAC layer is to allocate the multi-access medium
among the various users. The functionalities of the LLC are those of the
Data Link Layer for a point-to-point connection. The MAC layer and the
LLC layer constitute the Data Link Layer for a multi-access channel. Access
control is performed by the Monitor type and the LinkLayer
type models the LLC.
2.3.1 MAC Layer
When the same communication link is shared between several users, we need
an additional sub-layer between the LLC and the physical layer. This extra
layer is called Medium Access Control layer. Its purpose is to allocate
the multi-access medium among the various users.
There are two extremes among the different algorithms designed for
this issue. The fist extreme is the ''free for all'' approach, in which
a user sends a message hoping for no interference from other users. The
second one is ''perfectly scheduled'' approach, in which some order is
estabilished among the users for channel usage.
The media access function is embedded in the Monitor, which
must be sub-typed in order to support different media access algorithms.
Features of the Monitor type
As we already mentioned, the monitor is a centralized component, that is
assigned to a network. It provides informations about the medium and it
monitors all the exchanges (or throughput) allowed in a slot. For point-to-point
communication, the throughput depends on slot duration and on channel properties.
For a broadcast channel, the throughput depends on slot duration, channel
properties and on the chosen MAC protocol. In both cases throughput is
the number of successfully delivered packets per packet transmission time.
Note that if the used throughput is the number of successfully sent packets,
the hidden conflict and the transmission during the critical period (collision
due to the use of one channel by several hosts) are part of the model;
the propagation errors (due to interference with other networks for example)
are modeled in the receiver.
The Monitor type must be sub-typed in order to implement specific
MAC layer protocols, such as CSMA or Token Ring.
For CSMA, the monitor keeps track of how many transmitters ask to send
data, and it uses this load to compute the number of transmitters allowed
to transmit in the next slot.
Interface for the Monitor
The Monitor type has a transmitters output variable. It is
the set of transmitters belonging to the network, which is described by
that Monitor. This set is updated by the transmitters themselves
(in their setup action or in the initial transition).
type Monitor
{
output set(Transmitter) transmitters := {};
}
2.3.2 Logical Link Layer
The purpose of the the Logical Link Layer is to transfer messages without
error in the case of unicast communication. For broadcast (or multi-cast)
communication, the error correction must be done at an upper layer.
The Logical Link Layer interface is described in the LinkLayer
type and it has to be subtyped in order to implement a specific error control
algorithm.
Each LinkLayer component belongs to one network, and can deal
with several connections at the same time. The following two paragraphs
provide a description of the Buffer type and of the Link type. Both of
them are used by the LinkLayer.
Interface for the Buffer
To write in the buffer, the user must provide the ItemIn input and
he must synchronize with the buffer's not_full event. To read and
delete an item in the buffer, the user must synchronize with the buffer´s
not_empty event. After this the value to be read can be found in
the ItemOut output.
The SHIFT description of the interface for the Buffer type is
given below:
function modulo(number index;
// The modulo function is a C
number bufferSize) // function used by the
-> number; // Buffer
type.
type Buffer
{
input Message itemIn;
// Message to record.
output Message itemOut;
// Message to read.
number
getPlace := 0; // Index of the next message
to read.
number
putPlace := 0; // Index of the next message
to write.
number
numberOfItems := 0; // Number of recorded message.
number
bufferSize; // Size of
the buffer.
array(Message) buffer;
// Array of recorded messages.
setup do { buffer := [nil : i in [0 .. bufferSize - 1]];};
export open not_empty,
not_full;
discrete
empty,
// Buffer accessible in writing only.
neither,
// Buffer accessible in writing and reading.
full;
// Buffer accessible in reading only.
transition
empty -> neither {not_full}
do {
buffer[putPlace] := itemIn;
numberOfItems := numberOfItems + 1;
putPlace := modulo((putPlace
+ 1), bufferSize );
},
neither ->empty {}
when numberOfItems <= 0,
neither -> neither {not_full}
do {
buffer[putPlace] := itemIn;
numberOfItems := numberOfItems + 1;
putPlace := modulo((putPlace
+ 1), bufferSize);
},
neither -> neither {not_empty}
do {
itemOut := buffer[getPlace];
numberOfItems := numberOfItems - 1;
getPlace := modulo((getPlace + 1), bufferSize);
},
neither -> full {}
when numberOfItems >= bufferSize,
full -> neither {not_empty}
do {
itemOut := buffer[getPlace];
numberOfItems := numberOfItems -1;
getPlace := modulo((getPlace + 1), bufferSize);
};
}
The LL_Buffer subtype doesn't delete the item immediately after
reading it. To delete the last read message, the user must explicitly synchronize
with the buffer's cancel event.
Interface for the Link
Each connection between a local and a remote user is modeled at the Data
Link Layer by the Link type. There are several informations that
must be remembered about a Data Link connection. These informations are
stored in a type called Link.
Among the outputs in Link are the remote and local LinkLayer
(or a set of LinkLayer in the case of multi-cast communication)
and a reference to the local user's two buffers (one to read from messages
from the upper layer and one to write messages to the upper layer). In
addition there are several variables dealing with the send and receive
sequence numbers.
When a LinkLayer component receives a new message from the local
user to a remote user, it creates a Link to model this connection.
A few parameters must be set in the Link: the connection type (unicast,
broadcast, multi-cast), the size of the buffers and a reference to the
remote LinkLayer (or a set of remote LinkLayer in case of
multi-cast communication).
A Link is also created when the LinkLayer receives a new
message from a remote user. Therefore for each connection, two Link
instances are created (one at the source and one at the destination).
Note that Link must be subtyped according to the error correction
algorithm used at the Logical Link Layer.
The SHIFT description of the interface for the Link type is given
below:
type Link
{
output symbol
connectionType; // $UNI, $BROAD, $MULTI.
LinkLayer
destination; // Remote linkLayer(s)
involved
set(LinkLayer) destinations
:= {}; // in the connection
LinkLayer
source;
LL_Buffer
rBuffer; // Buffer accessible in reading by the linkLayer.
LL_Buffer
wBuffer; // Buffer accessible in writing by the linkLayer.
number
bufferSize;
// The following variables
are used by the Stop and Wait
// protocol implemented at
the Logical Link Layer.
number
sequenceNumber := 0;
number
requestNumber := 0;
symbol
LastFrameAck := YES;
symbol
LastFrameNack := NO;
setup define {
LL_Buffer t_rBuffer := create(LL_Buffer,
link := self,
bufferSize := bufferSize);
LL_Buffer t_wBuffer := create(LL_Buffer,
link := self,
bufferSize := bufferSize);
}
do {
rBuffer := t_rBuffer;
wBuffer := t_wBuffer;
};
discrete init,
establish;
export open exiting;
transition
init -> establish {}
define {
LinkLayer t_linkLayer := source;
}
do {
Links(t_linkLayer) := Links(t_linkLayer) + {self};
},
all -> exit {exiting};
}
Interface for the Logical Link Layer
The LinkLayer type is an interface for the Logical Link Layer. It
must be sub-typed in order to implement different error correction algorithms.
At creation time, the receiver and transmitter outputs
must be properly initialized.
For unicast communication, when the network layer wants to send data,
it must provide the following inputs: messageIn and destinationIn
(the LinkLayer at the remote host). It must also synchronize with
the LL_ready event.
For multi-cast communication, when the network layer wants to send
data, it must provide the following inputs: messageIn and destinationsIn
(which is a set containing the LinkLayers at the remote hosts).
It must also synchronize with the LL_ready event.
For broadcast communication, when the network layer wants to send data,
it must provide the following messageIn input and it must synchronize
with the LL_ready event.
Each connection between local and remote users is modeled through the
Link type. When an error free frame arrives, the LinkLayer
stores the frame in the write-buffer corresponding to this connection,
and issues an LL_indication event.
To receive the frame, the upper layer must synchronize on the LL_indication
event and it must also synchronize with the link's buffer where the
frame was stored. The itemOut output of this buffer contains the
frame to be read. To delete the frame and free the buffer, the upper layer
must synchronize with the cancel event issued by the buffer.
The SHIFT description of the interface for the LinkLayer type
is given below:
type LinkLayer
{
input Message messageIn; // Message to be transmitted.
LinkLayer destinationIn; // Message destination.
set(LinkLayer) destinationsIn; // Message destinations.
output Receiver receiver; // Receiver attached to the link layer.
Transmitter transmitter; // Transmitter attached to the link layer.
set(Link) Links := {}; // Set of connection recorded at the link layer.
number bufferSize; // Size of the buffers at the link layer.
export open LL_ready,
exiting;
closed LL_confirm,
LL_indication;
}
How Logical Error Control is Modeled
The problem: one protocol entity wants to send another protocol entity
a sequence of frames without errors.
The LinkLayer type has to model the four following scenarios:
corrupted frames, lost frames, mis-ordered frames, duplicated frames. It
also has to set up the following three error control mechanisms: acknowledgment,
timeout, checksum (see figure1).
| Scenario |
Cause |
Detection Method |
| corrupted msg |
bit error on the link |
checksum |
| lost msg |
congestion |
ack/timeout |
| mis-ordered msg |
different paths and retransmission |
sequence # |
| duplicated msg |
retransmission |
sequence # |
Figure 1. Possible scenarios and detection methods
Error control mechanisms:
- acknowledgment: tells the sender what has (not) been received (ACK
or NACK)
- timeout: an entity waits a given amount of time before retransmitting
(sender timeout) or asking to retransmit (receiver timeout).
- checksum.
At the sender, we model three scenarios:
(1) the receiver issues the error_free_frame event; the new
frame is a supervisory frame which acknowledges the last sent frame and
asks for the next one.
(2) the receiver issues the error_free_frame event; the new
frame is a supervisory frame but does not acknowledge the last frame sent
and asks for a retransmission.
(3) the receiver issues the error_frame event; the new frame
is a corrupted supervisory frame. This mechanism allows us to model the
timeout. The sender retransmits the last frame.
Figure 2 shows the simplified logical error control mechanism at the
transmitter.
At the receiver, we model three scenarios:
(1) the receiver issues the error_free_frame event; the new
frame is a data frame and its sequence number corresponds to the expected
sequence number. The remote user sends back an acknowledgment and asks
for the next frame.
(2) the receiver issues the error_free_frame event; the new
frame is a data frame but its sequence number does not correspond to the
expected sequence number (it's a duplicate). The remote user asks for the
next frame.
(3) the receiver issues the error_frame event; the new frame
is a corrupted data frame. The remote user asks for the same frame.
Figure 3 shows the simplified logical error control mechanism at the
receiver.
3. Examples
In this chapter we describe the subtypes of Transmitter, Receiver, Monitor
and LinkLayer, implementing a point-to-point connection using Stop-And-Wait
algorithm at the Logical Link Layer. For a broadcast channel, one can find
a lot of algorithms to provide the functionalities required by the MAC
and the LLC layer. We made a selection among all these algorithms and we
decided to model a semi persistent network, and a persistent network. For
the semi persistent network, we used a Carrier Sense Multiple Access (CSMA)
protocol at the MAC layer and a Stop-And-Wait (SAW) protocol at the Logical
Link Control layer.
For the persistent network, we used a Token Ring protocol at the MAC
layer and a Stop-and-Wait (SAW) protocol at the Logical Link Control layer.
3.1 Point-to-point connection
In order to model a point to point connection, Transmitter, Receiver
and Monitor are subtyped in UniPointTransmitter, GnrErrReceiver
and UniPointLink.
3.1.1 The UniPointTransmitter type
Figure 4 shows the logical behavior of the Transmitter sub-type
for a point-to-point connection. The transmitter begins in the idle
state. When creating the transmitter, the user must initialize the
monitor output. In its setup action, the transmitter adds itself
to the Transmitters output variable of the monitor. This variable
is a set of Transmitter which is used by the monitor to detect ready-to-transmit
transmitters.
The higher layer must synchronize with the MAC_ready_point event.
It must also provide the messageIn and receiverIn inputs.
Then the transmitter moves to the check_point state and stores the
message and the destination of the message in its message and receiver
outputs. After this it goes in the get_channel_point state and
issues the get_channel event. The monitor must synchronize
with this event to keep track of all the ready-to-transmit transmitters
during a slot.
The monitor must synchronize with the MAC_data_point event to
begin the transmission. To defer the transmisson to the next slot the monitor
synchronizes with the backlogged event.
After transmitting the message, the transmitter issues the MAC_confirm_point
event.
The SHIFT description of the UniPointTransmitter is given below
in several fragments.
Output
type UniPointTransmitter : Transmitter
{
output UniPointLink uniPointMonitor; // Monitor involved in the
...} // point-to-point connection
State
type UniPointTransmitter : Transmitter
{
state number timer := 0;
flow defer_law {timer' = 1;};
...}
Exported events
type UniPointTransmitter : Transmitter
{
export
open backlogged,
getChannel;
...}
Transition
-
In this transition, the transmitter adds itself to the monitor's set of
transmitters.
type UniPointTransmitter : Transmitter
{
transition
init -> idle {}
do {
uniPointTransmitters(uniPointMonitor)
:= uniPointTransmitters(uniPointMonitor)
+ {self};
},
...}
-
The higher layer must synchronize with the transmitter's MAC_ready_point
event and it must provide the messageIn and receiverIn inputs
to send a message.
type GnrCsmaTransmitter : Transmitter
{
transition
idle -> check_point {MAC_ready_point},
...}
-
The transmitter checks the status of the channel. The monitor must synchronize
with the getChannel event to keep track of all the ready-to-transmit
transmitters in a slot.
type GnrCsmaTransmitter : Transmitter
{
transition
check_point -> get_channel_point
{getChannel}
do {
receiver := receiverIn;
message := messageIn;
},
...}
-
This transition is taken when the transmitter is not allowed to transmit.
The monitor must synchronize with the transmitter's backlogged event
to defer its transmission.
type GnrCsmaTransmitter : Transmitter
{
transition
get_channel_point -> defer_point {backlogged},
...}
-
The transmitter senses again the channel, one slot later.
type GnrCsmaTransmitter : Transmitter
{
transition
defer_point -> get_channel_point
{getChannel}
when timer >= slot
do {
timer := 0;
},
...}
-
The monitor must synchronize with the transmitter's MAC_data_point
event to start the transmission.
type GnrCsmaTransmitter : Transmitter
{
transition
get_channel_point -> transmit_point
{MAC_data_point},
...}
-
The transmitter issues the MAC_confirm_point event when the message
is sent.
type GnrCsmaTransmitter : Transmitter
{
transition
transmit_point -> idle {MAC_confirm_point},
...}
3.1.2 The GnrReceiver and GnrErrReceiver Types
The Receiver type is the same for point-to-point connection and
for a broadcast channel. Figure 5 shows the logical behavior of the Receiver
for unicast communication.
The receiver starts in the awaiting state. It moves to the forwarding_point
state by synchronizing with the MAC_data_point event of one of the
transmitters in the TxNetwork variable. In this state, the receiver
checks if it is the destination of the message. If it is not, it goes back
to awaiting. If it is, it issues the MAC_indication_point
event and goes back to awaiting.
The SHIFT description of the GnrReceiver for unicast, broadcast,
and multi-cast communication is given below.
type GnrReceiver : Receiver
{
state
Receiver receiver;
set(Receiver) receivers;
discrete
awaiting,
forwarding_point,
forwarding_multi,
forwarding_broad;
transition
awaiting -> forwarding_point
{TxNetwork:MAC_data_point(one:t)}
do {
transmitter := t;
receiver := receiver(t);
message := message(t);
},
forwarding_point -> awaiting
{}
when receiver /= self
do {
transmitter := nil;
message := nil;
},
forwarding_point -> awaiting
{MAC_indication_point}
when receiver = self,
awaiting -> forwarding_multi
{TxNetwork:MAC_data_multi(one:t)}
do {
transmitter := t;
receivers := receivers(t);
message := message(t);
},
forwarding_multi -> awaiting
{}
when not (self in receivers)
do {
transmitter := nil;
message := nil;
},
forwarding_multi -> awaiting
{MAC_indication_multi}
when (self in receivers),
awaiting -> forwarding_broad
{TxNetwork:MAC_data_broad(one:t)}
do {
transmitter := t;
message := message(t);
},
forwarding_broad -> awaiting
{MAC_indication_broad},
all -> exit {exiting};
}
The SHIFT description of the GnrErrReceiver for an non-perfect
channel is given below.
type GnrErrReceiver : GnrReceiver
{
state number ErrorProbability := 0;
Receiver receiver;
set(Receiver) receivers;
export error_free_frame, // Issued when the message
is error free.
error_frame;
// Issued when the message is not error free.
discrete
awaiting,
forwarding_point,
forwarding_multi,
forwarding_broad;
transition
awaiting -> forwarding_point
{TxNetwork:MAC_data_point(one:t)}
do {
transmitter := t;
receiver := receiver(t);
message := message(t);
ErrorProbability := random();
},
forwarding_point -> awaiting
{}
when receiver /= self
do {
transmitter := nil;
message := nil;
ErrorProbability := 0;
},
forwarding_point -> awaiting
{MAC_indication_point, error_free_frame}
when receiver = self
and ErrorProbability >= ErrorTransmission
do {
ErrorProbability := 0;
},
forwarding_point -> awaiting
{MAC_indication_point, error_frame}
when receiver = self
and ErrorProbability <
ErrorTransmission
do {
transmitter := nil;
message := nil;
ErrorProbability := 0;
},
awaiting -> forwarding_multi
{TxNetwork:MAC_data_multi(one:t)}
do {
transmitter := t;
receivers := receivers(t);
message := message(t);
ErrorProbability := random();
},
forwarding_multi -> awaiting
{}
when not (self in receivers)
do {
transmitter := nil;
message := nil;
},
forwarding_multi -> awaiting
{MAC_indication_multi}
when (self in receivers)
and ErrorProbability >= ErrorTransmission
do {
ErrorProbability := 0;
},
forwarding_multi -> awaiting
{}
when (self in receivers)
and ErrorProbability <
ErrorTransmission
do {
transmitter := nil;
message := nil;
ErrorProbability := 0;
},
awaiting -> forwarding_broad
{TxNetwork:MAC_data_broad(one:t)}
do {
transmitter := t;
message := message(t);
ErrorProbability := random();
},
forwarding_broad -> awaiting
{MAC_indication_broad}
when ErrorProbability >= ErrorTransmission
do {
ErrorProbability := 0;
},
forwarding_broad -> awaiting
{}
when ErrorProbability <
ErrorTransmission
do {
ErrorProbability := 0;
},
all -> exit {exiting};
}
3.1.3 The UniPointLink Monitor Type
Figure 6 shows the logical behavior of the Monitor subtype for point-to-point
connection.
The monitor begins in the Wait state. In every slot, the monitor
allows a fixed number of transmissions. The number of allowed transmissions
is called TheoreticalThroughput and it is calculated in the monitor's
setup action.
If TxThisSlot is greater than 0, the monitor moves to phase1
by synchronizing with the getChannel event of one of the transmitters
in the transmitters variable. If TxThisSlot is less than
0, the monitor moves to state phase2 by synchronizing with the getChannel
event of one of the transmitters in the transmitters variable.
In phase1, the monitor allows the transmission by synchronizing
with the specific transmitter's MAC_data_point event. In phase2,
the monitor defers the transmission by synchronizing with the specific
transmitter's backlogged event.
The SHIFT description of the Monitor subtype is given below.
type UniPointLink : Monitor
{
output set(UniPointTransmitter) uniPointTransmitters := {};
state
number timer := 0;
number TxThisSlot;
UniPointTransmitter uniPointTransmitter;
flow default { timer' = 1;};
setup define {
number t_TransmissionTime := PacketLenght / DataRate;
number t_TheoriticalThroughput := ( slot
/ t_TransmissionTime);
}
do {
TransmissionTime := t_TransmissionTime;
TheoriticalThroughput := t_TheoriticalThroughput;
};
discrete
await,
phase1,
phase2;
transition
await -> await {}
when timer >= slot
do {
TxThisSlot := TheoriticalThroughput;
timer := 0;
},
await -> phase1 {uniPointTransmitters:getChannel(one:t)}
when TxThisSlot > 0
do {
TxThisSlot := TxThisSlot - 1;
uniPointTransmitter := t;
},
await -> phase2 {uniPointTransmitters:getChannel(one:t)}
when TxThisSlot = 0
do {
uniPointTransmitter := t;
},
phase1 -> await {uniPointTransmitter:MAC_data_point},
phase2 -> await {uniPointTransmitter:backlogged};
}
3.2 Broadcast channel: CSMA at the MAC layer
3.2.1 CSMA algorithm
At the MAC layer we use a Carrier Sense Multiple Access protocol. A description
of the algorithm is given below.
* The model of a transmitter A is:
A has a message to send to B.
A senses the channel (busy or idle):
if idle,
A transmits the message and then deletes it
A waits for a new message from the higher layer
else
A waits a random delay before sensing again the channel.
* The model of a receiver B is:
B receives a message from A
B computes the Cyclic Redundancy Code (CRC) and compares it with
the CRC in the message:
if the CRCs are equal,
the message is forwarded to the higher layer
else
the message is deleted.
In order to model CSMA, Transmitter, Receiver and Monitor
are subtyped in GnrCsmaTransmitter, GnrErrReceiver and GnrCsma.
These subtypes support unicast, broadcast and multi-cast communication.
3.2.2 The GnrCsmaTransmitter Type
The SHIFT description of the GnrCsmaTransmitter for unicast, broadcast,
and multi-cast communication is given below in several fragments.
Output
type GnrCsmaTransmitter : Transmitter
{
output GnrCsma gnrCsmaMonitor; // Monitor involved in the CSMA network.
...}
State
type GnrCsmaTransmitter : Transmitter
{
state number timer := 0;
flow defer_law
{ // When a transmitter is backlogged, it
timer' = 1; // waits one slot before sensing again
}; // the channel. The timer models this
...} // delay.
Exported events
type GnrCsmaTransmitter : Transmitter
{
export
open backlogged,
getChannel;
...}
Transition
-
In this transition, the transmitter adds itself to the monitor's set of
transmitters.
type GnrCsmaTransmitter : Transmitter
{
transition
init -> idle {}
do {
gnrCsmaTransmitters(gnrCsmaMonitor)
:= gnrCsmaTransmitters(gnrCsmaMonitor) + {self};
},
...}
-
This transition is for unicast communication. The higher layer must synchronize
with the transmitter's MAC_ready_point event and it must provide
the messageIn and receiverIn inputs.
type GnrCsmaTransmitter : Transmitter
{
transition
idle -> check_point {MAC_ready_point},
...}
-
This transition is for unicast communication. It is taken when the transmitter
checks the status of the channel. The monitor must synchronize with the
getChannel event to keep track of all the ready-to-transmit transmitters
in a slot.
type GnrCsmaTransmitter : Transmitter
{
transition
check_point -> get_channel_point {getChannel}
do {
receiver := receiverIn;
message := messageIn;
},
...}
-
This transition is for unicast communication. It is taken when the transmitter
is not allowed to transmit. The monitor must synchronize with the transmitter's
backlogged event to defer its transmission.
type GnrCsmaTransmitter : Transmitter
{
transition
get_channel_point -> defer_point
{backlogged},
...}
-
This transition is for unicast communication. it is taken when the transmitter
senses again the channel, one slot later.
type GnrCsmaTransmitter : Transmitter
{
transition
defer_point -> get_channel_point
{getChannel}
when timer >= slot
do {
timer := 0;
},
...}
-
This transition is for unicast communication. It is taken when the transmitter
sends data. The monitor must synchronize with the transmitter's MAC_data_point
event to allow it to start its transmission.
type GnrCsmaTransmitter : Transmitter
{
transition
get_channel_point -> transmit_point
{MAC_data_point},
...}
-
The transmitter issues the MAC_confirm_point event when the message
is sent.
type GnrCsmaTransmitter : Transmitter
{
transition
transmit_point -> idle {MAC_confirm_point},
...}
-
The following set of transitions are for multi-cast and broadcast communication.
The approach is the same than for point to point communication: only event
names are different.
type GnrCsmaTransmitter : Transmitter
{
transition // Multicast transitions
idle -> check_multi {MAC_ready_multi},
check_multi -> get_channel_multi
{getChannel}
do {
receivers := receiversIn; // Set of receivers.
message := messageIn;
},
get_channel_multi -> defer_multi
{backlogged},
defer_multi -> get_channel_multi
{getChannel}
when timer >= slot
do {
timer := 0;
},
get_channel_multi -> transmit_multi
{MAC_data_multi},
transmit_multi -> idle {MAC_confirm_multi},
...}
type GnrCsmaTransmitter : Transmitter
{
transition // Broadcast transitions
idle -> check_broad {MAC_ready_broad},
check_broad -> get_channel_broad {getChannel}
do {
message := messageIn;
},
get_channel_broad -> defer_broad {backlogged},
defer_broad -> get_channel_broad {getChannel}
when timer >= slot
do {
timer := 0;
},
get_channel_broad -> transmit_broad {MAC_data_broad},
transmit_broad -> idle {MAC_confirm_broad},
all -> exit {exiting};
}
...}
3.2.3 The CSMA Receiver
The Receiver subtype for point to point connection can also be used
for CSMA.
3.2.4 The GnrCsma Monitor Type
The monitor begins in the Wait state. In every slot, it computes
the number of transmitters that will be allowed to transmit in the next
slot. This number is stored in TxThisSlot.
TxThisSlot is computed as follows.
Let the throughput S be the number of successfully delivered packets
per packet transmission time Tp. Let G be the number of transmitters which
wanted to transmit in the last slot (offered traffic load in packets per
packet time). Let a be the propagation and detection delay (in packet
transmission unit) that is required for all sources to detect an idle channel
after transmission ends.
a is defined as a = tau * Tp, where tau is the
propagation delay. The throughput of the non-persistent CSMA protocol is
given by: S = (G exp(-aG)) / (G*(1+2a) + exp(-aG)) .
Assuming that the TheoreticalThroughput is the number of packets
that can be transmitted in one slot as a function of capacity C
and packet length L, than we define TxThisSlot := floor (TheoriticalThroughput
* S)
Example:
If C=11.2Kb/s, L=50Bytes, and slot=1sec, then
the TheoreticalThroughput is 28 packets in one slot. Assuming that
G is the number of transmitters which wanted to transmit in the
last slot, say 4, and a=0.01 we get S=0.76 and we conclude
that TxThisSlot = 17 packets can be successfully transmitted during
the next slot.
The SHIFT description of the Monitor is given below.
type GnrCsma : Monitor
{
output set(GnrCsmaTransmitter) gnrCsmaTransmitters := {};
state number timer := 0;
number TxThisSlot := 0; // Transmitters allowed to transmit in
// the next slot.
number SumTx := 0; // Transmitters which want to transmit during
// the slot.
GnrCsmaTransmitter gnrCsmaTransmitter;
//Current requesting transmitter.
flow
default {
timer' = 1;
};
setup
define {
number t_TransmissionTime := PacketLenght / DataRate;
number t_TheoreticalThroughput := (slot / t_TransmissionTime);
}
do {
TransmissionTime := t_TransmissionTime;
TheoreticalThroughput := t_TheoreticalThroughput;
};
discrete
await,
phase1,
phase2;
transition
await -> await {}
when timer >= slot
define {
number t_SumTx := SumTx;
number t_Throughput := (t_SumTx * exp(-a*t_SumTx))
/ (t_SumTx*(1+2*a) + exp(-a*t_SumTx));
}
do {
Throughput := t_Throughput;
TxThisSlot := floor(TheoreticalThroughput * t_Throughput);
SumTx := 0;
timer := 0;
},
await -> phase1 {gnrCsmaTransmitters:getChannel(one:t)}
when TxThisSlot > 0
do {
gnrCsmaTransmitter := t;
TxThisSlot := TxThisSlot - 1;
SumTx := SumTx + 1;
},
await -> phase2 {gnrCsmaTransmitters:getChannel(one:t)}
when TxThisSlot = 0
do {
gnrCsmaTransmitter := t;
SumTx := SumTx + 1;
},
phase1 -> await {gnrCsmaTransmitter:MAC_data_point},
phase1 -> await {gnrCsmaTransmitter:MAC_data_multi},
phase1 -> await {gnrCsmaTransmitter:MAC_data_broad},
phase2 -> await {gnrCsmaTransmitter:backlogged};
}
3.3 Broadcast Channel: Stop And Wait at the Logical Link Control (using
CSMA at the MAC layer)
3.3.1 Stop And Wait algorithm
At the Data Link layer we use the simplest retransmission protocol called
Stop_And_Wait protocol (SWP). Whenever the receiver gets a correct packet
it transmits an acknowledgment back to the sender. The sender automatically
sends a copy of the packet if it does not get the acknowledgment within
T seconds. The packets and the acknowledgments are numbered. The channel
between the sender and the receiver is half-duplex, so the packets and
the acknowledgments can not propagate at the same time.
A description of the Stop_And_Wait algorithm is given below.
* The algorithm at node A for A-to-B transmission
1) Set the integer variable SN (Sequence Number) to 0.
2) Accept a packet from the higher layer; assign SN to this new packet.
3) Transmit the SNth packet in a frame containing SN in a sequence
number field.
4) If an error-free frame is received from B containing a Request
Number greater than SN, increase SN to RN and go to step 2. If no such
frame is received go to step 3.
* The algorithm at node B for A-to-B transmission
1) Set the integer variable RN to 0 and then repeat step 2 and 3
forever.
2) Whenever an error-free frame is received from A containing a
sequence number SN equal to RN. Release the received packet to the
higher layer and increment RN.
3) After receiving any error-free data frame from A, transmit a frame
to A containing RN in the requesting number field.
3.3.2 State machine for Stop And Wait Logical Link Layer
Figure 7 shows the logical behavior of the LinkLayer subtype implementing
the Stop and Wait algorithm for unicast communication. Broadcast and multi-cast
communication are omitted for legible reasons.
3.3.3 SHIFT description for LL_Message type
Message is subtyped to model the N-Protocol Data Unit at the Logical
Link Layer.
type LL_Message : Message
{
output symbol messageType; // Supervisory or Information.
number sequenceNumber; // Used by the SAW protocol.
number requestNumber; // Used by the SAW protocol.
LinkLayer destination; // linkLayer at the remote user.
set(LinkLayer) destinations := {}; // linkLayer at the remote users.
LinkLayer source; // linkLayer at the local user.
Message message; // N-Protocol Data Unit from
// the Network Layer.
}
3.3.4 SHIFT description for LinkLayer type
The SHIFT description for the Logical Link Layer using Stop_And_Wait protocol
for unicast communication is given below in several fragments.
Inputs
type UniCsmaLinkLayer : LinkLayer
{
input Message messageIn;
LinkLayer destinationIn;
} ....
Outputs
type UniCsmaLinkLayer : LinkLayer
{
output UniErrReceiver uniErrReceiver;
UniCsmaTransmitter uniCsmaTransmitter;
LL_Message message_from_host;
LL_Message message_to_host;
set(LL_Message) Acknowledgments := {};
Link link;
flow default {
uniCsmaTransmitter = narrow (UniCsmaTransmitter, transmitter);
uniErrReceiver = narrow (UniErrReceiver, receiver);
};
...}
States
type UniCsmaLinkLayer : LinkLayer
{
...
state LL_Buffer rBuffer;
LL_Buffer wBuffer;
symbol ReadyToSendData := NO;
...}
Discrete Transitions
-
The upper layer must synchronize with the LL_ready event and it
must provide the destinationIn and messageIn inputs. The
first and the third terms in the guard imply that the transition may be
taken when the connection to destinationIn does not exist:
a new Link will be created (currently there is no maximum number
of connections allowed). The second term of the guard implies that the
transition may be taken when the connection to destinationIn already
exists and its read-buffer is not full. MessageIn is assigned to
the itemIn input of the read-buffer.
type UniCsmaLinkLayer : LinkLayer
{
...
transition
connected -> network_ready {LL_ready}
when size (Links) = 0
or exists i in Links :
(destination(i) = destinationIn
and numberOfItems(rBuffer(i))
/= bufferSize(rBuffer(i)))
or not(exists j in Links :
(destination(j) = destinationIn))
define {
LinkLayer t_destination := destinationIn;
Message t_message := messageIn;
Link t_link := find{i: i in Links
| (t_destination = destination(i))}
default {create(Link,
sequenceNumber := 0,
requestNumber := 0,
destination := t_destination,
source := self,
bufferSize := bufferSize,
LastFrameAck := YES)};
LL_Buffer t_rBuffer := rBuffer(t_link) ;
}
do {
itemIn(t_rBuffer) := t_message;
rBuffer := t_rBuffer;
destinationIn := nil;
messageIn := nil;
},
....
}
-
Synchronization between the LinkLayer and the read-buffer that was chosen
in the network_ready state. When issuing the not_full event,
the buffer stores the message that was written in its itemIn input.
type UniCsmaLinkLayer : LinkLayer
{
...
transition
network_ready -> connected {rBuffer : not_full},
....
}
-
The linkLayer is looking for a new message to transmit. The first term
of the guard implies that the transition is taken only if the previous
message_from_host has been transmitted; The second term of the guard
implies that at least a connection has its last frame acknowledged and
another frame to transmit. In the read_buffer state, the linkLayer
records the chosen connection in its link output.
type UniCsmaLinkLayer : LinkLayer
{
...
transition
connected -> read_buffer {}
when ReadyToSendData = NO
and (exists i in Links : LastFrameAck(i) = YES
and (numberOfItems(rBuffer(i)) /= 0))
define {
Link t_link := find {i : i in Links
| LastFrameAck(i) = YES
and (numberOfItems(rBuffer(i)) /= 0)};
LL_Buffer t_rBuffer := rBuffer(t_link) ;
}
do {
rBuffer := t_rBuffer;
link := t_link;
ReadyToSendData := YES;
},
....
}
-
The linkLayer is looking for a new message to transmit. This transition
is parallel to the previous one. The first term of the guard implies that
the transition is taken only if the previous message_from_host has
been transmitted; The second term of the guard implies that at least a
connection has its last frame NOT acknowledged. In the read_buffer
state, the linkLayer records the chosen connection in its link output.
type UniCsmaLinkLayer : LinkLayer
{
...
transition
connected -> read_buffer {}
when ReadyToSendData = NO
and (exists j in Links : LastFrameNack(j) = YES
and (numberOfItems(rBuffer(j)) /= 0))
define {
Link t_link := find {i : i in Links
| LastFrameNack(i) = YES
and (numberOfItems(rBuffer(i)) /= 0)};
LL_Buffer t_rBuffer := rBuffer(t_link) ;
}
do {
rBuffer := t_rBuffer;
link := t_link;
ReadyToSendData := YES;
},
....
}
-
Synchronization between the linkLayer and the read-buffer that was chosen
in the read_buffer state. When issuing the not_empty event,
the buffer saves the next frame to send in its itemOut output.
type UniCsmaLinkLayer : LinkLayer
{
...
transition
read_buffer -> record_buffer {rBuffer : not_empty},
....
}
-
The linkLayer copies the next message to send from the buffer, and creates
a LL_message with the informations needed by the remote linkLayer.
type UniCsmaLinkLayer : LinkLayer
{
...
transition
record_buffer -> connected {}
define {
Message t_message := itemOut(rBuffer);
LL_Message t_LL_message := create(LL_Message,
messageType := I,
source := self);
}
do {
message_from_host := t_LL_message;
message(t_LL_message) := t_message;
source(t_LL_message) := source(link);
destination(t_LL_message):= destination(link);
sequenceNumber(t_LL_message)
:= modulo(sequenceNumber(link), 2);
requestNumber(t_LL_message)
:= modulo(requestNumber(link), 2);
LastFrameAck(link) := NO;
LastFrameNack(link) := NO;
ReadyToSendData := YES;
link := nil;
rBuffer := nil;
},
....
}
-
When the linkLayer is ready to send the next frame, it must synchronize
with the transmitter's MAC_ready_point event.
type UniCsmaLinkLayer : LinkLayer
{
...
transition
connected -> transmit {uniCsmaTransmitter : MAC_ready_point}
when ReadyToSendData = YES
do {
messageIn(uniCsmaTransmitter) := message_from_host;
receiverIn(uniCsmaTransmitter)
:= receiver(destination(message_from_host));
ReadyToSendData := NO;
},
...}
-
When the message has been sent the linkLayer issues the LL_confirm closed
event.
type UniCsmaLinkLayer : LinkLayer
{
...
transition
transmit -> connected {LL_confirm}
do {
message_from_host := nil;
},
...}
-
A message has been received error free by the receiver. There is synchronization
on the error_free_frame event between the receiver and the linkLayer.
The linkLayer stores the new message in its output variable message_to_host.
type UniCsmaLinkLayer : LinkLayer
{
...
transition
connected -> frame_arrival_error_free {uniErrReceiver : error_free_frame}
define {
Message t_message := message(uniErrReceiver);
LL_Message t_ll_message := narrow(LL_Message, t_message);
}
do {
message_to_host := t_ll_message;
},
...}
-
If the message is a supervisory one the linklayer goes in the supervisory_frame
state (acknowledgment from the remote linkLayer). The linkLayer copies
in its link output the link corresponding to the connection.
type UniCsmaLinkLayer : LinkLayer
{
...
transition
frame_arrival_error_free -> supervisory_frame {}
when messageType(message_to_host) = $S
define {
LinkLayer t_source := source(message_to_host);
Link t_link := find {i : i in Links
| (destination(i)
= t_source)};
}
do {
link := t_link;
rBuffer := rBuffer(t_link);
},
...}
-
The message acknowledges the last sent frame; the linkLayer goes back to
the connected state by synchronizing with the specific buffer's
cancel event, and remembers that the last sent frame (for this connection)
was acknowledged.
type UniCsmaLinkLayer : LinkLayer
{
...
transition
supervisory_frame -> connected {rBuffer : cancel}
when (requestNumber(message_to_host) =
modulo((sequenceNumber(link) + 1), 2))
define {
Link t_link := link;
}
do {
sequenceNumber(t_link) := requestNumber(message_to_host);
LastFrameAck(t_link) := YES;
LastFrameNack(t_link) := NO;
link := nil;
rBuffer := nil;
message_to_host := nil;
},
...}
-
The message does not acknowledge the last sent frame; the linkLayer goes
back to the connected state, and remembers that the last sent frame
(for this connection) was not acknowledged. The remote user asks for a
retransmission.
type UniCsmaLinkLayer : LinkLayer
{
...
transition
supervisory_frame -> connected {}
when (sequenceNumber(link) = requestNumber(message_to_host))
define {
Link t_link := link;
}
do {
LastFrameNack(t_link) := YES;
link := nil;
rBuffer := nil;
message_to_host := nil;
},
...}
-
The linklayer goes in the information_frame state if the message
is an information message (data from the remote linkLayer). In this state,
the linkLayer determines which link, among those in its set, is the one
which corresponds to this connection; if no such link exists, the linkLayer
creates one.
type UniCsmaLinkLayer : LinkLayer
{
...
transition
frame_arrival_error_free -> information_frame {}
when messageType(message_to_host) = $I
define {
LinkLayer t_source := source(message_to_host);
Link t_link := find {i: i in Links
| t_source = destination(i)}
default {create(Link,
sequenceNumber := 0,
requestNumber := 0,
destination := t_source,
source := self,
bufferSize := bufferSize,
LastFrameAck := YES,
LastFrameNack := NO)};
}
do {
link := t_link;
wBuffer := wBuffer(t_link);
},
...}
-
The message was expected; The linkLayer passes it to the write-buffer that
was chosen in information_frame.
type UniCsmaLinkLayer : LinkLayer
{
...
transition
information_frame -> frame_expected {}
when sequenceNumber(message_to_host)
= requestNumber(link)
do {
itemIn(wBuffer) := message(message_to_host);
requestNumber(link) := modulo((requestNumber(link) + 1), 2);
},
...}
-
Synchronization between the linkLayer and the specific write-buffer. When
issuing the not_full event, the buffer saves the message that was
written in itemIn.
type UniCsmaLinkLayer : LinkLayer
{
...
transition
frame_expected -> to_host {wBuffer : not_full}
do {
message_to_host := nil;
},
...}
-
The LL_indication event is issued when a message has arrived error
free. In the build_ack state, the linkLayer creates a supervisory
message to acknowledge the received message and to ask for the next one.
type UniCsmaLinkLayer : LinkLayer
{
...
transition
to_host -> build_ack {LL_indication}
define {
LL_Message t_acknowledgment
:= create(LL_Message,
messageType := S,
source := self,
destination := destination(link),
sequenceNumber := sequenceNumber(link),
requestNumber := requestNumber(link));
}
do {
Acknowledgments := Acknowledgments + {t_acknowledgment};
},
...
}
-
The frame is not expected. It is a duplicate.
type UniCsmaLinkLayer : LinkLayer
{
...
transition
information_frame -> duplicated_frame {}
when sequenceNumber(message_to_host)
= modulo((requestNumber(link) + 1), 2)
do {
message_to_host := nil;
},
...
}
-
In the build_ack state, the linkLayer creates a supervisory message
asking for the next frame.
type UniCsmaLinkLayer : LinkLayer
{
...
transition
duplicated_frame -> build_ack {}
define {
LL_Message t_acknowledgment
:= create(LL_Message,
messageType := S,
source := self,
destination := destination(link),
sequenceNumber := sequenceNumber(link),
requestNumber := requestNumber(link));
}
do {
Acknowledgments := Acknowledgments + {t_acknowledgment};
},
...
}
type UniCsmaLinkLayer : LinkLayer
{
...
transition
build_ack -> connected {}
do {
link := nil;
rBuffer := nil;
},
...
}
-
The linkLayer synchronizes with the transmitter's MAC_ready_point
event to send an acknowledgment.
type UniCsmaLinkLayer : LinkLayer
{
...
transition
connected -> transmit_ack {uniCsmaTransmitter : MAC_ready_point}
when size(Acknowledgments) /= 0
define {
LL_Message t_acknowledgment := choose{i : i in Acknowledgments};
LinkLayer t_destination := destination(t_acknowledgment);
}
do {
messageIn(uniCsmaTransmitter) := t_acknowledgment ;
receiverIn(uniCsmaTransmitter) := receiver(t_destination);
Acknowledgments := Acknowledgments
- {t_acknowledgment};
},
...}
type UniCsmaLinkLayer : LinkLayer
{
...
transition
transmit_ack -> connected {},
...}
-
A message has been received with an error by the receiver. There is synchronization
with the receiver's error_frame event. The linkLayer saves the new
message on its output message_to_host.
type UniCsmaLinkLayer : LinkLayer
{
...
transition
connected -> frame_arrival_error {uniErrReceiver : error_frame}
define {
Message t_message := message(uniErrReceiver);
LL_Message t_ll_message := narrow(LL_Message, t_message);
}
do {
message_to_host := t_ll_message;
},
...}
-
The wrong message is a supervisory message. The linkLayer seeks the link
corresponding to this connection and remembers that the last frame, for
this connection, was not acknowledged. This mechanism allows us to model
the timeout (the acknowledgment was lost or is wrong). The sender has to
resend the last frame.
type UniCsmaLinkLayer : LinkLayer
{
...
transition
frame_arrival_error -> time_out {}
when messageType(message_to_host) = S
define {
LinkLayer t_source := source(message_to_host);
Link t_link := find {i : i in Links
| (destination(i)
= t_source)};
}
do {
link := t_link;
LastFrameNack(t_link) := YES;
},
...}
type UniCsmaLinkLayer : LinkLayer
{
...
transition
time_out -> connected {}
do {
link := nil;
rBuffer := nil;
message_to_host := nil;
},
...}
-
The wrong message is an information message. The linkLayer seeks the link
corresponding to this connection or creates one. The resulting link is
then stored in the link output.
type UniCsmaLinkLayer : LinkLayer
{
...
transition
frame_arrival_error -> wrong_frame {}
when messageType(message_to_host) = I
define {
LinkLayer t_source := source(message_to_host);
Link t_link
:= find {i : i in Links
| (destination(i) = t_source)
default {create(Link,
sequenceNumber := 0,
requestNumber := 0,
destination := t_source,
source := self,
bufferSize := bufferSize,
LastFrameAck := YES,
LastFrameNack := NO)};
}
do {
link := t_link;
},
...}
-
The frame was not received correctly by the linkLayer. A retransmission
is needed.
type UniCsmaLinkLayer : LinkLayer
{
...
transition
wrong_frame -> build_ack {}
define {
LL_Message t_acknowledgment
:= create(LL_Message,
messageType := S,
source := self,
destination := destination(link),
sequenceNumber := sequenceNumber(link),
requestNumber := requestNumber(link));
}
do {
Acknowledgments := Acknowledgments + {t_acknowledgment};
},
...}
type UniCsmaLinkLayer : LinkLayer
{
...
transition
all -> exit {exiting};
...}
3.4 Broadcast channel: Token Ring at the MAC layer
3.4.1 Token Ring algorithm
In a Token Ring network the hosts are connected in the shape of a ring.
The protocol is based on the use of a small frame called token, that circulates
when all users are idle. A ready-to-transmit user has to wait until
it detects the next available token as it passes by. When a station seizes
a token and begins to transmit a data frame, there is no token in the ring,
so other users wishing to transmit must wait. The transmitting user will
insert a new token on the ring when both of the following conditions are
met: the user has completed the transmission of its frame and an acknowledgment
from the destination of the frame has been received.
In order to implement the basic functionalities of the token ring protocol
the Transmitter type and the Monitor type have been subtyped
with UniTokenTransmitter and UniToken. Currently only unicast
communication is implemented.
The following features of the Token Ring protocol are not implemented:
1) there is no initialization sequence. When a user joins the network,
it should go through an initialization sequence to become part of the ring.
This is done to inform the neighbors of its existence.
2) there is no active monitor. The active monitor