Open Collections

UBC Theses and Dissertations

UBC Theses Logo

UBC Theses and Dissertations

Implementation of a protocol validation and synthesis system Tong, Darren Pong-Choi 1985

Your browser doesn't seem to have a PDF viewer, please download the PDF to view this item.

Item Metadata

Download

Media
831-UBC_1985_A6_7 T66.pdf [ 2.14MB ]
Metadata
JSON: 831-1.0051871.json
JSON-LD: 831-1.0051871-ld.json
RDF/XML (Pretty): 831-1.0051871-rdf.xml
RDF/JSON: 831-1.0051871-rdf.json
Turtle: 831-1.0051871-turtle.txt
N-Triples: 831-1.0051871-rdf-ntriples.txt
Original Record: 831-1.0051871-source.json
Full Text
831-1.0051871-fulltext.txt
Citation
831-1.0051871.ris

Full Text

f fi IMPLEMENTATION OF A PROTOCOL VALIDATION AND SYNTHESIS SYSTEM • By DARREN PONG-CHOI T O N G B. Comp. Sci., University of Windsor, 1983 A THESIS SUBMITTED IN PARTIAL FULFILLMENT OF T H E REQUIREMENTS FOR T H E DEGREE OF MASTER OF SCIENCE in T H E F A C U L T Y OF GRADUATE STUDIES (Department of Computer Science) We accept this thesis as conforming to the required standard T H E UNIVERSITY OF BRITISH COLUMBIA May 1985 © Darren Pong-Choi Tong, 1985 In p r e s e n t i n g t h i s t h e s i s i n p a r t i a l f u l f i l m e n t of the requirements f o r an advanced degree at the U n i v e r s i t y o f B r i t i s h Columbia, I agree t h a t the L i b r a r y s h a l l make i t f r e e l y a v a i l a b l e f o r r e f e r e n c e and study. I f u r t h e r agree t h a t p e r m i s s i o n f o r e x t e n s i v e copying o f t h i s t h e s i s f o r s c h o l a r l y purposes may be granted by the head of my department or by h i s o r her r e p r e s e n t a t i v e s . I t i s understood t h a t copying or p u b l i c a t i o n of t h i s t h e s i s f o r f i n a n c i a l g a i n s h a l l not be allowed without my w r i t t e n p e r m i s s i o n . Department of COMPUTZ-K sci&f\jc£ The U n i v e r s i t y of B r i t i s h Columbia 1956 Main Mall Vancouver, Canada V6T 1Y3 >E-6 (3/81) ii Abstract VALISYN, an automated system for the validation and synthesis of error-free protocols has been implemented in C language. It assists designers in the detection and prevention of various kinds of potential design errors, such as state deadlocks, non-executable interactions, unspecified receptions and state ambiguities. The technique employed is a stepwise application of a set of production rules which guarantee complete reception capability. These rules are implemented in a tracking algorithm, which prevents the formation of non-executable interactions and unspecified receptions, and which monitors the existence of state deadlocks and state ambiguities. The implementation of VALISYN is discussed and a number of protocol validation and synthesis examples are presented to illustrate its use and features. iii Table of Contents ABSTRACT » T A B L E O F F I G U R E S v A C K N O W L E D G E M E N T S v i 1. In t roduct ion 1 1.1. M o t i v a t i o n s and objectives 1 1.2. Thesis out l ine 2 2. P r o t o c o l M o d e l l i n g a n d P o t e n t i a l Design Errors 3 2.1. P r o t o c o l M o d e l l i n g 3 2.2. P o t e n t i a l Des ign E r r o r s 5 3. T h e V A L I S Y N — A l g o r i t h m A n a l y s i s and Implementat ion 8 3.1. P r o d u c t i o n Rules 8 3.2. A p p l y i n g the P r o d u c t i o n Rules 14 3.3. T e r m i n a t i n g the Synthesis Process 18 3.4. S u m m a r y of the A l g o r i t h m 20 3.5. H a n d l i n g of the P o t e n t i a l Design Errors 23 3.6. Features of V A L I S Y N 24 4. P r o t o c o l V a l i d a t i o n / S y n t h e s i s Examples 25 4.1. E x a m p l e 1. A general example 25 4.2. E x a m p l e 2. Synthesis w i t h unbounded channel 32 4.3. E x a m p l e 3. Use of Erase M o d u l e 36 4.4. E x a m p l e 4. Detec t ion of var ious k inds of potent ia l design errors 41 4.5. E x a m p l e 5. Independence of input order sequences 44 5. Conclus ions 47 5.1. Thesis s u m m a r y 47 5.2. F u t u r e w o r k B i b l i o g r a p h y V Table of Figures Figure 1. Simple access authorization protocol [ZWRC80] 4 Figure 2. Example contains various Potential Design Errors 6 Figure 3. Derivation of production Rule 1 [ZWRC80] 9 Figure 4. Derivation of production Rule 2 [ZWRC80] 11 Figure 5. Derivation of production Rule 3 [ZWRC80] 13 Figure 6. A synthesis design example 15 Figure 7. Flooring of the tree structure 18 Figure 8. Example with unbounded channels 19 Figure 9. Another example with unbounded channels 20 Figure 10. Removal of arc -3 from Figure 6 23 Figure 11. Example with unbounded channel (index not shown) 35 Figure 12. Resulting diagram by connecting the arcs 41 vi Acknowledgements I would like to thank Dr. Son Vuong for his ideas and guidance, as well as for carefully reading this thesis. I am also grateful to Dr. Sam Chanson for reading and commenting on the drafts. Finally, I would also like to acknowledge Mr. H.Y. Wang for his contribution to designing some of the structures. 1 Chapter 1 Introduction 1 . 1 . Motivations and objectives W i t h t h e g r o w i n g t r e n d t o w a r d s i n c r e a s e d r e l i a b i l i t y o f c o m p u t e r n e t w o r k s c a p a b l e o f p e r f o r m i n g m o r e s o p h i s t i c a t e d f u n c t i o n s , c o m m u n i c a t i o n p r o t o c o l s h a v e g r o w n e n o r m o u s l y i n c o m p l e x i t y [ Z W R C 8 0 , G o u d 8 4 | . A s a r e s u l t , c o m p u t e r -a u t o m a t e d t o o l s f o r p r o t o c o l v a l i d a t i o n a n d s y n t h e s i s a r e i n g r e a t d e m a n d . C o l l e c t i v e l y , five t y p e s o f f o r m a l f r a m e w o r k s f o r m o d e l l i n g c o m m u n i c a t i o n p r o t o c o l s a r e a v a i l a b l e [ G o u d 8 4 ] . T h e y a r e t h e Finite State Machines [ G o S h 8 3 , H o U 1 7 9 ] , Petri Nets ( o r v e c t o r A d d i t i o n S y s t e m s ) [ B e T e 8 2 , K a M i 6 9 , P e t e 8 1 ] , Communicating Finite State Machines [ B o c h 7 8 , Z a f i 7 8 , B o S u 8 0 , B r Z a 8 3 , G M Y u 8 3 ] , Extended Communicating Finite State Machines [ B o c b . 8 0 , B o c h 8 2 ) , a n d Parallel Programs [ S u n s 8 1 ] . T h e C o m m u n i c a t i n g F i n i t e S t a t e M a c h i n e s m o d e l h a s s u c c e s s f u l l y m o d e l l e d s o m e p r a c t i c a l p r o t o c o l s , s u c h as t h e A l t e r n a t i n g - b i t p r o t o c o l [ B o c h 7 8 , G M Y u 8 3 ] , t h e B i n a r y S y n c h r o n o u s p r o t o c o l [ C G L a 8 3 ] , a n d o t h e r s [ G o u d 8 4 ] . W e i m p l e m e n t e d a t o o l , V A L I S Y N ( V A L I d a t o r - S Y N t h e s i z e r ) , u s i n g t h e C o m m u n i c a t i n g F i n i t e S t a t e M a c h i n e s m o d e l a n d t h e t e c h n i q u e d e v e l o p e d b y Z a f i r o p u l o e t a l . [ Z W R C 8 0 ] , w h i c h a l l o w s t h e u s e r s t o d o p r o t o c o l s y n t h e s i s i n a n 2 interactive manner. In addition, it can also be used for protocol validation. In the latter application, the user can make a comparison between the protocol specification of the original copy and the error-free copy generated by the synthesis procedure. 1.2. Thesis outline In this thesis, protocol validation and synthesis via resynthesis is discussed. This technique has been used to validate the X.75 Packet Level protocol [VuCo83b]. Before protocol validation and/or synthesis analysis can be done, a model must be set up. Chapter 2 will introduce the model employed and the existence of various kinds of potential design errors. Chapter 3 presents the algorithm and the implementation of V A L I S Y N . The various features and usage of V A L I S Y N are demonstrated by a number of examples described in Chapter 4. Finally, Chapter 5 concludes the thesis and outlines possible extensions that can be added to V A L I S Y N . 3 Chapter 2 Protocol Modelling and Potential Design Errors In this chapter , we discuss the model a n d some potent ia l errors t h a t m a y arise i n designing a pro toco l . 2.1. P r o t o c o l M o d e l l i n g T h e C o m m u n i c a t i n g F i n i t e State M a c h i n e s ( C F S M ) M o d e l , used by B o c h m a n n [Boch78], is employed to represent the interact ions between t w o C F S M s and the protocol itself. In th is model t w o C o m m u n i c a t i n g F i n i t e State M a c h i n e s are used to model a network , f r o m w h i c h messages are exchanged v i a t w o uni -d i rec t iona l channels. F igure 1 shows a s imple example using this model [ Z W R C 8 0 ] . In the figure, i t can be seen that process A and process B start at the i r i n i t i a l states 0. E a c h message or event is represented by a directed arc or edge w i t h a labe l : negative for event t ransmiss ion and posit ive for event recept ion . F o r example , process A t ransmi ts the message A C C E S S R E Q U E S T to process B , w h i c h is represented by integer - 1 ; whi le process B receives the message A C C E S S R E Q U E S T , w h i c h is represented by +1. E a c h directed arc connects t w o states. T h e one that occurs before the event traversal is ca l led the departure state; the other one that is reached after the event traversal is the entry state. In F i g u r e 1, state 1 (departure state) of process B A REQUESTING PROCESS a AUTHORIZING PROCESS F i g u r e 1. S i m p l e a c c e s s a u t h o r i z a t i o n p r o t o c o l [ Z W R C 8 0 ] . t r a n s m i t s t h e m e s s a g e - 2 ( R E F U S E D A C C E S S ) a n d e n t e r s s t a t e 0 ( e n t r y s t a t e ) . T h e s t a t e p a i r ( 0 , 0 ) i s s a i d t o b e a p a i r o f stable states. A s t a b l e s t a t e p a i r o c c u r s w h e n e v e r t h e c h a n n e l s b e t w e e n t h e t w o p r o c e s s e s a r e e m p t y . T h u s (1, 1) a n d ( 2 , 2 ) a r e o t h e r e x a m p l e s o f s t a b l e s t a t e p a i r s . T h e C F S M m o d e l is e s t a b l i s h e d w i t h t h e f o l l o w i n g a s s u m p t i o n s : (1) E a c h p r o c e s s w i l l b e i n i t i a l i z e d c o r r e c t l y ( i . e . t o i t s z e r o o r r e s e t s t a t e s ) p r i o r t o t h e s t a r t o f a n y i n t e r a c t i o n . (2) T h e c h a n n e l s a r e p e r f e c t . T h i s m e a n s t h e r e w i l l b e n o l o s s o r d i s t o r t i o n o f m e s s a g e s . If a p r o c e s s t r a n s m i t s a m e s s a g e , t h e n t h e o t h e r p r o c e s s w i l l r e c e i v e i t . 5 (3) T h e channels are F i r s t _ I n _ F i r s t _ O u t ( F I F O ) . If process A sends message 1 fo l lowed by message 2, then process B w i l l receive message 1 before i t receives message 2. (4) T h e r e is no t ime constra ints such as t ransmiss ion a n d / o r response delays . O n e advantage of e m p l o y i n g this model is that i t has an expressive power equivalent to that of T u r i n g machines , thus a l l protocols c a n be model led i n th is w a y [Goud84]. 2.2. Potential Design Errors W i t h the above assumptions made for the C F S M model , four k i n d s of potent ia l design errors can be detected, namely , state deadlocks, unspecified receptions, non-executable interactions a n d state ambiguities. F i g u r e 2 shows a n example w i t h these four k i n d s of potent ia l design errors. 1) State Deadlocks W h e n the states of a stable pair have no alternatives other t h a n r e m a i n i n g indefinitely i n the i r current states, a state deadlock occurs. In other words , each state of the stable state pa i r does not have any transmiss ion arc. F o r example , this occurs w h e n process A t ransmits a -1 and at the same t ime process B t ransmits a - 3 . A s a result b o t h process A and process B enter state 2. T h e stable state p a i r (2, 2) w i l l remain indefinitely in these states, because the channels are e m p t y a n d neither states have a t ransmiss ion arc . 6 PROCESS A PROCESS B + 3 -2 H + 1 +2 + 2 +2 1+1 F i g u r e 2 . E x a m p l e c o n t a i n s v a r i o u s P o t e n t i a l D e s i g n E r r o r s . S t a t e d e a d l o c k s i n g e n e r a l r e p r e s e n t e r r o r s , b u t t h e r e a r e s o m e e x c e p t i o n s . F o r e x a m p l e , a p r o t o c o l m a y b e d e s i g n e d t o t e r m i n a t e i n s t a t e s w i t h n o t r a n s m i s s i o n a r c s w h e n a f u n c t i o n is finished [ Z W R C 8 0 ] . T h i s k i n d o f p o t e n t i a l e r r o r m u s t b e d e t e c t e d . 2) U n s p e c i f i e d R e c e p t i o n s T h e s e o c c u r w h e n f e a s i b l e r e c e p t i o n s a r e n o t s p e c i f i e d ; i n o t h e r w o r d s , p o s i t i v e r e c e p t i o n a r c s t h a t c a n b e t r a v e r s e d a r e m i s s i n g . F o r e x a m p l e i n F i g u r e 2 , i f p r o c e s s B t r a n s m i t s a n a r c - 3 , t h e n s t a t e 0 o f p r o c e s s A s h o u l d b e a b l e t o r e c e i v e t h e r e c e p t i o n a r c + 3 . H o w e v e r , i t i s n o t s p e c i f i e d . U n s p e c i f i e d r e c e p t i o n s a r e h a r m f u l i n p r o t o c o l d e s i g n s . W h e n t h e y h a p p e n , u n k n o w n s t a t e s a r e e n t e r e d a n d t h u s t h e i n t e r a c t i o n s a n d b e h a v i o r c a u s e d b y t h e r e c e p t i o n a r c s a r e u n p r e d i c t a b l e . 7 3) Non-executable Interactions Non-executable interact ions are overspecifications of either t r a n s m i s s i o n arcs or reception arcs. In F i g u r e 2, no interact ion sequences c a n cause state 3 of process B to receive event +2. Hence the reception arc +2 f r o m state 3 to state 1 in process B w i l l be a non-executable interact ion. T o view i t i n another w a y , the reception arc w i l l be executable o n l y if process A can t r a n s m i t t w o - 2 events w i t h o u t a - 1 event i n between. However , this is impossible . Non-executable interact ions m a y be h a r m f u l i n designs, because the designers t h i n k t h a t these arcs w i l l be encountered under n o r m a l in terac t ion operations. 4) State A m b i g u i t i e s State a m b i g u i t y occurs w h e n there are two (or more) pairs of stable states (xu and (x2, y2), such t h a t xx ^ z 2 and yx = y2, or xx = x2 and yx 7^ y2. In F i g u r e 2, as process A t ransmits a - 1 , it enters state 1; whi le i n process B , i t can receive the recept ion arc +1 a n d remain in state 0. T h u s we have the stable state pairs (0, 0) a n d (1, 0), w h i c h produce state a m b i g u i t y . State ambiguit ies may or may not result in errors. H o w e v e r , if the designer's in tent ion is t h a t state 0 of process A w i l l o n l y coexist w i t h state 0 of process B , then it w i l l be a n error . T h e C F S M model , together w i t h an a lgor i thm, w h i c h w i l l be discussed in the next chapter , enable us to detect a l l the above potent ia l design errors. 8 Chapter 3 The V A L I S Y N — Algorithm Analysis and Implementation The technique we employed was developed by Zafiropulo et al. [ZWRC80]. It is made up of two parts: the Three Production Rules and a Tracking Algorithm. Both of these are automated by the data-directed design programming method [CoLu78, CGWL80]. The algorithm, based on the cause-and-effect relationships mentioned in [ZWRC80], which prevents the formation of unspecified receptions and non-executable interactions and notifies the designer in case of state ambiguities or state deadlocks. 3.1. Production Rules The three production rules are used to generate the reception arcs for two interacting processes. They are modified from an earlier incomplete version [Zafi78]. Their necessity and sufficiency are proved in [ZWRC80]. The first production rule considers the case when there is a transmission arc after a reception arc. In Figure 3(a), process P2 transmits the message -e after the reception of message +x. If process Pi transmits the message -z and stops, then its entry state should be able to receive the message -fe . PROCESS P1 PROCESS P2 9 - X +. +x F i g u r e 3 . D e r i v a t i o n o f p r o d u c t i o n R u l e 1 [ Z W R C 8 0 J . 10 However , if after the t ransmiss ion of -x a n d before the recept ion of +e , process P i t ransmi ts -y, then the entry state of -y s h o u l d be able to receive the message +e, w h i c h is m a r k e d as +ey. T h e reception arc has the subscr ipt y to indicate tha t messages -y and - e collide. C o l l i s i o n occurs whenever t w o (or more) messages i n different processes are being t r a n s m i t t e d before neither is received. F igure 3(b) shows the general izat ion of rule 1, w h i c h is s u m m a r i z e d as fo l lows: R u l e 1: If - e is appended to +x t h e n , a) a p p e n d + e to -z ; b) append +e , to every negative arc sequence -a a t tached to -x w i t h o u t pars ing any posit ive arc. Here (a) is for the generation of reception arcs w i t h o u t col l i s ion, whereas (b) is used for those t h a t col l ide. T h e second rule is for the case when we have a message t ransmiss ion fo l lowed by another message t ransmiss ion . In process P 2 of F i g u r e 4(a), we have the t ransmiss ion arc -e a t tached to the transmiss ion arc -x. T h u s i n process P i , after the receiving of message +z , i t should be able to receive the message +e . M o r e o v e r , if i n process P i , i t t ransmits message -y before the reception of any message, then message -y i n process P i w i l l be i n col l is ion w i t h messages -x a n d - e i n process P 2 . Therefore, we have +xy appended to -y, and +ey appended to +xy. If message -z is t r a n s m i t t e d after the reception of +xy but before t h a t of message -e , then message -e w i l l coll ide w i t h messages -y a n d -z i n process P i . (b) F i g u r e 4. D e r i v a t i o n o f p r o d u c t i o n R u l e 2 [ Z W R C 8 0 ] . 12 T h u s +ey , is appended to -z. S i m i l a r l y , if process P I t ransmi ts -z' , then +ezi is appended to i t . F i g u r e 4(b) shows the generalized R u l e 2, w h i c h is s u m m a r i z e d as fol lows: Rule 2: If - e is appended to -x t h e n , a) to every +x a n d + xt append +e a n d -f e, respectively; b) to every negative arc sequence -s' a t tached to +x or +ar,, append tt> a n d +e, ,i respectively. note: - a and -s ' are t ransmiss ion sequences. T h e t h i r d rule is needed when we have a t ransmiss ion arc appended to a subscr ipted reception arc. In F igure 5(a), t ransmiss ion arc - c is appended to reception arc +wt. T h i s means that the messages -w i n P I a n d -x i n P2 col l ide . Therefore process P I is able to receive the message +e o n l y if i t has t r a n s m i t t e d the message -w a n d received +xv. T h e event +e is not subscribed because i t is not i n col l is ion w i t h any arc. However , if P i t r a n s m i t s -y before the reception of +xw , then message -x w i l l coll ide w i t h b o t h -w and -y whi le -c w i l l coll ide w i t h -y o n l y . T h u s we have +xw y appended to the entry state of -y a n d +ey appended to +zWty T h e f o r m a t i o n of arc +ey2 is exact ly the same as that of F igure 4 (a) . T h e generalized R u l e 3 is as fol lows: F i g u r e 5 . D e r i v a t i o n o f p r o d u c t i o n R u l e 3 [ Z W R C 8 0 J . 14 R u l e 3: If - e is appended to +v „ in P 2 , then w i t h i n the tree w i t h root -v i n P I : a) append +e to +u „ and +e, to every + « „ , ; b) to every negative arc sequence - * ' a t tached to +u „ or + « . . „ , append +e ( / or +e , y , respectively. note : 1) -s a n d - * ' represent t ransmiss ion sequences. 2) s tands for an a r b i t r a r y message sequence. 3) p a r t (b) of R u l e 3 uses the same mechanism as t h a t of p a r t (b) i n R u l e 2. 3.2. Applying the Production Rules Due to the fact t h a t the p r o d u c t i o n rules are based on the cause-and-effect re lat ionships, we need two precondit ions for their appl icat ions . F i r s t , each negative arc has t o be uniquely defined w i t h i n a process; second, pr ior to the start of protoco l synthesis, a f ic t i t ious event ( - n , +n events i n F i g u r e 6) m u s t occur . F u r t h e r m o r e , the a lgor i thm requires designer interventions to provide semantic i n f o r m a t i o n , such as the entry state of a recept ion event. T h e state diagrams are represented internal ly as trees. A f t e r the exchange of the f ict i t ious event, the a l g o r i t h m w i l l request for a design ac t ion . T h e designer enters A , 0 — » 1 = - 1 , w h i c h means that there is a t ransmiss ion event f r o m departure state 0 to the entry state 1 i n process A and the event is m a r k e d as - 1 . However , in THOCESS B PROCESS A F i g u r e 6. A s y n t h e s i s d e s i g n e x a m p l e . 16 the tree s tructure of process A , it is shown as 0.0—•1.0=-1.0, a d e c i m a l f rac t ion has been added to each n u m b e r . T h e reason for a d d i n g the f rac t iona l par t is t h a t we can only have one a r r i v a l (entry) arc for each state (node) i n a tree s t ruc ture a n d a state m a y be entered more t h a n once. T h e dec imal f r a c t i o n is needed to ident i fy each state. In general, if state * t ransmits an event - c , the a l g o r i t h m w i l l dupl i ca te -e by at taching -e.i to *.i a n d i t w i l l a p p l y the rules to each arc i n d i v i d u a l l y . Since there is o n l y one copy of state 0 (0.0), so just one arc (-1.0) is created and its ent ry state is 1.0. N o w we have the case where a transmiss ion event (-1.0) fol lows a recept ion event ( + n ) , t h u s rule 1 is appl ied . F r o m rule 1(a), the recept ion arc +1.0 is appended to - n . A t this p o i n t , the designer w i l l be p r o m p t e d for a n entry state, to complete the interac t ion B ,Q-*? — l. A s the designer enters 0, the state 0.1 is created ( w h i c h is the second copy of state 0). T h i s ends the a p p l i c a t i o n of rule 1 since rule 1(b) cannot be appl ied . T h e a l g o r i t h m proceeds to p r o m p t for the next in terac t ion f r o m the designer, A , l - * 2 = - 2 , w h i c h turns into A ,1.0—•2.0=-2.0. T h i s is the case of a t ransmiss ion event (-2.0) f o l l o w i n g another t ransmiss ion event (-1.0), a n d hence rule 2 can be appl ied . T h e a l g o r i t h m forms the reception event B ,0.1—>-?=+2.0 a n d the designer enters 0 for ? to complete the interact ion . T h e 0 is represented as 0.2 i n t e r n a l l y (the t h i r d copy of state 0). A t this point the designer enters the t h i r d t ransmiss ion event B ,0—•l=-3. Since there are three copies of state 0, so three events, B ,0.0—•1.0=-3.0, 17 B , 0 . 1 — 1 . 1 = - 3 . 1 , a n d B ,0 .2—1.2=-3.2 are created. R u l e 2 is a p p l i e d t o the first event (event -3 .0) , w h i c h produces the reception events A , 0 . 0 — l . l = + 3 . 0 , A , 1 .0—2.1=3 .0 ! 0 , a n d A ,2 .0—0.1=3.0! 0 2 0 . T h e last t w o event come f r o m the appl ica t ion of rule 2(b). It is w o r t h y to note that the node 0.0 i n process B has 2 departure arcs, -3 .0 and +1.0, and i t should be possible for the state node 1.0 i n process B to receive reception arc +1, after the t ransmiss ion of -3 .0 . T h i s can be done b y r e a p p l y i n g rule 1 to arc -1 .0 . B u t a s impler m e t h o d called replication is e m p l o y e d . T h e rep l i ca t ion procedure w i l l copy the recept ion tree f rom the departure state of the t ransmiss ion arc to its en t ry state, w i t h o u t pars ing any negative arcs, a n d al l the recept ion arcs are subscr ipted to indicate co l l i s ion . T w o examples are + 1 . 0 3 0 a n d + 2 . 0 3 0 i n process B . O n the other h a n d , the state node 0.1 i n process A should be able to t r a n s m i t the event - 1 . T h e a l g o r i t h m w i l l create the t ransmiss ion event a u t o m a t i c a l l y a n d placed it i n a future event queue. A f t e r a p p l y i n g the rules to arcs -3.1 a n d -3 .2 , the arcs i n the future event queue w i l l be examined. F o r example , w h e n rule 3 is appl ied to the t ransmiss ion event A ,0.2—1.3=—1.2, the reception event B ,0.3—0.5=+1.2 is created. However , the a l g o r i t h m , and not designer intervent ions , a u t o m a t i c a l l y determines the entry state 0.5 because i t is identical to the event 5 , 0 . 0 — 0 . 1 = 1 . 0 . T w o reception events a.6, y and er f* . / , w i t h departure states e.f a n d g.h, are identical if e = g, a = c, i = k and j = 1 [CRZa80] . A l s o the entry state 0.5 is regarded as a dead node, because the subtree obta ined f rom this node w i l l be a d u p l i c a t i o n f r o m another node (the one it is identical to). 1 8 A n o t h e r d e f i n i t i o n , similar, w i l l b e c o n s i d e r e d w h e n e v e r t h e i d e n t i c a l t e s t f a i l s . T w o r e c e p t i o n e v e n t s a.b^.j a n d e . r f t . j , w i t h d e p a r t u r e s t a t e s e . f a n d g . h , a r e similar i f e = g , a — c , a n d i = * k . I f t h e s i m i l a r t e s t a l s o f a i l s , t h e n t h e a l g o r i t h m w i l l r e q u e s t t h e d e s i g n e r t o e n t e r t h i s p i e c e o f s e m a n t i c i n f o r m a t i o n . F i g u r e 6 s h o w s a c o m p l e t e t r e e o f t h e s y n t h e s i s . 3.3. Terminating the Synthesis Process A f t e r t h e first i n t e r a c t i o n f r o m t h e d e s i g n e r , t h e f u t u r e e v e n t q u e u e w i l l a l w a y s c o n t a i n s o m e t r a n s m i s s i o n e v e n t s , w h i c h i m p l i e s t h e t r e e s w i l l g r o w i n d e f i n i t e l y . T h e r e f o r e , s o m e w a y m u s t b e e m p l o y e d t o h a l t t h e e x t r a r e s y n t h e s i s . T h e t e c h n i q u e w e u s e d i s c a l l e d flooring [ Z W R C 8 0 ] , w h i c h c o l l a p s e s t h e t r e e s t r u c t u r e b y r e m o v i n g PROCESS A PROCESS B F i g u r e 7 . F l o o r i n g o f t h e t r e e s t r u c t u r e . 19 t h e d e c i m a l f r a c t i o n s i n a l l t h e a r c s a n d s t a t e n o d e s . F i g u r e 7 s h o w s t h e flooring o f F i g u r e 6. I f t h e n e w flooring r e s u l t i s t h e s a m e a s t h e o l d o n e , t h e n t h e a l g o r i t h m w i l l s t o p t h e r e s y n t h e s i s a n d w i l l r e q u e s t t h e d e s i g n e r t o e n t e r t h e n e x t t r a n s m i s s i o n e v e n t . H o w e v e r , i f t h e t w o floorings a r e d i f f e r e n t , t h e a l g o r i t h m w i l l c o p y t h e t r a n s m i s s i o n a r c s f r o m t h e f u t u r e e v e n t q u e u e t o t h e c u r r e n t e v e n t q u e u e , a n d i t w i l l a p p l y t h e p r o d u c t i o n r u l e s t o t h e s e t r a n s m i s s i o n e v e n t s . N e v e r t h e l e s s , t h i s w o r k s o n l y i f t h e c h a n n e l s b e t w e e n t h e p r o c e s s e s a r e b o u n d e d . T h e p r o o f c a n b e f o u n d i n [ Z W R C 8 0 ] . F o r t h e u n b o u n d e d c h a n n e l s , s e e F i g u r e 8 . P r o c e s s B c a n t r a n s m i t t h e m e s s a g e e v e n t - 3 a f t e r e a c h r e c e p t i o n e v e n t . A s s u m e p r o c e s s B d o e s t h i s , a n d p r o c e s s A c a n t r a n s m i t i n a v e r y h i g h s p e e d s u c h t h a t i t a l w a y s r e c e i v e s m e s s a g e + 3 a t s t a t e 2 . T h a t i s , f o r e v e r y m e s s a g e + 3 r e c e i v e d , i t t r a n s m i t s t w o m e s s a g e s . T h u s t h e c h a n n e l f r o m p r o c e s s A t o p r o c e s s B w i l l g r o w i n d e f i n i t e l y . F i g u r e 9 s h o w s a t r i v i a l e x a m p l e w h i c h c o n t a i n s u n b o u n d e d PROCESS A PROCESS 3 + 3 F i g u r e 8 E x a m p l e w i t h u n b o u n d e d c h a n n e l s . 20 PROCESS A PROCESS 3 9 9 " I F i g u r e 9. A n o t h e r e x a m p l e w i t h u n b o u n d e d c h a n n e l s . c h a n n e l s , e a c h o f p r o c e s s A o r B c a n t r a n s m i t w h e n e v e r i t w a n t s . If t h e i r t r a n s m i t t i n g s p e e d s a r e s u f f i c i e n t l y h i g h , t h e n t h e y c a n e a s i l y f l o o d t h e c h a n n e l s . I n o r d e r t o t e r m i n a t e s y n t h e s e s w i t h u n b o u n d e d c h a n n e l s , a t i m e r i s u s e d . 3.4. S u m m a r y o f t h e A l g o r i t h m T h i s s e c t i o n a t t e m p t s t o d e s c r i b e t h e a l g o r i t h m i n d e t a i l e d [ C R Z a 8 0 ] . 1. S e t u p t h e fictitious t r a n s m i s s i o n e v e n t . 2 . D e t e r m i n e t h e f l o o r o f e a c h t r e e . 3 . I n p u t a n e v e n t t r a n s m i s s i o n p, x — ut = - e w h e r e p is t h e p r o c e s s n u m b e r , x t h e d e p a r t u r e s t a t e , w t h e e n t r y s t a t e a n d - e t h e l a b e l o f t h e t r a n s m i s s i o n a r c . 4. D u p l i c a t e t h e m e s s a g e - e s u c h t h a t - c i i s a p p e n d e d t o s t a t e x.i, a n d p l a c e t h e m i n a n e v e n t q u e u e . 21 5. W h i l e the event queue is not e m p t y , remove the top element a n d m a r k i t as the current arc . 5.1. Determine w h i c h rule (1, 2, or 3) to apply to the current arc . 5.1.1. A p p l y the appropriate rule . 5.1.1.1. Generate reception arcs as long as it is possible to do so. 5.1.1.1.1. F o r each generated arc, determine its entry state y.j and duplicate any negative arcs a t tached to the entry state y. 0 and place i t in a future event queue. T h e entry state of a reception arc m a y be de termined by an ident ical arc, a s imi lar arc, or request ing the designer to specify. 5.2. Repl icate the reception tree at tached to the depar ture state of the current arc. 6. Determine the floor of the trees. 7. If the floor is different f r o m the floor value i n step 2, then 7.1. Replace the event queue by the future event queue a n d m a r k the future event queue e m p t y . Save floor value of the tree. R e t u r n to step 5. 8. Save floor values of the trees. 9. Request the designer for next interact ion event or qu i t . 22 D u r i n g the synthesis process, it is most l ike ly t h a t a designer m a y give a piece of w r o n g semantic i n f o r m a t i o n . Therefore, an Erase M o d u l e is needed to erase errors instead of per forming the whole synthesis process again. Erase M o d u l e [CRZa80] 1. W h i l e there is a t ransmiss ion or one of its duplicates is t o be erased, 1.1. F i n d the t ransmiss ion or the dupl ica te . 1.2. Erase the t ransmiss ion or its dupl icate and the subtree a t tached to the entry state of the t ransmiss ion arc (or dupl icate) . 1.3. F i n d al l receptions corresponding to the t ransmiss ion (or dupl icate) a n d erase each reception a n d al l subtrees at tached to the ir entry state. 2. C h e c k each t ransmiss ion i n b o t h trees to determine if it has any corresponding receptions, if there are no receptions, erase the t ransmiss ion . 3. C h e c k each reception i n b o t h trees to determine if it has any corresponding t ransmiss ion , if there are no transmissions, erase the recept ion. T h e erase module w o u l d remove the subtrees f r o m the error p o i n t , as w e l l as a l l the d u p l i c a t e d transmissions or receptions t h a t w o u l d slow d o w n the synthesis process. F igure 10 shows the resul t ing trees after the r e m o v a l of t ransmiss ion event - 3 i n F i g u r e 6. 2 3 PROCESS A PROCESS 3 -1-0 + 1-0 ® -2-0 +2-0 ® F i g u r e 1 0 . R e m o v a l o f a r e - 3 f r o m F i g u r e 6. 3.5. H a n d l i n g of the P o t e n t i a l Design E r r o r s I n t h e g e n e r a t i o n o f t h e r e q u i r e d r e c e p t i o n a r c s , s i n c e t h e p r o d u c t i o n r u l e s a r e c o m p l e t e [ Z W R C 8 0 ] , s o i t i s n o t p o s s i b l e t o c r e a t e n o n - e x e c u t a b l e i n t e r a c t i o n s a n d u n s p e c i f i e d r e c e p t i o n s . I n a d d i t i o n , e a c h t i m e w h e n w e h a v e t h e e v e n t p a i r s ( - e , - f e ) , (+ey, + ye), o r (+e ...,y + y ...,e)» t h e i r e n t r y s t a t e s ( i , j ) i s a s t a b l e s t a t e p a i r . F o r e a c h s t a b l e s t a t e p a i r , i f t h e a l g o r i t h m c a n n o t find a n y t r a n s m i s s i o n e v e n t d e p a r t i n g f r o m t h e m , i t w i l l r e p o r t s t a t e d e a d l o c k . F u r t h e r m o r e , i f t w o s t a b l e p a i r s ( i , j ) a n d (I , k ) e x i s t , e i t h e r i = 1 o r j = k w i l l i n d i c a t e s t a t e a m b i g u i t y . L a s t l y , t h e a l g o r i t h m i s d e s i g n e d w i t h t h e r e s y n t h e s i s t e c h n i q u e ; t h e final p r o t o c o l d e s i g n i s i n d e p e n d e n t o f t h e o r d e r o f t h e i n p u t t r a n s m i s s i o n e v e n t s . H e n c e w i t h d i f f e r e n t e v e n t s e q u e n c e s , f o r e x a m p l e , ( - 1 , - 2 , - 3 ) a n d ( - 3 , - 1 , -2), t h e d e s i g n e r w o u l d g e t t h e s a m e final r e s u l t . 24 3.8. Features of V A L I S Y N T h e package, V A L I S Y N , is w r i t t e n i n C language a n d runs on V A X * 11/750 under 4.2bsd U N I X * . T w o modes, interact ive and non- interact ive , are avai lable for the v a l i d a t i o n a n d synthesis of c o m m u n i c a t i o n protocols . There is a s imi lar package, w r i t t e n in A P L , adopted f r o m the U n i v e r s i t y of Water loo , C a n a d a , now r u n n i n g on A m d a h l 4 7 0 / V 8 under M T S ( M i c h i g a n T e r m i n a l System). In c o m p a r i n g these two packages, V A L I S Y N is preferable over the other package because of the f o l l o w i n g features: - V A L I S Y N is w r i t t e n i n C language rather t h a n A P L , so i t is more por tab le . - V A L I S Y N has b o t h interact ive and non-interact ive modes, whi le the package w r i t t e n i n A P L can o n l y be used interact ive ly . - A n erase procedure is avai lable i n V A L I S Y N but not i n the other package; this procedure is very he lp fu l i n protocol syntheses. A p p a r e n t l y , V A L I S Y N is slower t h a n the other package by about 3 0 % . However , V A L I S Y N runs on a m i n i c o m p u t e r , V A X 11/750, whi le the other package runs o n a large mainf rame computer , A m d a h l 4 7 0 / V 8 . T h u s the difference i n execution t i m e is not s ignif icant . V A X is a trademark of Digital Equipment Corporation. *UNDC is a trademark of A T & T Bell Laboratories. 25 Chapter 4 Protocol Validation/Synthesis Examples This chapter will illustrate the use of VALISYN by means of examples. The package can be used both interactively or non-interactively. For interactive applications, the package requires the designer to enter semantic information when necessary. An Erase Module is also available to erase errors. In non-interactive applications, the designer initially enters all the transmission and reception arcs of the two state diagrams, then the algorithm will produce the final result and any potential design errors. Examples 1 to 3 demonstrate interactive applications of the package, while the other two illustrate non-interactive usages. 4.1. Example 1. A general example. The following is a sample session to illustrate the use of VALISYN, as well as the kind and meaning of information obtained from it. package Debugging information? [y\nj y Level 2 debugging information? [y\nj y 26 Interactive or Non-interactive? [i\nj Enter transmission event 1,0^1=1 1 0.0 -1.0 1.0 Rule 1 is called 2,0-+ f = 1 enter ? OR h - HELP 0 2 0.0 1.0 0.1 Rule IB is called Replicate is called Display stable pairs? [y\nj y Stable States Process 1 Process 2 0 0 1 1 1 Enter transmission event 1,1^2=2 1 1.0 -2.0 2.0 Rule 2 is called 2, 0-* ? = 2 enter ? OR h - HELP 0 2 0.1 2.0 0.2 Rule 2B is called Replicate is called Display stable pairs? [y\nj y Stable States Process 1 Process 2 0 0 1 1 1 Example 1 continue 27 2 1 Enter transmission event 2,0-* 1=3 2 0.0 -3.0 1.0 Rule 2 is called 1,0-* ? = 3 enter ? OR h - HELP 1 1 0.0 3.0 1.1 Rule 2B is called 1, 1-+ ? = 8(1) enter ? OR h - HELP 2 1 1.0 3.0 2.1 1.0 Rule 2B is called l y 2 - + ? = 3(2) enter ? OR h - HELP 0 1 2.0 3.0 0.1 2.0 1.0 Rule 2B is called Replicate is called 8, 1-+ f = 1(8) enter ? OR h -- HELP 2 2 1.0 1.0 2.0 3.0 Replicate is called 2, 2^ ? = 2(3) enter ? OR h - HELP 3 2 2.0 2.0 3.0 3.0 Replicate is called 2 0.1 -3.1 1.1 1, 1-+ ? = s enter ? OR h - HELP 2 1 1.0 3.1 2.2 Rule IB is called Similar - 1 2.0 3.1 0.2 2.0 Rule IB is called Replicate is called 2, i — ? = 2(3) enter ? OR h - HELP Example 1 continue 28 0 2 1.1 2.0 0.3 3.1 Replicate is called 2 0.2 -3.2 1.2 Rule 1 is called 1,2-+ 9 = 3 enter ? OR h - HELP 0 1 2.0 3.2 0.3 Rule IB is called Replicate is called 1 1.1 -2.1 2.3 Rule 1 is called 2, 1-* ? = 2 enter ? OR h - HELP 0 2 1.0 2.1 0.4 Rule IB is called Replicate is called 1 0.1 -1.1 1.2 Rule 3 is called 2 , 3 ^ 9 = 1 enter ? OR h - HELP 2 2 3.0 1.1 2.1 Rule SB is called Replicate is called 1 0.2 -1.2 1.3 Rule 3 is called Identical - 2 0.3 1.2 0.5 Rule SB is called Replicate is called 2 0.3 -3.3 1.3 Rule 3 is called Identical - 1 0.2 3.3 1.4 Example 1 continue 29 Rule SB is called Similar - 1 1.3 3.3 2.4 1.2 Rule SB is called Replicate is called Similar - 2 1.3 1.2 2.2 S.3 Replicate is called 1 0.3 -1.3 1.5 Rule 1 is called 2, 1-+ ? = 1 enter ? OR h - HELP 2 2 1.2 1.3 2.3 Rule IB is called Replicate is called 2 0.4 -3.4 1.4 Rule 1 is called Identical - 1 2.3 3.4 0.4 Rule IB is called Replicate is called 1 1.2 -2.2 2.5 Rule 2 is called 2, 2-+ ? = 2 enter ? OR h - HELP 3 2 2.1 2.2 3.1 Rule 2B is called Replicate is called 1 1.5 -2.3 2.6 Rule 2 is called Identical - 2 2.3 2.3 3.2 Rule 2B is called Replicate is called Display stable pairs? [y\nj y Example 1 continue 30 Stable States Process 1 Process 2 0 12 8 0 1 1 0 1 1 1 1 1 0 2 1 1 1 1 Enter transmission event end Process 1 has the following transmission arcs 0-+ 1 = 1 1^2 = 2 Process 1 has the following reception arcs 2 -* 0 = 3 0-^1=3 1^2 = 3 Process 1 has the following reception arcs with collision 2 ^ 0 = 3(2) 1-+ 2 = 3(1) Process 2 has the following transmission arcs 0^1=8 Process 2 has the following reception arcs 0-^0 = 1 0-* 0 = 2 1 - + 0 = 2 1-^2 = 1 8 — 2 = 1 2-+ 3 = 2 Process 2 has the following reception arcs with collision 1 -+ 0 = 2(3) 1^2 = 1(3) 2-+ 3 = 2(3) *** PROTOCOL ERROR — Deadlock states (2, 1) (2, 2) (2, 3) Total CPU time : 1 560000 sec. Total System Call: 1 200000 sec. Example 1 continue 31 T h i s example tries to show the details of how the trees are b u i l t . T h e f o l l o w i n g points are w o r t h n o t i n g : - T h e " d e b u g g i n g i n f o r m a t i o n " tells the designer the rule or rep l i ca t ion being appl ied . - T h e " level 2 debugging i n f o r m a t i o n " w i l l p r in t out each arc created. F o r example , (2 1.1 2.0 0.3 3.1) means that i n tree 2, the recept ion arc +2.0 w i t h subscr ipt 3.1, w h i c h departs f r o m state node 1.1 to entry state node 0.3, is created. - T h e t ransmiss ion event is entered as 1,0—•1=1 ra ther t h a n 1,0—•1=-1, because i t is only necessary for the designer to enter the t ransmiss ion arcs, a n d the recept ion arcs w i l l be generated a u t o m a t i c a l l y . - W h e n the a l g o r i t h m requests the designer to enter the ent ry state, e.g. 1, 1 —• ? == 3(1), the "1" i n parentheses is the subscr ipt of the recept ion arc. - T h e stable states is a two-dimens ional m a t r i x , a "1" i n element ( i , j) implies state[row(i)j and state[column(j)| are a pair of stable states. It is useful to show the state ambiguit ies i n the design. - " S i m i l a r " indicates the recept ion arc is s imi lar to another one w i t h i n the tree, and the state is decided automat i ca l ly . - " I d e n t i c a l " indicates the reception arc is ident ica l to another arc, w h i c h means a dead node is f o r m e d . - T h e resul t ing state diagrams for this example can be o b t a i n e d by connect ing a l l the arcs ( w h i c h is the same as F igure 7). 32 4.2. Example 2. Synthesis with unbounded channels. This sample session shows how VALISYN reacts when dealing with unbounded channels. package Debugging information? [y\nj n Level 2 debugging information? [y\n] n Interactive or Non-interactive? [i\nj Enter transmission event 1,0-+0=1 2, 0-+ ? = 1 enter ? OR h - HELP 0 Display stable pairs? [y\n] n Enter transmission event 1,0-^0=2 2, 0 — ? = 2 enter ? OR h - HELP 0 Display stable pairs? [y\nj n Enter transmission event 2,0^0=1 1 , 0 - + ? = 1 enter ? OR h - HELP 0 1,0 ^ ? = 1(1) enter ? OR h - HELP 0 1 , 0 - + ? = 1(2} enter ? OR h - HELP 0 33 Display stable pairs? [y\nj n Enter transmission event 2,0-^0=2 1 , 0 ^ ? = 2 enter ? OR h - HELP 0 lt 0-+ ? = 2(1) enter ? OR h - HELP 0 1,0-* ? = 2(2) enter ? OR h - HELP 0 Total CPU time : 13 90000 sec. Total System Call: 1 460000 sec. *** Warning — the protocol may be unbounded Display stable pairs? [y\nj y Stable States Process 1 Process 2 0 0 1 Flooring of arcs? jy\nj y Process 1 has the following transmission arcs 0-+ 0 = 1 0^0 = 2 Process 1 has the following reception arcs 0-^0 = 1 0-* 0 = 2 Process 1 has the following reception arcs with collision 0 — 0 = 1(1) 0-+ 0 = 1(2) 0-+ 0 = 2(1) 0 — 0 = 2(2) Example 2 continue 34 Process 2 has the following transmission arcs 0-+ 0 = 1 0 — 0 = 2 • Process 2 has the following reception arcs 0-+ 0 = 1 0^0 = 2 Process 2 has the following reception arcs with collision 0-+ 0 = 1(1) 0-+ 0 = 1(2) 0-^0 = 2(1) 0-+ 0 = 2(2) Carry on with the synthesis? [y\nj y Total CPU time : 30 340000 sec. Total System Call : 2 400000 sec. *** Warning — the protocol may be unbounded Display stable pairs? [y\n] V Stable States Process 1 Process 2 0 0 1 Flooring of arcs? [y\nj y Process 1 has the following transmission arcs 0-+ 0 = 1 0-* 0 = 2 Process 1 has the following reception arcs 0^0 = 1 0 — 0 = 2 Process 1 has the following reception arcs with collision 0 — 0 = 1(1) 0^0 = 1(2) 0-^0 = 2(1) E x a m p l e 2 c o n t i n u e 35 0 — 0 = 2(2) Process 2 has the following transmission arcs 0-* 0 = 1 0-* 0 = 2 Process 2 has the following reception arcs 0-^0 = 1 0—• 0 = 2 Process 2 has the following reception arcs with collision 0-+ 0 = 1(1) 0-+ 0 = 1(2) 0^0 = 2(1) 0^0 = 2(2) Carry on with the synthesis? [y\n] n Total CPU time : 36 890000 sec. Total System Call: 2 880000 sec. In Figure 11, each state has two self-transmitting loops, thus the channels can be easily flooded. When the timer fires, the following will occur: - give a warning to the designer for unbounded channels. PROCESS A PROCESS B Figure 11. Example with unbounded channels (index not shown). 36 - output the stable states. - output all the transmission and reception arcs. - ask the designer whether to continue or not. 4.3. Example 3. Use of Erase Module. This sample session illustrate the application of the Erase Module of VALISYN. package Debugging information? [y\n] n Level 2 debugging information? [y\n] n Interactive or Non-interactive? [i\nj Enter transmission event 1,0-^1=1 2,0-* ? = 1 enter ? OR h - HELP 1 Display stable pairs? [y\nj y Stable States Process 1 Process 2 0 1 0 1 1 0 0 1 Enter transmission event 2,1^2=3 37 1, 1 — ? » 5 enfer ? OR h - HELP 2 Display stable pairs? [y\nj y Stable States Process 1 Process 2 0 1 2 0 1 0 0 1 0 1 0 2 0 0 1 Enter transmission event 2,2^3=4 1 , 2 ^ ? = 4 enter ? OR h - HELP 3 Display stable pairs? [xfan] y Stable States Process 1 Process 2 Enter transmission event erase Enter the transmission arc to be ERASED 2,1-+2=3 Do you really want to ERASE the arc? [y\nj y Trans, arc 2, 1 —• 2 = 3 has been removed Display stable pairs? (y\nj y Stable States 0 1 2 3 0 1 2 3 1 0 0 0 0 1 0 0 0 0 1 0 0 0 0 1 E x a m p l e 3 c o n t i n u e 38 Process 1 Process 2 0 1 0 1 0 1 0 1 Flooring of arcs? [y\nj y Process 1 has the following transmission arcs 0-+ 1=1 Process 1 has the following reception arcs Process 1 has the following reception arcs with collision Process 2 has the following transmission arcs Process 2 has the following reception arcs 0 ^ 1 = 1 Process 2 has the following reception arcs with collision Enter transmission event 2,1-+ 2=3 1.1-+ 9 = 3 enter ? OR h - HELP 2 Display stable pairs? [y\nj n Enter transmission event 2,2^3=4 1.2-+ ? = 4 enter ? OR h - HELP 3 Display stable pairs? [y\nj n Enter transmission event 2,1-+0=2 l , l - * ? = 2 enter ? OR h - HELP 0 Example 3 continue 39 Display stable pairs? [y\nj n Enter transmission event 1,3^1=6 2 , 3 ~ * ? = 6 enter ? OR h - HELP 1 Display stable pairs? [y\nj n Enter transmission event 1,2-* 0=5 2 . 2 - + ? = 5 enter ? OR h - HELP 0 2.3-+ ? = 5(4) enter ? OR h - HELP 0 1, 0-+ 9 = 4(5) 0 2 , 0 ^ ? = 1(4) 1 l , l ^ ? = 4(1) enter ? OR h - HELP enter ? OR h - HELP enter ? OR h » HELP Display stable pairs? [y\n] U Stable States Process 1 Process 2 0 12 3 0 1 0 0 0 1 0 1 0 0 2 0 0 1 0 3 0 0 0 1 Enter transmission event end Process 1 has the following transmission arcs Example 3 continue 40 ( 7 — 1 = 1 3 — 1 = 6 Process 1 has the following reception arcs 1 — 0 = 2 1 — 2 = 3 2 — 5 =4 Process 1 has the following reception arcs with collision 0— 0 = 4(5) 1 - 1= 4(1) Process 2 has the following transmission arcs 1 — 0 = 2 1— 2 = 3 2— 3 = 4 Process 2 has the following reception arcs 2— 0 = 5 0 — 1 = 1 3— 1 = 6 Process 2 has the following reception arcs with collision 3— 0 = 5(4) 0- 1=1(4) Total CPU time : 2 140000 sec. Total System Call : 0 980000 sec. Example 3 continue 41 PROCESS A PROCESS B +S Figure 12. Resulting diagram by connecting the arcs. The Erase Module will erase the whole subtree from the error point. This example shows that when transmission event 2 is erased after the input sequence (1, 2, 3), event 3 is also removed. Figure 12 shows the final state diagrams. 4.4 . Example 4 . Detection of various kinds of potential design errors. In the sample session, VALISYN is used as a validator to detect various kinds of potential errors. package Debugging information? [y\n] n Level 2 debugging information? /y jn/ n Interactive or Non-interactive? [i\n] n Have default CPU limit 50 sec. ? [y\nj y 'Class notes, CPSC 530, University of British Columbia, 1985. 42 Format for inputting the arc E.g. Trans, arc -12 3 i.e. from Dept. atate 1 to Entry state 2 with Trana. arc 3 Note — the FIRST Trana. arc in Process 1 will be executed first Recept. arc - 1 23 4 i.e. from Dept. state 1 to Entry state 2 with Recept. arc 3 and collision arc 4 Enter a ZERO for collision arc if no or unknown collision occurs Enter the Trans. Arcs for Process 1 — end with a NULL line 0 1 1 12 2 Enter the Recept. Arcs for Process 1 — end with a NULL line 1 2 3 0 2 0 3 0 Enter the Trans. Arcs for Process 2 — end with a NULL line 0 13 Enter the Recept. Arcs for Process 2 — end with a NULL line 0 0 10 0 0 2 0 10 2 0 1 2 1 0 2 3 2 0 3 2 1 0 3 1 2 0 Stable States Process 1 Process 2 0 12 3 0 1 1 0 1 1 1 0 1 0 2 1 1 1 1 3 0 1 0 0 Process 1 has the following transmission arcs 0— 1=1 1— 2 = 2 Example 4 continue 43 Process 1 has the following reception arcs 2-* 0 = 3 1— 2 = 3 0—3 = 3 Process 1 has the following reception arcs with collision 2-* 0 = 3(2) 1 — 2 = 3(1) Process 2 has the following transmission arcs 0—1=3 Process 2 has the following reception arcs 0 — 0 = 1 0- 0 = 2 1 — 2 = 1 3—2 = 1 2-* 8 = 2 Process 2 has the following reception arcs with collision 1-+ 0 = 2(3) 1 _ 2 = 1(3) 2-* 3 = 2(3) *** Warning — the following specified arcs are not executable 2, 3-* 1 = 2 *** Error — the following Recept. arcs arc not specified 1, o — 3 = 3 *** PROTOCOL ERROR — Deadlock states Total CPU time : 1 80000 sec. Total System Call : 0 630000 sec. In this example , the package is used non- interact ive ly , a n d the t ransmiss ion a n d reception arcs of F igure 2 are entered as i n p u t d a t a . Example 4 continue 44 T h e final o u t p u t indicates that there are non-executable arc, unspecified reception, state deadlock and state ambiguit ies ( from the stable state m a t r i x ) . A l l these serve to i l lustrate the potent ia l design errors described i n C h a p t e r 2. 4.5. Example 5. Independence of input order sequences. W i t h different i n p u t order sequences, V A L I S Y N can produce the same final result . package Debugging information? [y\nj n Level 2 debugging information? [y\nj n Interactive or Non-interactive? [i\nj n Have default CPU limit 50 sec? ly\nj V Format for inputting the arc E.g. Trans, arc -12 3 i.e. from Dept. state 1 to Entry state 2 with Trans, arc 3 Note — the FIRST Trans, arc in Process 1 will be executed first Recept. arc —12 3 4 i.e. from Dept. state 1 to Entry state 2 with Recept. arc 3 and collision arc 4 Enter a ZERO for collision arc if no collision occurs Enter the Trans. Arcs for Process 1 — end with a NULL line Oil 2 05 3 16 4 5 Enter the Recept. Arcs for Process 1 •• end with a NULL line 0 04 0 1140 10 2 0 123 0 2 3 4 0 Enter the Trans. Arcs for Process 2 — end with a NULL line 10 2 123 2 3 4 Enter the Recept. Arcs for Process 2 — end with a NULL line 0 110 2 0 5 0 3 160 3 05 0 Stable States Process 1 Process 2 0 1 2 3 0 1 0 0 0 1 0 1 0 0 2 0 0 1 0 3 0 0 0 1 Process 1 has the following transmission arcs 2— 0 = 5 0— 1 = 1 3— 1 = 6 Process 1 has the following reception arcs 1 _ 0 = 2 1— 2 = 3 2— 3 = 4 Process 1 has the following reception arcs with collision 0— 0 = 4(5) 1 - 1 = 4(1) Process 2 has the following transmission arcs 1 — 0 = 2 E x a m p l e 5 c o n t i n u e 46 1— 2 = 3 2— 3=4 Process 2 has the following reception arcs 2— 0 = 5 0 — 1 = 1 3— 1=6 Process 2 has the following reception arcs with collision 3— 0 = 5(4) 0- 1=1(4) Total CPU time : 1 260000 sec. Total System Call : 0 680000 sec. This last example uses Figure 12 in Example 3 as input. In spite of different input order sequences, (1, 3, 4, 2, 6, 5) in Example 3 and (1, 2, 3, 5, 4, 6) in this example, the final result is the same as that of Example 3. 47 Chapter 5 Conclusions 5 .1. T h e s i s s u m m a r y A package for protocol validation/synthesis has been implemented in C language. The tool performs protocol validation by resynthesizing error-free versions of the given protocols. The algorithm, based on a stepwise application of a set of production rules, is able to detect various kinds of potential design errors, such as state deadlocks, non-executable interactions, unspecified receptions and state ambiguities. However, when the algorithm is applied to protocols with unbounded channels, especially self-loop transmissions, a limitation arises, namely, too many dead nodes are being generated. This limitation can be corrected by altering the design, such as setting a bound on the level of resynthesis, or employing a timer. But both of these can at times prematurely terminate the generation of reception events. This problem becomes more serious when the protocol is large and complex. Some decomposition schemes would be helpful in breaking the large protocol into smaller, more manageable components [VuCo82a]. Despite this limitation, the tool has proven useful in validating and synthesizing various practical protocols, such as X.75 [VuCo83b]. 4 8 5.2. Future work The algorithm can be extended to cope "with non-ideal channels, priority channels, and interactions among N-processes. In addition, it would be desirable to have the ability to save the work and resume it some time later, but this feature may add an excessive amount of space overhead. Finally, it is worth noting that the algorithm applied in VALISYN is essentially equivalent to the reachability analysis method [VuCo82b, VuCo83a|. A similar tool has been developed, called VALIRA, which can handle the same kinds of errors [Hui85]. The VALIRA can handle N-process protocols, non-FIFO and priority channels as well as the FIFO channels. Nevertheless, VALISYN can be used as a synthesis tool and it gives the designers more insight into the errors. Both tools, VALISYN and VALIRA, can be used in a complementary manner. 4 9 Bibliography [BeTe82] G. Berthelot and R. Terrat, "Petri Net Theory for the Correctness of Protocols", IEEE Trans, on Comm., Vol. COM-30, No. 12, December 1982, pp. 2497-2505. [Boch78] G.V. Bochmann, "Finite State Description of Communication Protocols", in Network Protocols Symp., Liege, Belgium, February 1978. [Boch80] G.V. Bochmann, " A General Transition Model for Protocol and Communication Services", IEEE Trans, on Comm., Vol. COM-28, April 1980, pp. 643-650. [Boch82] G.V. Bochmann et al., "Experience with Formal Specifications using an Extended State Transition Model", IEEE Trans, on Comm., Vol. COM-30, No. 12, December 1982, pp. 2506-2513. [BoSu80] G.V. Bochmann and C. Sunshine, "Use of Formal Methods in Communication Protocol Design", IEEE Trans, on Comm., Vol. COM-28, No. 4, April 1980, pp. 624-631. [BrZa83] D. Brand and P. Zahropulo, "On Communicating Finite-State Machines", J. ACM, Vol. 30, No. 2, April 1983, pp. 328-342. [CGLa83] C. Chow, M. Gouda and S. Lam, " A Discipline for Constructing Multi-Phase Communication Protocols", Tech. Rep. TR-233, Department of Computer Sciences, University of Texas at Austin, October 1983. [CGWL80] D.D. Cowan, J.W. Graham, J.W. Welch and C.J.P. Lucena, " A Data-directed Approach to Program Construction", Software Practice and Experience, Vol. 10, May 1980, pp. 355-372. [CoLu78] D.D. Cowan and C.J.P. Lucena, "Some Thoughs on the Construction of Programs—A Data-directed Approach", in Proc. 3rd Jerusalem Conf. Inform. Technoi, Jerusalem, Israel, August 1978. [CRZa80] D.D. Cowan, H. Rudin and Zafiropulo, "The Synthesis of Two-process Interactions and Protocols", Internal Paper, University of Waterloo, 1980. 50 [GMYu83] M. Gouda, E. Manning and Y. Yu, "On the Progress of Communication between Two Finite State Machines", Tech. Rep. No. 200, Department of Computer Sciences, University of Texas at Austin, May 1982, revised August 1983. [Goud84] M. Gouda, "Modelling, Analysis and Synthesis of Protocols using CFSMs", Internal Paper, Department of Computer Sciences, University of Texas at Austin, 1984. [GoSh83] M. Gouda and H. Shen, "Specification, Programming and Verification of CSP-Communication by Channel Observation Sequences", Tech. Rep. TR-227, Department of Computer Sciences, University of Texas at Austin, May 1983. [HoU179] J. Hopcroft and J. Ullman, "Introduction to Automata Theory, Languages, and Computation", Addison-Wesley, Reading, Mass., 1979. [Hui85] D. Hui, "Protocol Validation via Reachability: An Implementation", Master Thesis, Department of Computer Science, University of British Columbia, May 1983. [KaMi69] R. Karp and R. Miller, "Parallel Program Schemata", J. of Computer and System Sciences, Vol. 3, No. 2, 1969, pp. 147-195. [Pete8l] J. Peterson, "Petri Net Theory and the Modelling of Systems", Prentice Hall, Englewood Cliffs, N.J., 1981. [Suns8l] C. Sunshine, "Formal Modelling of Communication Protocols", Research Report 81-89, USC/Inform. Sc. Institute, March 1981. [VuCo82a] S.T. Vuong and D.D. Cowan, " A Decomposition Method for the Validation of Structured Protocols", Proc. INFOCOM Conf., April 1982. [VuCo82b] S.T. Vuong and D.D. Cowan, "Reachability Analysis of Protocols with non-FIFO Channels", Proc. COMPCON Fall 82, September 1982. [VuCo83a] S.T. Vuong and D.D. Cowan, "Reachability Analysis of Protocols with FIFO Channels", Proc. ACM SIGCOMM'83 Symp. on Communications Architecture and Protocols, March 1983, pp. 49-57. [VuCo83b] S.T. Vuong and D.D. Cowan, "Automated Protocol Validation Via Resynthesis: The CCITT X.75 Packet Level Recommendation as an Example", J. of Telecommunication Networks, Vol. 2, No. 2, Summer 1983, pp. 153-176. 51 [Zafi78A] P. Zafiropulo, "Protocol Validation by Duolouge-Matrix Analysis", IEEE Trans, on Comm., Vol. COM-26, No. 8, August 1978, pp. 1187-1194. [Zafi78B] P. Zafiropulo, "Design Rules for Producing Logical Complete Two-process Interactions and Communications Protocols", in Proc. 2nd Int. Conf. Comput. Software and Applications, Chicago, IL., November 1978, pp. 680-685. [ZWRC80] P. Zafiropulo, C H . West, H. Rudin, D.D. Cowan and D. Brand, "Towards Analyzing and Synthesizing Protocols", IEEE Trans, on Comm., Vol. COM-28, No. 4, April 1980, pp. 651-661. 

Cite

Citation Scheme:

        

Citations by CSL (citeproc-js)

Usage Statistics

Share

Embed

Customize your widget with the following options, then copy and paste the code below into the HTML of your page to embed this item in your website.
                        
                            <div id="ubcOpenCollectionsWidgetDisplay">
                            <script id="ubcOpenCollectionsWidget"
                            src="{[{embed.src}]}"
                            data-item="{[{embed.item}]}"
                            data-collection="{[{embed.collection}]}"
                            data-metadata="{[{embed.showMetadata}]}"
                            data-width="{[{embed.width}]}"
                            async >
                            </script>
                            </div>
                        
                    
IIIF logo Our image viewer uses the IIIF 2.0 standard. To load this item in other compatible viewers, use this url:
https://iiif.library.ubc.ca/presentation/dsp.831.1-0051871/manifest

Comment

Related Items