AccordingtoHolzmann [14], protocol speci?cationscomprise ?veelements:
the service the protocol provides toits users; the set of messages that
are exchanged between protocol entities; the format of each message; the
rules governingm- sage exchange (procedures); and the assumptionsabout
the environment in which the protocol is intended tooperate. In protocol
standards documents, information related to the operatingenvironment
isusually writteninformally andmayoccur in several di?erentplaces
[37]. This informal speci?cation style canlead to misunderstandings
andpossibly incompatible implementations. In contrast,
executableformalmodelsrequireprecisespeci?cations oftheoperating
environment. Ofparticularsigni?canceisthecommunicationmediumorchannel
over which the protocol operates. Channelscan havedi?erent
characteristics depending on the physical media (e. g. optical ?bre,
copper, cable orunguided media (radio)) they employ. The characteristics
also depend on the levelof the protocol inacomputer protocol
architecture. Forexample, the link-leveloperates over a singlemedium,
whereas the network, transport andapplication levelsmayoperate over a
network, or network of networks such as the Internet, which couldemploy
several di?erent physical media. Channels (such as satellite links) can
be noisy resulting in bit errors in packets. To correct biterrors in
packets, many importantprotocols (such the Internet's
TransmissionControl Protocol [27]) use CyclicRedundancy Checks
(CRCs)[28] to detect errors. On detectingan error, the receiver
discards the packet andrelies on the sender to retransmit itforrecovery,
known as Au- maticRepeatreQuest(ARQ)[28].
Thisisachievedbythereceiveracknowledging the receipt of good packets,
andby the transmitter maintainingatimer. When the timer expires before
an acknowledgementhasbeen received, the transmitter retransmits packets
that havebeen sent but are as yet notacknowledged. It may also be
possibleforpacketsto be lost due to routers in networks discarding
packets when congested.
