Protocol Engineering

Protocol Specification using
Sequence Chart or Message Flow DiagramApply Formal Method To Protocol Specification

The use of Formal Method

Specification Languages

Communicating Finite State Machines (CFSM)

CFSM operating semantic

Networks of CFSMs

CFSM Modeling Exercises

Pros and Cons of the CFSM model

The Alternating Bit Protocol as CFSMs

The Alternating Bit Protocol is used to guarantee the correct data delivery between a sender and receiver connected by an error channel that loses or corrupts messages. It got the name since it uses only one additional control bit in the message and this control bit only alternates when the previous message is correctly received.....

Verifying the Alternating Bit Protocol

Assume that C1 is the outgoing channel of the sender and C2 is the outgoing

channel of the receiver. Let us assume that C1 loses the odd numbered messages, i.e., the 1st, 3rd, 5th, and so on, while C2 delivers every message.

Let S be the sender, R be the receiver, and E stands for an empty channel.

Let the 4-tuple (sender state, receiver state, C1 content, C2 content)

represent the global state, a snapshot of the overall system state.

The following state transition sequence illustrates that the

alternating bit protocol in page 8 is capable of delivering data without

duplication and in the right order.

(1,1,E,E)--S:NewData-->(2,1,E,E) sender receives data, x, from its upper layer

(2,1,E,E)--S:-D0-->(3,1,D0,E) sender attaches a sequence bit 0 after x. D=x

(3,1,D0,E)--C1:lose D0-->(3,1,E,E)


(7,1,E,E)--S:-D0-->(3,1,D0,E) retransmit D0

(3,1,D0,E)--R:+D0-->(3,2,E,E) This time C1 correctly delivers the message.

(3,2,E,E)--R:DeliverDate-->(3,3,E,E) receiver delivers x to its upper layer



(4,4,E,E)--S:NewData-->(5,4,E,E) sender receives data, y, from its upper layer

(5,4,E,E)--S:-D1-->(6,4,D1,E) sender attaches a sequence bit 1 after y. D=y

(6,4,D1,E)--C1:lose D1-->(6,4,E,E) this is the third message received by C1


(8,4,E,E)--S:-D1-->(6,4,D1,E) retransmit D1

(6,4,D1,E)--R:+D1-->(6,5,E,E) This is the fourth msg. C1 delivers it.

(6,5,E,E)--R:DeliverData-->(6,6,E,E) receiver delivers y to its upper layer



Note that the message sequence xy from the upper layer of the sender is correctly delivered to the upper layer of the receiver.

Protocol Verification using Reachability Analysis

Reachability Analysis

Protocol Design Errors

Protocol Verification Exercises

More Exercise on Reachability Analysis

Pros and Cons of Reachability Analysis



Tools for specification development

I have ported the state exploration tool of PROSPEC to X window system.

It is called setool.

Homework #2

Exercise 1. Reachability Analysis. Given the following network of two communicating finite state machines,

a) Perform the reachability analysis on the Network (M, N).
b) What sizes of buffers are needed for the two FIFO channels?
c) Are there non-executable states or transitions?
Exercise 2. Describe the event sequence (starting from initial states) of the alternating bit protocol, if both channels lose every other message (it loses the 1st, 3rd, 5th,... messages it received)? Each event can be identified as <machine, src-state, dst-state, msglabel> or <channel, lost msg | deliver msg> Include events up to the one that successfully delivers A1.