Choi-a Decomposition Approach

A I ~ C O H P O S I T I O N 14~-£ROD FOR THE AI~gLYSIS A N D I~ESIG~I O F F I N I T E S T A T E P R O T O C O L S

Tat g. Choi and Raymond E. Miller*

Georgia Institute of Technology Atlanta, Georgia 30332

Abstract

fronting network architects remains the same: what principles can we draw on for the engineering of these systems? In this paper, we intend to address an important area of network architecture, that of protocol analysis and design. Despite the large number of networks in exis tence today and the experience gained from the implementation of these systems, the design and analysis of network protocols has remained ad hoc. Various efforts have been undertaken in the formal modeling of network protocols [2,3], yet these approaches have not solved the problem of complexity. Little has been done in the way of partitioning the analysis and design process, the use of canonical components for protocol design, or the establishment of practical theorems to aid in the analysis and design p r o c e s s [4,5]. To counteract the complexity of protocol analysis and design, we propose an approach of decomposition. Amongst the various ways of modeling protocols, we have chosen the finite state model for the following reasons. It is a simple, widely understood model, correctness conditions can be simply and completely stated, these conditions not only are decidable but usually have tractable algorithms for testing their validity, and it has been used with success in the modeling of many practical protocols. We realize that finite state models have their limitations, for example, a complete description of some protocols may require a large number of states. Yet, it is precisely the state explosion problem that we intend to solve in this paper, by showing that finite state protocols ~re conducive to structured techniques of analysis and design.

Finite state automata have been applied with success to the modeling of Computer Network Protocols. The interaction of finite state machines can be very complex especially if the protocol involves a large number of states. To counteract the complexity of analysis and design, we propose an approach of decomposition. Through this approach, the protocol graph can be partitioned into subgraphs each having a unique entry node and zero or more exit nodes. The exit nodes of one subgraph can be connected only to the entry nodes of other subgraphs. From the standpoint of protocol analysis, the correctness of the entire protocol graph can be inferred from the correctness of individual protocol subgraphs. From the standpoint of protocol design, the individual protocol subgraphs can be designed to correspond to different phases of the protocol. If the individual protocol subgraphs are designed correctly and the Connections between subgraphs conform to the structure discussed above, then we show that the entire protocol graph will operate correctly. I.

IITROIXJCTION

The early eighties has seen the proliferation of different types o f computer networks and their application in various areas. With this a variety of network architectures and protocols have arisen [I]. Whether the network under discussion be a local network offered b y a computer manufacturer or a long haul network offered by a common carrier, the question con-

II.

Permission to copy without fee all or part of this material is granted provided that the copies are not made or distributed for direct commercial advantage, the A C M copyright notice and the title of the publication and its date appear, and notice is given that copying is by persmission of the Association for Computing Machinery. To copy otherwise, or to republish, requires a fee and/or specific permission.

Protocols are modeled by processes exchanging messages through communication channels. In finite state protocols, the processes can be represented by finite state machines [6]. A commonly used model for finite state protocols is one based on the work of Zafiropulo, et. al. [7]. In this model, a finite state protocol is defined as follows: Defintion: A Finite State = (S,M,E,O,z) consists of:

Permission to copy without fee all or part of this material is granted provided that the copies are not made or distributed for direct commercial advantage, the ACM copyright notice and the title of the publication and its date appear, and notice is given that copying is by permission of the Association for Computing Machinery. To copy otherwise, or to republish, requires a fee and/or specific permission.

0-89791-113-X,/83/0010/0167500.75

Protocol

FSP

*Work on this paper was supported in part by National Science Foundation Grant MCS-8103608.

167 © 1983 A C M

TtUS PROTOCOL M O D E L

i.

S = {S ,S }, two disjoint 1 2 representlng the states of and P2 respectively.

finite sets processes P1

i. ii.

=

ii.

iii.

M = {MI2,M2.}, two finite sets, where represents ~he messages that can be from process PI to process P 2 and represents the messages that can be from process P2 to process PI*

MI 2 sent M21 sent

iii.

for every message x e Mij , the sending of message x is denoted by -x. Every send event -x is an element of Z.. 1

(2)

for every message x E M.., the 13 receiving of message x is denoted by +x. Every receive event +x is an element of Z.. 3

(3)

0 = { o i , o 2 }, where 01 e S. and 02 e S 2 • o I and o 2 are the initia~ states for processes PI and P2 respectively.

v.

T a transition function: S. x Z. ÷ S., 1 .I i~I,2. The transition functlon f~r event o E Z. at state s can be w r i t t e n as T (s,o). ~ t represents the next state reached by a process after executing event o at state s.

If T' = 01,~2,...,0 n is a sequence then let T = ST' = o, o1,~2,...,c n.

of

We now define the following col errors.

for

four types of proto-

events, i.

U n s p e c i f i e d Reqe~tions: A reception for message x at state s is unspecified iff it is not live.

ii.

Nonexecutable Interactions: A transition T(s,o) at state s for event o is nonexecutable iff it is specified and not executable.

iii.

State Deadlocks: A state deadlock is a stable state pair S = (si,sj) such that there is no x for wSich T (s~,-x) or T(s~,-x) is specified and S is ~ot a final ~ystem state.

iv.

State Ambiguities: A state ambiguity is a pair of stable states S = (Sp,Sq) and S' = (Sp,Sq) ' ' such that either

= T(T(S,~),T')

Definition: A Stable State Pair (sD,s q) is a pair derived f r o m ~ o b - a [ ~ t a E e ~ S , C ~ where S = (sp,Sq) and C = (c12,c21) with both c12 and c21 empty. I-- on global states

all the

Definition: A message x at state s is live iff there is a reachable global state <S,C> with S = (si,s~) and s = s i or s = s ~ a n d there exists an <S',C4> such that <S,C> I <S',C'> where S' = (Sk,S £) and if s = s i, then T(s ,+x) is specik fled and executable and if s = sj, then T(s£,+x) is specified and executable.

A Global State is a pair <S,C> (st's2) with sl e I and s 2 e S 2 the current s t a t e s S o f process PI = (c12,c21) representing the curof channels C12 and C21.

A binary relation as follows:

execution rule applied, <S',C'> are equal to

Definition: A transition at state s for event is executable iff there exists a reachable global state < ( s i , s j ) , ( c i j , c j i ) > with s = s i or = s., and if o Is a recelve t r a n s i t i o n +xi hen ~or s = si, c~= = xY and for s = s , c ~ = xZ, with Y and Z being arbitrary. 3 J~

Definition: A C h a n n e l Cij is a FIFO queue connecting process i to process j. The contents of C i j is labeled cij, it is a string of symbols from M.~ 13 and represents the FIFO queue of mes sages being sent from process i to process j. Each entry in cij is an element of Mij. Definition: where S = representing and P2 and C rent contents

and c[j = cij

Definition: A transition at state s event o is s=pecified iff T(s,~) is defined.

Definition: An extended transition function T(s,T) is defined for a state s E S i and a sequence of events T by the following equation: T(s,T)

s i = x(si,l)

Definition: A global state <S,C> is said to be reachable from an initial state <So,Co> iff <So,Co> J-* <S,C> where <So,Co> = <(Ol,O2), (A,A)> t and I-- * denotes the reflexive, transitive closure of I--.

a null or internal event is denoted by I and % is an element of Z.. 1

iv.

• x

s! = T(sj, +x) and cij = x • c~ ] 19

Except for the one other elements of elements of <S,C>.

Z = {Z.,Z_}, two finite sets of events on M of t~e ~ollowing kind: (I)

s!1 = ~(si' -x) and c~13 = cij

1.

Sp = Sp' and Sq ~ Sq' or

2.

Sp ~ S~ and Sq = s~

A state ambiguity

is a p o t e n t i a l design error.

is defined

Definition: A global state <S,C> I-- <S',C'> iff there exists i,j and cij satisfying one of the following execution rules:

SHere we use A to represent the null symbols, which intuitively represents queue.

168

string of the empty

Definition: A finite state protocol is said to be logicall~ correct w.r.t, unspecified receptions, nonexecutable interactions and state deadlocks if and only if it is free from these errors.

partition ~' of graph g by forming the union of subgraphs of partition z such that the resulting subgraphs satisfy the structured requirements state above. The algorithm for constructing structured partitions can be found in [16].

Various techniques have been applied for the validation of finite state protocols [8,9]. The most common one being teachability analysis. Let the finite state machines for process PI and P2 be represented by the finite state graphs ~ and g2 respectively. Then the protocol graph PG(gl,g2) denotes the protocol between process PI and process P2" The teachability tree RT (gl,g2) for the protocol graph PG(gl,g 2) can be constructed by successively generating reachable global states from the initial global state.

In the following, we will refer to a graph g or subgraph G i by its nodes {v.}. By that we 1 mean the graph or induced subgraph whlch includes all the nodes {vi}. Example 3.1 Consider the graph structure g for the call control phase of Recommendation X.21 as shown in Fig. 3.1 [10]. We have omitted state 13 since the final transition can occur as soon as state 12 (READY FOR DATA) is reached and is not considered to be part of the call establishment procedure. Recommendation X.21 provides many options which network implementors can choose from. We have chosen the option to include all the states thus omitting all bypassing links in the state diagram. In that case, the graph structure g = (I, 2, 3, 4, 5, 6A, 6B, 7/10, 8, 9, 10his, 11, 12, 15). The smallest structured partition ~(0) = {GI, G2, G3, G4, G5, G6A, G6B, G7/10, GS, G9, G10bis, G11, G12, G15}, where G I

Definition: A finite state protocol is balanced if and only if the finite state graphs gl and g2 representing process PI and P2 respectively are isomorphic.

III.

"~us S T R U C T U R E D PARTITION A PROT(~OLGRAPH

OF

Let g be the finite state graph representing process P. For the purpose of protocol decomposition, we define a Structural Partition n of graph g into subgraphs as follows:

=

each subgraph G i contains a unique header node h and zero or more exit nodes e.

ii.

any node v i belonging to subgraph G i can be connected to any other node belonging to the same subgraph.

iii.

iv.

only the exit node e be connected to the graphs and any such the header node h of a header node e.

node

can

IV.

of a subgraph G i can nodes of other subedge is connected to other subgraphs Gj.

also

serve

G2 =

(2),

(? ;)

G3 =

(3),

G4 =

(4),

G5 =

(5),

= )( G6B = (6B), G7/I.0 = (7/10), G 8 = (8), G 9 , G10bi s = (10bls;, G11 = (11), G12 = (12) and G15 = (15) are single node subgraphs. From the smallest structured partition ~(0), we can optionally construct a larger partition ~' = {G~} by forming subgraph G~ = G I U G 2 U G 8 with th~ rest of the subgraphs remaining the same. Thus G{ = (1,2,8), G~ = (3), G~ = (4), G ~ = (5), G ~ A = (6A), G ~ B = {6B), G~/10 (7/I0), G~ = (9), G{0bi s = (10bis), G~I = ~11), G{2 = (12) and G{5 = (15). This partition will be needed in our later discussion.

Definition: A partition n = {GI,G2,...,G ~} of graph g into subgraphs is a Structured Par£1tion if and only if it satisfies the following conditions: i.

(I),

G,A

A STRIR~TURETHEORYFOR FINITE STATE PROTOCOLS

Consider the protocol between two processes PI and P2 connected by communication channels C12 and C21. Let process PI be represented by the finite state graph ~ which can be partitioned structurally into m subgraphs H I = (GI,...,Gm). Let process P2 be represented by finite state graph g2 which can be partitioned structurally into n subgraphs ~2 = (G|,..., G~). Let subgraphs G I and GI be the initial subgraphs for gl and g2 respectively, where they contain the initial node for each graph. Let G i be the i th successor subgraph to G I in graph gl and G 1 be the ith successor subgraph to GI in graph g2" We say that G I in g2 is the corresponding subgraph to G i in g1" For balanced protocols, the corresponding subgraphs are quite obvious since graphs gl and g2 are identical in structure. In other cases, we are referring to the pair of corresponding subgraphs that are reachable from the initial pair of subgraphs. Let G i U h denote the union of subgraph G i with the header node h of its successor subgraph

as an exit

In the event that a node acts as both header and exit nodes, the same rules apply. The minimal subgraph is a single node, in which case the single node acts as both a header and exit node. The structured partition z of a graph g is not unique. The set of all structured partitions SP = {~ .} of graph g forms a partially ordered set. ~he largest structured partition z(1) of graph g is one that has a single block that includes the entire graph g. The smallest structured partition 7(0) of graph g is one in which there are as many blocks as there are nodes which means that every node v i of graph g is a subgraph. From a smaller partition ~ of the graph g, we can construct a larger

169

Gj. Consider an arbitrary subgraph G i U h of 91' and its successor subgraph G~. Its correJ sponding counterparts in 92 are subgraphs G i U h' and G~. See Fig. 4.1. Between subgraphs G i U G.j an~ G!i U G!, there are four regions of interaction. See ~ a b l e 4.1. We can distinguish b e t w e e n two kinds of interactions.

4.1

~£ons

~

of Interactlon ~egion 1

region

2

re~ion 3

region

2.

Cross

4

Regim~

of XmteEactioa

Process P!

Process P2

Gi U h

G[ U h '

~

G~

Gi U h

G~

Gj

G~ U h'

Interactions

In regions 3 and 4, while process P! is in subgraph G i U h or Gj, process P2 is in its c o r r e s p o n d i n g successor or predecessor subgraph, namely, G 3 or G 1 U h' respectively. This can happen as a result of one process racing ahead into its successor subgraph w h i l e the other process lags behind. By itself, this does not signify that a process in one subgraph will exchange events with another p r o c e s s in its predecessor or successor subgraph. However, if they do so, we refer to this as a 'cross interaction' between subgraphs. In some instances, either process P! or P2 can race ahead into successor subgraphs of G~. or G! while the other process lags behind in d! U h ~ or G i U h. In those cases, we can -i have 'cross interaction' between processes that are separated by more than one subgraph. Clearly, from the standpoint of a structured approach to protocol analysis and design, these are the interactions we want to avoid. In a well designed protocol, one would expect that whatever events are exchanged between subgraphs G i U h and G 1 U h', they would be c o n f i n e d to those subgraphs, and once process P! or P2 enters subgraph Gj or G~, the other process will follow suit. In the -following, we will state two different propositions under which 'cross interaction' is absent.

Fig. 3.1 The graph structureg for the call control phase of x.21 with state 13 omitted

Process P1

Process P2

c12

JU

Propo. sition 4.1: If the set of events in protocol graph PG(G i U h, G~ U h') is totally different from the set of events in PG(Gj, G3) , then there can be no 'cross interaction' 5 e t w e e n the two subgraphs.

C21

Fig. 4.1 The ProtocolSubgraphPG(Gi U Gj, G[ U G~)

I.

Expected

The reason for this is obvious. However, the above c o n d i t i o n may not always be the case and we will have to rely upon the following proposition for no cross interaction.

Interactions

In both regions I and 2, while process P! is in subgraph G i U h or G~, process P2 is in its corresponding subgraph G i U h' or G~ respec1 tively. When they exchange events in these subgraphs, we refer to them as the 'expected interactions' between subgraphs.

Prq~osition 4.2: If the protocol given by the protocol graph PG(G i U h, G[ U h') is correct, then all the messages sent by process P! in subgraph ~ h will be received by P2 in subgraph GI _ _ ' U a n d vice versa, i.e. there can be no cross interaction b e t w e e n the two subgraphs.

170

If there are no cross interactions between subgraphs, then the reachability tree of PG(G i U Gj, GII U G~) is the union of the teachability tree of PG(G i U h, GII U h') and the teachability tree of PG (Gj, G~ ) over the global state <(h,h'),(A,A)>-plus a transition region. See Fig. 4.2. The transition region represents intermediate states where one process races ahead into subgraph G. or G_'. while the other 3 G i, U h' or G i U process lags behind in 3 subgraph h. It is generated as a result of connecting subgraph Gj to G i and G ~ to G[. The correctness of the prdtocols given by PG(G i U h, G 1 U h') and PG(Gj, G~) guarantees the correctness of the transiti6n legion. This is because for any sequence of transitions through the transition region, there is an equivalent sequence through the union of the teachability tree of PG(G i U h, G.~ U h') and the reachability tree of PG(Gj, G~). By equivalent sequences, we mean the two sequences have the same set of events except the order in which they occur [11].

the set of successor subgraphs to G I. Let H i = {h k} be t~e set of header nodes of successor subgraphs {G~.} and H' = { h' } be the °set of header n o d e ~ of successor su~graphs {G'~.}. We extend the term 'no cross interaction ~etween subgraphs' to mean that process PI in subgraph G i U H i should not e~change events with process P2 in any subgraph G: . Similarly process P2 in subgraph G 1 U HI should not ~xchange events with process PI in any subgraph G_.. Let PG(G i U H i , G 1 U H I) be the protocol g~aph formed by the union of subgraph G i and G.I' with the set of header nodes H i and s I. See Fig. 4.3. For m successor subgraphs to G i and n successor subgraphs to G I, there are m x n combinations of header state pairs of the form (hx,h ;) . Only a subset of these header state pairs are reachable. The existence of stable header state pairs of the form (hx,h¢) in the reachability tree of PG(G i U Hi, G [ - U HI) means that when process P ~ makes a transition into successor subgraph G';, process P2 can make a similar transition 3into subgraph G 'y. 3 Process ~i

Reachabillty Tree

process P2

(Gi V h, Gi

C12

C21 ~<S.~

TrRe: tion

of PG(Gj, G;)

l

(Region 2)

/

For multiple successor subgraphs the reaGhability tree of PG(G i U G. U .. U G m, G" U G~ i U ,n . . .~. .. U G. ) is the unlon o@ the reac~ablllty ~ree of PG(~ i U H i , GlI U H11) with the teachability trees of Drotocol subgraphs of the form PG(G x, G'.~r) where (Gx, G'.y) is any pair of reachable 3 successor subgr~phs 3 to (G i U H i, GI1 U HI), plus a set of transition regions, see Fig. 4.4.

Fig. 4.2 Reachability Tree of PG(G i U Gj, G~ U G~)

Lemma 4.1 The correctness of the protocols given by the protocol subgraphs PG(G i U b, G[ U h') and PG(G~, G~) implies the correctness of the proJ tocol given by PG(G i U Gj, G[ U G~). We now see that the converse sarily true.

Lemma 4.3 If the protocol given by the protocol graph PG(G i U Hi, G.~ U HI) is correct and for every reachable stable header state pair (hx,h¢) of PG(G~ U H4. G" U H') , the protocol "given x ~y ~ by PG(G., G'. ) is also icorrect, then the protocol given ~ PG(G: U G. U ... U Gin., G' U G~ U 3 ~ 3 • ,. U G 'n . ) iS ~-~--~AU a & ~ ; L~. i 3

is not neces-

Lemma 4.2 The correctness of the protocol the protocol graph PG(G i U Gj, G~ U G~) imply the correctness of th~ protocols the protocol subgraphs PG(G i U h, G[ PG (Gj ,G~).

given does given U h')

by not by or

Again,

the

converse

is

not

necessarily

true. Lemma 4.4

We will now generalize the situation to include multiple successor subgraphs to G i and G~. Let {G~}, k = 1,...,m be~the set of successor s u b g r a ~ s to G i and {G~ }, £ = I .... ,n be

The correctness of the protocol given by the protocol graph PG(G i U G.I U .. U G m , G i, ,I ,n U G U .. U G ) does not impl~ the correctness of ~he protoc~l given by PG(G i U Hi, G~ U H.~)

171

or PG(GX., G! y) where (Gx, G 'y) is any pair of reachable s%ccessor sub'rapes to (G i U Hi, G~ U

Corollary:

HI) Given a protocol graph PG(91,92 ) consisting of n subgraphs, if for each protocol subgraph PG(G i U Hi, G i U Hi), the only stable header state pairs reachable are of the form (hx,h~), then the correctness of the protocols given by the individual subgraphs plus the header nodes of successor subgraph PG(G i U Hi, G i U HI), i = 1,...,n implies the correctness of the entire protocol graph PG(G I U .. U G n , G{ U .. U G~).

<S.C~ - <(hx.hy).(A.A)• <s',c'>- <(h,,h$),(^,^)>

ReachabilityTree

of

PG(Gi U Hi, G[ U H~)

The converse

is not necessarily

true.

Theorem 4.2 tion •

°

°

Given a protocol graph PG(91,92 ) where 91 representing process PI which can be partitioned into m subgraphs ~I ='{GI'''''Gm} and 92 representing process P2 which can be partitioned into n subgraphs ~2 = %G2,...,G~}, the correctness of the protocol ~iven ~ y the*~ntire protocol graph PG(G I U ... U G m, G~ U ... U GA) does not imply the correctness of the protocols given by the protocol subgraphs PG(G k U Hk, G~ U H~) where (Gk U Hk, G~ U G h ) is any pair of subgraphs reachable from initial subgraphs (G I U HI,

•

J G~.

w~ere (hx,h ~) and (hu,h~) ~ e any ~ea=hablestableheaderstatepairs of

PG(G~u Hi, G[ u S~)

G~ u .{)

Finally, we generalize the situation to include the entire protocol graph and arrive at the following theorems.

For balanced protocols, we have the following corollary to Theorem 4.2

Theorem 4.1 Corollary: Given a protocol graph PG(91,92) where 91 representing process PI which can be partitioned •

=

l ~ i : g S ~ : ~ S p ~ h i c { h G ~ n

.,.

Given a balanced protocol graph PG(91,92 ) consisting of n subgraphs, the correctness of the protocol given by the entire protocol graph PG(G I U ... U G n, G{ U ... U G~) does not imply the correctness of the protocol given by the individual protocol subgraphs PG(G i U Hi, G 1 u Hi), i = I ..... n.

-

~eG%ar~i~i~e~e~o

n subgraphs ~. = {G~,...,G' }, then the protocol given by the ~rotoc~l grap~ PG(G I U .. U Gm, G{ U .. U G~) is correct if i.

the initial protocol subgraph G{ U H{) is correct, and

PG(G I U HI, V.

ii.

if the protocol given by PG(G u U Hu, G$ U H$) is correct and (hx, h$) is a stable header state pair of PG(G u U H u, G$ U H$), then the protocol given by PG(G x U Hx, G' U H~) must also be correct where G x is {he successor subgraph of G u with header h x and G~ is the successor subgraph of G$ with header h~.

S

~

~

I'IK~DCOL ANALYSIS AND DES I ( ~

Based on the theory discussed in section IV, we have developed a structured approach to protocol analysis and design. This approach provides a systematic method to the analysis and design of finite state protocols based on protocol subgraphs.

For balanced protocols, the processes PI and P2 are represented by identical graph structures. In that case, there is a one-to-one correspondence between the subgraphs of process PI and the subgraphs of process P2" If the protocols are well designed, the processes engaged in the protocol will not enter into different successor subgraphs. This means that for the protocol subgraph PG(G i U Hi, GI U Hi), the only stable header state pairs reachable will be of the form (hx,h~) where (hx,h~) are the header nodes of successor subgraphs to (Gi,GI). Under those circumstances, we have the following corollary to the theorem.

A.

Structural

Protocol

Analysis

In the following, we restrict our analysis procedure to balanced protocols. This ensures that there is a one-to-one correspondence between the subgraphs of 91 and 9 2 . We begin our analysis with the smallest structured partition ~(0) and whenever we detect the possibility for cross interaction between subgraphs, we form a larger partition until that cross interaction is eliminated. If the protocol graph is correct, then we arrive at a partition z in which all the protocol subgraphs are correct and there are no cross interactions between any two proto-

172

col subgraphs. This partition can be the largest structured partition ~(I) which means that we have to analyze the protocol graph as a whole.

tween what are 'definite' protocol errors and what are 'potential' protocol errors. By potential errors, we mean those errors that may vanish as a result of forming larger partitions. This is because partition ~CURR is too fine and as a result we h a v e cross interactions between subgraphs. By definite errors, we mean that they are errors not only for the protocol subgraph PG(G u U H u, G~ U H~), but will also become errors for the entire protocol graph PG(gI,@ 2) as well.

Let PG(@I,@2) be the balanced protocol graph to be analyzed, t h e structured analysis method for PG(gI,~2 ) is given as follows: Step

1=

Let ~ be the current structured • urr partition of the protocol graph PG(@I,@2 ) to be analyzed. Initialize ~ to the smallest structured • CUrE partltzon z(0).

5.1 ~tentl~ and ~ f M i t e ~otocoE ~ z ~ m

2:

Ste~

Algorithm i.

For the protocol graph PG(@I,@2) partitioned according to ~ , construct the protocol tree pTC~/~,T2 ) by converting graphs @I and @2 into trees T I and T 2 respectively using the following algorithms:

Definite Protocol Erroz

Potential Protocol

DeadlOCksT

<(p,q},(A,A)>

<(hx,q),(A,A)>

Onsp~=ified Receptions

<(p,q),(X,Y)>

<(hx,q),(X,Y)>

((p,q},(X,A)>

<(hx,q),(A,¥)>

<(p,q),(A,Y)>

<(p,h~),(X,Y)>

<(bx,q),(X,A)>

<(p,b~),(X,A}>

State

Error

<(p,h~),(A,A)>

5.1

Let the initial subgraph G I of ~ be represented by the root node of t ~ r ~ r e e " T I•

<(p,h~),(A,Y)>

<(bx,h~),(X,Y)> <(hx,h~),(A,Y)>

ii.

Let the immediate successor subgraph G i to G I in graph 91 be represented by the immediate descendants to node G I in the tree T I .

iii.

For each successor subgraph Gi, let the immediate successor subgraph G= to G i in graph @I be represented by th~ immediate descendants to node G i in the tree T I.

iv.

Repeat (iii) until every terminal node of the tree T I is either a duplicate node or a final node.

<(bx,h~),(X,A)>

T<(hx,b~), (A,A)> is r~ard~ u a final global

Step 4

~(G i U Hi, G i U Hi).

If the state deadlocks and unspecified receptions in the teachability tree RT(G u U Hu, G~ U H$) are all definite protocol errors, then record these errors. Record the nonexecutahle interactions and state ambiguities and go to Step 5. If the teachability tree RT(G u U H u, G~ U H$) contains potential protocol errors, then construct a larger partition ~ > ~CU RR by forming the union of su~graphs G u and G v' with its successor subgraphs for which cross interaction is possible and in addition any other subgraph whose inclusion is required by the definition of a structured partition. Let ~NEW be ~CURR and go to Step 2.

Using the same algorithm, we can construct tree T 2 for g r a p h @2" The protocol tree PT(TI,T 2) so constructed is equivalent to the protocol graph PG(@I,@2). Step

state of

Starting with the root node G I and G{ of the protocol tree PT(TI,T2), construct the teachability tree for the protocol subgraph PG(G I U HI, G{ U H{). If the teachability tree RT(G I U H, G{ U H{) contains protocol errors, then go to step 4, else go to step 5.

Step 5

For any protocol subgraph PG(G u U Hu, G~ U H~), if there are state deadlocks or unspecified receptions, then we have to distinguish between 'definite' protocol errors and 'potential' protocol errors. Let p be any node of subgraph G u and q be any node of subgraph G~. Let h~ and h i be the header nodes of any Immediate successor subgraphs G~. and G~ y to G u and G~ respectively. ~et X ~ d Y denote any arbitrary sequences of messages. Table 5.1 makes the distinction be-

173

If the final global states for PG(G u U Hu, G~ U Hi) are of the form <(hx,h~),(A,A)> where h x and h i are the h~ader nodes of successor subgraphs G x and G~ respectively, then the next set of ~rotocol subgraphs we need to examine are of the form PG(G x U Hx, G~ U Hi). For each protocol subgraph PG(Gx U H x, G'y U H'),y construct the reachabili~y tree RT(G x U Hx, G~ U H i) . If it contains protocol errors, then go back to Step 4, else repeat Step 5 until all reachable pairs of subgraphs have been examined.

The structured technique described above simplifies the analysis process by looking only at subtrees RT(G u U H u, G~ U H~) of the entire teachability tree RT(gl,g 2) and omitting transition regions which for our purpose can be viewed as 'redundancies' in the teachability tree. B.

Structured Pzotocol

graphs to G i and G[ chosen using design rule I. We disallow choosing any other stable state pairs of the form (hx,h ~) or (hy,h~) as header state pairs for successor subgraphs to G i and G[.

Design

Step

3:

For every header state pair (hx,h ~) chosen in step 2, construct the protocol subgraph PG(G u U Hu, G i U Hi). Let the subgraphs G u and G~ be the immediate descendants to G I and G{ in trees T I and T 2 respectively.

step

4:

Using design rule I and 2, determine the new header state pairs (hx,h l) for each protocol subgraph PG(G u U H u, G i U H i) with h x e H u and h' e H'. x u

Step

5:

For each header state pair (hx,h~), construct the protocol subgraph PG(G v U H v, G~ U H~). Let the subgraphs G v and G~ be the immediate descendants to G u and G i in tree T I and T 2 respectively. If subgraph G v and G v have appeared in trees T I and T 2 before• i.e. it is a duplicate node, then subgraph G v and G$ are terminal nodes of tree T I and T 2 respectively. If the protocol subgraph PG(G v U Hv, Gj U __H~ is a final subgraph• i.e. ~ = H$ • then subgraph G v and G v are terminal nodes of tree T I and T 2 also. Repeat steps 4 and 5 until every leaf of tree T I and T 2 is a terminal node.

The theory discussed in section IV provides us with a definition for structured protocol design. By structured protocol design, we require the following: i.

ii.

iii.

the entire protocol graph P G ~ I , @ 2 ) is constructed from the union of protocol subgraphs PG(G i U Hi, G[ U HI), i = 1,...,n with each protocol subgraph designed to correspond to some phase of the protocol. there are no cross protocol subgraphs.

interactions

when one process makes a transition into one of its successor subgraphs, the other process will follow suit and make a similar transition into its corresponding subgraph.

The structured protocol design PG(gl,g 2) is given as follows: step

Step

between

I:

2:

approach

for

Construct the initial protocol subgraph PG(G I U H I, G~ U H~) using, for example, the production rules of Zafiropulo [12]. Let subgraphs G I and G{ be the root nodes of trees T I and T 2 to be constructed.

step

To determine which nodes in subgraphs G I U H I and G~ U H{ can act as header nodes h x e H I and h~ ~ H{ for successor subgraphs to G I and G{ respectively, use design rule I.

Finally• PT(TI,T2) col graph cal nodes

convert the protocol tree so constructed to the protoPG(@I,~2) by merging identiin trees T I and T 2.

Using the structured design technique described above• we can construct complicated protocol graphs by connecting together relatively simple protocol subgraphs. This forms the basis for a building block approach to protocol design.

Design Rule I= Let p and p' be any node of subgraph G i U H i and G~ U H~ other than the header nodes h i and h~. Let q and q' represent any nodes of subgraph G i U H i and G~ U H! respectively including p and p'. I~ in the reachability tree of PG(G i U Hi, G[ U H~), there exists a global state of the form <(p,p'), (A,A)> without any accompanying global states of the form <(p,q'),(X or A, Y)> or <(q,p'),(X, Y or A)>, then nodes p and p' can serve as header nodes h x and h~ ! for successor subgraphs G x and G x respectively.

In the following• we will illustrate the above procedures with a practical example, We have chosen to use the call control phase of CCITT Recommendation X.21. Recommendation X.21 has been validated by different authors [13,14]. It is not our intention to revalidate this protocol" but only to demonstrate how the structured approach would apply. We will not examine the issue of time limits and timeouts but only the logical correctness as given by the state diagram. Example 5 . 1

In order to avoid processes from entering into different successor subgraphs, use design rule 2. Desi@n header

6:

The call control phase for circuit switched service is specified by the state diagram Fig. A-2 in Recommendation X.21 [10]. The state diagram can be translated into separate state transition graphs for the DTE and the DCE participating in the protocol. See Fig. 5.1. The

R u l e 2: Let (hx,h ~) be the state pair for successor sub-

174

four main interface circuits are T, C, R, I, [15]. s(t,c) and s(r,i) represent a send event by the DTE and DCE respectively, while r(r,i) and r(t,c) represent a receive event by the DTE and DCE respectively. Let ~I and ~2 be the state transition graphs representing the DTE and DCE respectively. The P G ~ I ,~ 2 ) represents the protocol between the DTE and DCE. In this case, the two graphs 91 and g2 have an identical structure . The smallest structured partition of g is given by ~(0) = {GI, G 2, G 3, G 4, G 5, G6A, G6B, G7/I0, G8, G 9, G10bi s, GII, G12, G15 ~. See Example 3.1. Frcx, the protocol graph PG(~I,g2), we construct the protocol tree PT(TI,T2). Since both trees T I and T 2 have an identical structure, we will c a l l it T. See Fig. 5.2.

~

=(o,om

,)

s(~,on)

fied reception of the form <(s2,s8), ([0,ON], [BEL,OFF])> which is a potential protocol error, we form a larger subgraph G{ = G I U G 2 U G 8. The new partition so formed ~' = ~G~, G~, G~, G~, G~A, G.~B, G~/10, G~, G{0bi s, G{I, U{2, U { ~ xs given in Example 3.1. For the new partztion ~ , we construct a new tree T' of ~ as shown in Fig. 5.4. The protocol tree PT(T{,T~) tells us that the protocol graph PG(gl,g2 ) is correct iif the protocol subgraphs PG(G.~ U ""' i ' G'i O H~), = I, 3, 4, 5, 6A, 6B, 7/10, 9, 10bis, 11, 12, 15 are correct. See Fig. 5.5. For the simple protocol subgraphs of Fig. 5.5, the validation can be done by sight.

)

=(o,oN) =(+,QfT)

$11 ,(RI)

)

I

S (L~3, (AY)

11 ca)

S{÷,O~l

¢ ( sy~ ,o1~1

Fig. 5.3

The Protocol Subgraph PG(G 1 U H I, G~ U H~)

¢(IAS,OS)

I S{I,~)

¢1IA5,aFF)

TIC,OFt)

¢(Ir~,w,~ly} ~ (~'B,OFFI

i

¢11,

s(m.~

I ~(l,crr)

~(L%5,CeT)

s (sTe,~)

s { .T33 ,o1~1

)

s(1,~)

/ Fig. 5°4

For structured protocol design, we will first construct the protocol subgraph PG(G{ U H|, G] U H{) and let G{ and G{ be the root nodes of trees T] and T~ to be constructed. Using rules I and 2 discussed above, we chose (s3,s3), (s9,Sg), and (s15,s15) to be the header state pairs of successor subgraphs to G]. Next we construct protocol subgraphs PG(G~ U Hi, G~ U H~) PG(G~ U H a, G~ U H~), and PG(G{5 U H]5, G{5 U H{5) and let subgraphs G~, G~, and G]5 be the immediate descendents to G] in trees T{ and T~. Following the structured protocol design procedure described above, we build up trees T] and T~. The process terminates when we arrive at subgraphs G~A and G]I which are duplicate nodes and subgraph G{2 which is a final node.

/ Fiqo 5.2

The T~ae T o~ G r ~

The Tree T' of C~aph

g

For structured protocol analysis, we will first examine the protocol subgraph PG(G I U H I, G 1 U HI). See Fig. 5.3. Since the teachability tree of PG(G I U H, G I U H I) contains an unspeci-

175

• s¢o,om

r (o,ou)

c ( m ~ , o l ,T ;

rig. s.s

~

~.~o~

s,~r~.~= ~(~[,

National Bureau of Standards, "Formal DescriptionTechniques for Network Protocols," Report No. ICST-HLNP-80-3, June 1980.

[4]

T. F. Piatkowski, "An Engineering Discipline foe Distributed Protocol Systems," Proc. INWG/NPL Workshop on Protocol Testing, Vol. I, May 1981, pp. 177-215.

[5]

H. Rudin and C. H. West, "Validation of Protocols using State Enumeration: A summary of some exper ience," Proc. INWG/NPL Workshop on Protocol Testing, Vol. I, May 1981, pp. 371-375.

[6]

G. V. Bochmann, "Finite State Description of Communication Protocols," Computer Networks, Vol. 2, Oct. 1978, pp. 361-372.

[7]

D. Brand and P. Zafiropulo, "On Communicating Finite State Machines," IBM Research Report RZ 1053, Jan. 1981.

[8]

C. H. West, "General Techniques for Communication Protocol Validation," IBM J. Res. Develop., Vol. 11, No. 4, July 1978, pp. 393-404.

[9]

H. Rudin, et. al., "Automated Protocol Validation: One chain of development," Computer Networks, Vol. 2, No. 4/5, 1978, pp. 373-380.

a[, 4;...~)

Finally, convert the protocol tree PT(T~,T~) to the protocol•graph PG(@I,g2). The protocol so constructed is a structured protocol since it satisfies the three requirements stated above. VI.

[3] s (~,orr)

CK~ICLUS IOHS

[10]

CCITT Recommendation Switzerland, 1980.

[11]

J. Ruhin and C. H. West, "An Improved Protocol Validation Technique," Computer Networks, Vol. 6, 1982, pp. 65-73.

[12]

P. Zafiropulo, et. al., "Towards Analyzing and Synthesizing Protocols," IEEE Trans. on Communications, Vol. COM-28, No. 4, April 1980, pp. 651-661.

[13]

The extension of the structure theory to protocols involving more than two processes can be done in a straightforward manner. In the limited space available, we have presented a summary of our work. A complete account is given in [16].

C. H. West and P. Zafiropulo, "Automated Validation of a Communications Protocol: the CCITT X.21 Recommendation," IBM J. Res. Develop., Vol. 22, No. I, Jan. 1978, pp. 60-71.

[14]

R. Razouk and G. Estrin, "Validation of the X.21 Interface Specification Using SARA," Proceedings of the NBS Trends and Applications Symposium, May 29, 1980.

wJ~J~mgCES

[15]

H. C. Folts, "Procedures for Circuit Switched Service in Synchronous Public Data Networks," IEEE Trans. on Communications, Vol. COM-28, No. 4, April 1980, pp. 489-496.

[16]

T. Y. Choi, "A Structured Approach to the Analysis and Design of Finite State Protocols," Ph.D. Thesis, School of Electrical Engineering, Georgia Institute of Technology, 1983 (in preparation).

In this paper, we introduced a 'Structured Partition' of a finite state graph into subgraphs and described the properties of such a partition. Based on the structured partition, we presented a structure theory for finite state protocols. We developed a structured approach to protocol analysis and design based on subgraphs. We applied the technique to the analysis of the call control phase of CCITT Recommendation X.21 and verified its correctness. We also found that the call control phase of Recommendation X.21 conforms with our requirements for structured protocol design.

[I]

A. S. Tanenbaum, "Network Protocols," Computing Survey, Vol. 13, No. 4, Dec. 1981, pp. 453-489.

[2]

C. A. Sunshine, "Formal Modeling of Communication Protocols," University of Southern California, ISI RR-81-89, March 5, 1981.

176

X.21,

Geneva,