Identifiant pérenne de la notice : 238882349
Notice de type
Notice de regroupement
Note publique d'information : 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