SMI

Symbolic Model Interface
  Sommaire  

 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

Lotos-Behavior

hide SEND, RECEIVE, ACK, SENDACK in

(transmitter.aut ||| receiver.aut )

|[ SEND, RECEIVE, ACK, SENDACK]|

( medium1.aut ||| medium2.aut )

bitalt.types

nat 30

bitalt.order

transmitter : 0 transmitter : ce transmitter : be transmitter : me

medium1 : 0 medium1 : b1 medium1 : m1

receiver : 0 receiver : me receiver : br receiver : cr

medium2 : 0 medium2 : b2

transmitter.aut

be, ce : bool

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

b1 : bool

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

b2 : bool

des (0, 3, 2)

( 0, receive SENDACK ?b2, 0)

( 0, receive SENDACK ?b2, 1)

( 1, send ACK !b2, 0)

receiver.aut

br, cr : bool

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)

Fischer Mutual Exclusion Protocol