- Principles, p1
- Applications, p1
- Examples, p2
- Manual Pages, p3
- Contact, p3
Examples
Alternating Bit Protocol
The alternating bit protocol is part of the 4th OSI transport layer. It allows the exchange of messages betweeen two entities, a transmitter and a receiver, linked by unreliable communication channels.
The protocol is composed by four asynchronous processes : a transmitter, a receiver and the two communication channels between them. The communication is performed via 6 ports, which link the processes and their environnment. The SMI description of this protocol is given in the following files :
bitalt.exp
hide SEND, RECEIVE, ACK, SENDACK in
(transmitter.aut ||| receiver.aut )
|[ SEND, RECEIVE, ACK, SENDACK]|
( medium1.aut ||| medium2.aut )
bitalt.types
bitalt.order
medium1 : 0 medium1 : b1 medium1 : m1
receiver : 0 receiver : me receiver : br receiver : cr
medium2 : 0 medium2 : b2
transmitter.aut
me : nat
des (0, 5, 3)
( 0, be :=false ce :=true, 1)
( 1, receive ACCEPT ?me, 2)
( 2, [ (be <=> ce)] send SEND !me !be, 2)
( 2, [ (be <=> ce)] receive ACK ?ce, 2)
( 2, [be <=> ce] be := be, 1)
medium1.aut
m1 : nat
des ( 0, 3, 2)
( 0, receive SEND ?m1 ?b1, 0)
( 0, receive SEND ?m1 ?b1, 1)
( 1, send RECEIVE !m1 !b1, 0)
medium2.aut
des (0, 3, 2)
( 0, receive SENDACK ?b2, 0)
( 0, receive SENDACK ?b2, 1)
( 1, send ACK !b2, 0)
receiver.aut
mr : nat
des (0, 4, 2)
( 0, br :=true cr :=false, 1)
( 1, [ (br<=>cr)] send SENDACK !br, 1)
( 1, [ (br<=>cr)] send RECEIVE ?mr ?br, 1)
( 1, [br <=>cr] send TRANSMIT !mr cr := cr, 1)
