Open Collections

UBC Theses and Dissertations

UBC Theses Logo

UBC Theses and Dissertations

Specification-verification of protocols : the significant event temporal logic technique Tsiknis, George 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 T74_4.pdf [ 4.1MB ]
Metadata
JSON: 831-1.0051887.json
JSON-LD: 831-1.0051887-ld.json
RDF/XML (Pretty): 831-1.0051887-rdf.xml
RDF/JSON: 831-1.0051887-rdf.json
Turtle: 831-1.0051887-turtle.txt
N-Triples: 831-1.0051887-rdf-ntriples.txt
Original Record: 831-1.0051887-source.json
Full Text
831-1.0051887-fulltext.txt
Citation
831-1.0051887.ris

Full Text

SPECIFICATION-VERIFICATION OF PROTOCOLS - THE SIGNIFICANT EVENT TEMPORAL LOGIC TECHNIQUE by \ TSIKNIS GEORGE A THESIS SUBMITTED IN PARTIAL FULFILMENT OF THE REQUIREMENTS FOR THE DEGREE OF MASTER OF SCIENCE i n THE FACULTY OF GRADUATE STUDIES (Department of Computer Science) We accept t h i s t h e s i s as conforming to the r e q u i r e d standard THE UNIVERSITY OF BRITISH COLUMBIA A p r i l 1985 © TSIKNIS GEORGE, 1985 In p r e s e n t i n g t h i s t h e s i s -in 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 THE UNIVERSITY OF BRITISH COLUMBIA, I agree that 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 ref e r e n c e and study. I f u r t h e r agree that p e r m i s s i o n f o r e x t e n s i v e copying of 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 or her r e p r e s e n t a t i v e s . I t i s understood that 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 gain 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 Computer Science) THE UNIVERSITY OF BRITISH COLUMBIA 2075 Wesbrook Place Vancouver, Canada V6T 1W5 Date: A p r i l 1985 ABSTRACT This t h e s i s addresses the problem of p r o t o c o l v e r i f i c a t i o n . We f i r s t present a b r i e f review of the e x i s t i n g s p e c i f i c a t i o n methods f o r communication p r o t o c o l s , with emphasis on the h y b r i d techniques. The a l t e r n a t i n g b i t p r o t o c o l i s s p e c i f i e d i n ISO/FDT, BBN/FST and UNISPEX to provide a comparison between three i n t e r e s t i n g h y b r i d models of p r o t o c o l s p e c i f i c a t i o n . A method f o r a p p l y i n g the unbounded s t a t e Temporal Logi c to v e r i f y a p r o t o c o l s p e c i f i e d i n a h y b r i d technique ( i n p a r t i c u l a r FDT) i s o u t l i n e d . F i n a l l y , a new s p e c i f i c a t i o n and v e r i f i c a t i o n method c a l l e d SETL i s proposed, which i s based on event sequences and temporal l o g i c . To i l l u s t r a t e the method two data t r a n s f e r p r o t o c o l s namely, the stop-wait and a l t e r n a t i n g b i t p r o t o c o l s are s p e c i f i e d i n SETL and v e r i f i e d . We demonstrate that SETL i s a g e n e r a l i z a t i o n of the h y b r i d techniques, i t i s sound and that i t can be semi-automated. ACKNOWLEDGEMENT Thanks to Dr. S. T. Vuong f o r s u p e r v i s i n g my r e s e a r c h and f o r h i s comments on t h i s t h e s i s . I a l s o thank Dr. K. Abrahamson f o r h i s comments and f o r reading the f i n a l d r a f t . Table of Contents I. INTRODUCTION 1 A. Mot i vat ion 1 B. T h e s i s O u t l i n e 3 I I . SPECIFICATION TECHNIQUES 5 A. SPECIFICATION OF PROTOCOLS 5 B. EXISTING MODELS 7 1. T r a n s i t i o n models 7 2. Programming languages 9 3. Temporal Logic Models 10 4. Hybrid Techniques 11 C. BBN's FORMAL SPECIFICATION TECHNIQUE 12 D. FORMAL DESCRIPTION TECHNIQUE (FDT) 16 E. UNISPEX 20 F. COMPARISON OF THE THREE SPECIFICATION TECHNIQUES 24 I I I . VERIFICATION OF PROTOCOLS SPECIFIED IN FDT USING TEMPORAL LOGIC ^.29 A. THE UNBOUNDED SEQUENCE MODEL ..29 B. VERIFICATION OF AN FDT SPECIFICATION 30 C. A STOP-WAIT PROTOCOL 3 3 1 . The Network . 35 2. The event p r o p e r t i e s 36 D. VERIFICATION OF THE STOP-WAIT PROTOCOL 37 1. Safety 37 2. L i v e n e s s 40 IV. THE SIGNIFICANT EVENT TEMPORAL LOGIC TECHNIQUE 44 A. THE SIGNIFICANT EVENT MODEL (SEM) 44 i v B. SPECIFICATION LANGUAGE 46 C. TEMPORAL LOGIC SYSTEM 49 D. VERIFICATION IN THE SETL TECHNIQUE 50 E. TRANSLATION FROM FDT TO SETL . 51 F. A STOP-WAIT PROTOCOL 52 G. VERIFICATION OF THE STOP-WAIT PROTOCOL 54 1. Sender 54 2. Receiver 59 3. Safety of the System 60 4. Liveness of the System 61 H. THE ALTERNATING BIT PROTOCOL 63 I. VERIFICATION OF THE ALT. BIT PROTOCOL 65 1. E n t i t y S afety • 65 2. System Sa f e t y 67 3. E n t i t y L i v e n e s s 70 4. System L i v e n e s s 73 V. CONCLUSIONS 76 REFERENCES 78 APPENDIX 1 82 APPENDIX 2 .86 APPENDIX 3 89 APPENDIX 4 - 93 APPENDIX 5 , 94 APPENDIX 6 , 96 APPENDIX 7 100 APPENDIX 8 103 v I. INTRODUCTION A. MOTIVATION Over the l a s t ten years the tr e n d in d i s t r i b u t i o n of computation and data, as w e l l as the need of computer communication have been growing d r a m a t i c a l l y . Computers are org a n i z e d i n t o l o c a l , n a t i o n a l or i n t e r n a t i o n a l networks, l i k e ARPAnet,[McQuill77],CSnet [Landw82],Datapac [Clipham76] or CYCLADES [Pousin82]. Communication over these networks i s a c h i e v a b l e v i a a set of formal r u l e s and procedures which are c a l l e d p r o t o c o l s . P r o t o c o l s f o r long haul networks need to be s t a n d a r d i z e d while p r o t o c o l s f o r l o c a l area networks can be v a r i e d . N e v e r t h e l e s s , i n both cases, p r o t o c o l s need to be we l l s p e c i f i e d , r e l i a b l e , and w e l l t e s t e d . Most of the p r o t o c o l s i n h e r i t a great complexity e i t h e r because they have to d e a l with u n r e l i a b l e mediums or because they have to be g e n e r a l i z e d . As a r e s u l t , a n a t u r a l language d e s c r i p t i o n of a p r o t o c o l i s not only a lengthy one, but a l s o an ambiguous one, as i t i s concluded from the e a r l y ISO d e s c r i p t i o n s . Moreover, such d e s c r i p t i o n do not provide any means of v e r i f i c a t i o n or automatic implementation. Consequently, a formal s p e c i f i c a t i o n technique which supports unambiguous s p e c i f i c a t i o n , v e r i f i c a t i o n , and automatic implementation of the p r o t o c o l s i s h i g h l y d e s i r a b l e . 1 2 A great number and v a r i e t y of formal s p e c i f i c a t i o n techniques f o r p r o t o c o l s have been developed over the past ten y e a r s . Although the spectrum of the e x i s t i n g s p e c i f i c a t i o n methods i s very broad, the m a j o r i t y of them f a l l s i n t o one of the four c a t e g o r i e s ' t r a n s i t i o n models,  programming language models, h y b r i d models and temporal  l o g i c models. T r a n s i t i o n models are based on s t a t e t r a n s i t i o n s of f i n i t e machines. They are i d e a l i n e x p r e s s i n g the c o n t r o l a spects of a p r o t o c o l but, poor in the semantic a s p e c t s . G l o b a l ( l i v e n e s s ) p r o p e r t i e s , l i k e freedom of deadlock can e a s i l y be v a l i d a t e d using some e x i s t i n g v a l i d a t i o n systems. T h e i r disadvantages i n c l u d e the s t a t e space exposion r e s u l t i n g from using these models in s p e c i f y i n g complicated p r o t o c o l s , as w e l l as the d i f f i c u l t y i n v a l i d a t i n g i n v a r i a n t s ( s a f e t y p r o p e r t i e s ) of p r o t o c o l s . The programming language models are i d e a l f o r c a p t u r i n g the semantic aspects of a p r o t o c o l but poor i n e x p r e s s i n g the c o n t r o l a s p e c t s . V a l i d a t i o n p r o o f s u s u a l l y use a s s e r t i o n s . They are lengthy, u s u a l l y done by hand and they are e r r o r prone. The h y b r i d modules combine the two p r e v i o u s techniques, as w e l l as t h e i r advantages. Most of the e x i s t i n g h y b r i d techniques are implementation o r i e n t e d ; so, they do not p r o v i d e any sound method f o r v a l i d a t i o n . The methods used i n programming languages can be a p p l i e d here but the p r o o f s become even more com p l i c a t e d because of the l a c k of the 3 language semantics. F i n a l l y , the temporal l o g i c techniques g i v e a sound system f o r proving the l i v e n e s s p r o p e r t i e s but, i n v a r i a n t p r o o f s are not supported. I t i s c l e a r that we need a method which can combine the advantages of a l l the above methods and p r o v i d e a means for easy v a l i d a t i o n of p r o t o c o l s . With t h i s background, we developed the SETL method which combines the h y b r i d and temporal l o g i c techniques. We b e l i e v e that i t p r o v i d e s the means f o r v a l i d a t i o n of the p r o t o c o l s s p e c i f i e d i n i t and moreover, we regard that i t can be semiautomated. B. THESIS OUTLINE The r e s t of t h i s t h e s i s i s d i v i d e d i n t o four c h a p t e r s . Chapter II g i v e s a b r i e f review of the more popular s p e c i f i c a t i o n methods emphasizing the h y b r i d t e c h n i q u e s . The advantages and disadvantages of the methods are a l s o s t a t e d . The same p r o t o c o l namely the a l t e r n a t i n d b i t p r o t o c o l , i s s p e c i f i e d i n three h y b r i d techniques, the ISO/FDT, BBN/FST and UNISPEX in order to show the s i m i l a r i t i e s among them. In chapter I I I , we show how the unbounded s t a t e temporal l o g i c technique can be used f o r v e r i f i c a t i o n of the p r o t o c o l s s p e c i f i e d i n ISO/FDT. A simple data t r a n s f e r p r o t o c o l i s udes as an example. Chapter IV i n t r o d u c e s the SETL s p e c i f i c a t i o n - v e r i f i c a t i o n technique. Two examples, a simple stop-wait p r o t o c o l and the a l t e r n a t i n g b i t p r o t o c o l , are given as examples i n t h i s c h a p t e r . F i n a l l y , chapter V 4 c o n t a i n s the c o n c l u s i o n and f u t u r e p e r s p e c t i v e s of t h i s method. I I . SPECIFICATION TECHNIQUES A. SPECIFICATION OF PROTOCOLS Acc o r d i n g to the ISO Open System A r c h i t e c t u r e Reference Model [IS082], a communication system i s composed of a h i e r a r c h y of p r o t o c o l l a y e r s . A p r o t o c o l at l a y e r N p r o v i d e s a set of s e r v i c e s to i t s user ( l a y e r N+1 p r o t o c o l ) and in i t s t u rn i t uses the s e r v i c e s p r o v i d e d by the adjacent lower l a y e r (N-1 l a y e r p r o t o c o l ) . Moreover, each l a y e r may be composed by many e n t i t i e s i n t e r a c t i n g with each other e i t h e r d i r e c t l y or v i a a t r a n s i t i o n machine (composition of a l l the l a y e r s below i t ) , as i t i s shown on f i g u r e 1. Consequently, a p r o t o c o l s p e c i f i c a t i o n c o n s i s t s o f : a. A s e r v i c e s p e c i f i c a t i o n d e s c r i b i n g the s e r v i c e s t h i s l a y e r p r o v i d e s to the higher one, (provided s e r v i c e s ) , as w e l l as the s e r v i c e s t h i s l a y e r expects to be provided with, by the l a y e r below (used s e r v i c e s ) . T h i s i n c l u d e s the d e f i n i t i o n s of the d i f f e r e n t types and formats of the messages the e n t i t i e s of the p r o t o c o l use i n communicating with the two adjacent l a y e r s . b. A p r o t o c o l s p e c i f i c a t i o n d e s c r i b i n g the i n t e r n a l behaviour of the e n t i t i e s . T h i s i n c l u d e s the data types, as w e l l as the a c t i o n s each e n t i t y takes i n response to i t s i n t e r a c t i o n s with i t s environment. A s p e c i f i c a t i o n i t i s n e i t h e r necessary, nor wise to i n c l u d e a g r e a t deal of d e t a i l s . I t should keep a high l e v e l pf a b s t r a c t i o n i n order to leave c e r t a i n freedom to 5 Provided services Layer N+1 Used services Transmission Machine Layer N Layer f P l Figure 1. Structure of a Protocol Layer ON 7 implementors. A g u i d e l i n e i s : " a s p e c i f i c a t i o n should give only the d e t a i l s necessary f o r the v a l i d a t i o n of the p r o t o c o l " . Having d e s c r i b e d what a s p e c i f i c a t i o n of p r o t o c o l s i s , we now present some s p e c i f i c a t i o n models. B. EXISTING MODELS Most of the e x i s t i n g formal techniques f o r p r o t o c o l s p e c i f i c a t i o n belong to one of the f o l l o w i n g c a t e g o r i e s . 1. TRANSITION MODELS These can be f u r t h e r d i v i d e d i n t o f i n i t e s t a t e machines, formal languages and graph models. a. F i n i t e s t a t e machines T h i s i n c l u d e s the e a r l i e s t models i n which each p r o t o c o l e n t i t y i s d e s c r i b e d by the s t a t e s of a f i n i t e s t a t e machine, while the events are denoted by the set of inputs and outputs of the machine. In some models the whole system i s r e p r e s e n t e d by one machine while i n others each e n t i t y c o n s t i t u t e s a separate machine. E x t e n t i o n s to t h i s o r i g i n a l idea a r e : The Communication F i n i t e S tate Machine (CFSM) presented in [ Z a f i r o p u l o 7 8 ] . Each p r o t o c o l i s d e s c r i b e d by a p a i of graphs with a r c s l a b e l l e d by signed i n t e g e r s r e p r e s e n t i n g the t r a n s m i s s i o n (-) and r e c e p t i o n (+) events. The topology of the two graphs i s s i m i l a r and each i n t e r a c t i o n sequence i s given by p a i r s of paths. 8 The method o f " c o l o q u i e s " presented by LeMoli i n 78. b. Formal languages In t h i s kind of models, the p r o t o c o l s are d e s c r i b e d u s i n g formal grammars, which generate a language whose sentences capture the i n t e r a c t i o n s between the communication e n t i t i e s . So, the alphabet symbols represent the events and the sentences are the l e g a l d i a l o g u e s c r e a t e d by the p r o t o c o l . c. Graph models In t h i s formalism the nodes in the graph r e p r e s e n t s s t a t e s of the e n t i t i e s and messages i n t r a n s i t . The a r c s , the t r a n s i t i o n s , the topology of the graph and the token(s) placement, model the events i n the system. These models are more powerful than f i n i t e s t a t e machines in the sense that they allow the m o d e l l i n g of c e r t a i n p r o t o c o l s with i n f i n i t e number of s t a t e s . In t h i s category belong the P e t r i Nets and the models of extended P e t r i Nets (with s t a t e v a r i a b l e s ) i n t r o d u c e d by Bochmann and K e l l e r . Most of the t r a n s i t i o n models are proven s u i t a b l e f o r h a n d l i n g a c o n t r o l aspects of a p r o t o c o l ( c a l l set up, e t c ) but they are poor i n d e s c r i b i n g the semantic a s p e c t s (window mechanism, e t c . ) . V a l i d a t i o n of the p r o t o c o l s s p e c i f i e d i n one of these formalisms, can be achieved by a p p l y i n g some r e a c h a b i l i t y a n a l y s i s technique or some s t a t e e x p l o r a t i o n techniques with some c o n t r o l on the p o t e n t i a l c o m b i n a t o r i a l 9 e x p l o s i o n on the number of s t a t e s . Some automatic v a l i d a t i o n software t o o l s have already been developed and used l i k e the IBM one u s i n g Z a f i r o p o u l o s ' method and the OGIVE which i s used to v a l i d a t e P e t r i Nets. The v a l i d a t i o n i n these systems i n c l u d e s mainly a v a l i d a t i o n of the g l o b a l l i v e n e s s p r o p e r t i e s of the p r o t o c o l namely, absence of deadlock, absence of s t a r v a t i o n , e t c . Proofs of the s a f e t y p r o p e r t i e s of a system ( i . e . t h a t messages are d e l i v e r e d i n c o r r e c t order e t c ) are not supported. Moreover, these models have l i m i t e d e x p r e s s i v e power and are s u s c e p t i b l e to what i s known as c o m b i n a t o r i a l s t a t e e x p l o s i o n i f the p r o t o c o l i s complicated. 2. PROGRAMMING LANGUAGES In t h i s approach, p r o t o c o l s are d e s c r i b e d as f l o w c h a r t s or programs i n some programming language. Each e n t i t y of the p r o t o c o l i s ~ represented by a separate module. The modules communicate with each other through message p a s s i n g , shared v a r i a b l e s or any other IPC f a c i l i t y . Examples of such techniques i s the SPEX model d e s c r i b e d in [Schwabe8l], the Gooda model i n [Gooda78] and the GYPSY system i n [ D i V i t o 8 2 ] . These methods give means of e x p r e s s i n g any semantic aspect of the p r o t o c o l and data, but they are c o n s i d e r e d poor i n e x p r e s s i n g the c o n t r o l a s p e c t s . The v e r i f i c a t i o n methods used with these techniques i n c l u d e symbolic e x e c u t i o n , i n d u c t i v e a s s e r t i o n techniques and temporal l o g i c . V a l i d a t i o n , i n g e n e r a l , i s more d i f f i c u l t i n these 10 techniques than i n the t r a n s i t i o n ones. 3. TEMPORAL LOGIC MODELS While i n the previous methods (as w e l l as i n h y b r i d t e c h n i q u e s ) , i n f o r m a t i o n about the system i s encoded w i t h i n the s t a t e of the system , these methods encode the in f o r m a t i o n as requirements on the sequence of the system s t a t e s . The s t a t e component of the system simply d e f i n e s whether a given event can occur. The model uses a set of event sequences, ( h i s t o r i e s , and s p e c i f i c a t i o n s are temporal l o g i c formulas i n c l u d i n g a r b i t r a r y p r e d i c a t e s on the event h i s t o r i e s . Consequently, these methods give a very high l e v e l of a b s t r a c t i o n . The Unbounded St a t e Temporal Logic method developed by H a i l p e r n [Hailpern80] i n c l u d e an unbounded h i s t o r y v a r i a b l e f o r each input and output of a module, which records the messages exchanged between the module and i t s environment. Modules are s p e c i f i e d i n terms of p r o p e r t i e s that the h i s t o r y v a r i a b l e s must s a t i s f y . We s h a l l use t h i s method f o r v e r i f i c a t i o n purposes i n Chapter 3. The Event Based Temporal Logic developed by Vogt [Vogt82] uses only one event sequence per system, which records a l l the events occured i n the system. The s p e c i f i c a t i o n of a module c o n s i s t s of temporal l o g i c formulas which d e f i n e the f u t u r e sequence which are c o n s i s t e n t with t h i s module. 11 F i n a l l y , the bounded s t a t e temporal l o g i c i n [Schwartz82] i n c l u d e a s t a t e component which holds the l a s t sent, or r e c e i v e d message. The s p e c i f i c a t i o n of a module i s given by temporal l o g i c formulas which i n c l u d e the s t a t e components as w e l l as the events (some s p e c i a l events l i k e dequeue e t c . are used to d e s c r i b e queue a c t i o n s ) occured i n the module. A l l these methods provide a sound t o o l f o r v a l i d a t i n g l i v e n e s s p r o p e r t i e s of a system using some temporal l o g i c a x iomatic system. Since most of the s p e c i f i e d module p r o p e r t i e s have the form p D <>q (that i s i f event(s) p occur then e v e n t u a l l y event(s) q w i l l o c c u r ) , v a l i d a t i o n of s a f e t y p r o p e r t i e s of a system s p e c i f i e d by them i s very d i f f i c u l t . Some of them r e s o r t to d i f f e r e n t methods ( o u t s i d e temporal l o g i c ) , i i k e Hoare l o g i c , f o r the above purpose. 4. HYBRID TECHNIQUES They are a l s o known as " u n i f i e d " or "extended s t a t e machines" and they i n v o l v e both s t a t e t r a n s i t i o n s and programming language. Such techniques are the FDT d e s c r i b e d i n [IS084], the FST i n [Blumer82]., the PDIL i n [Ansart83] which i s very s i m i l a r to FDT, and the UNISPEX i n [Vuong82], In most h y b r i d s p e c i f i c a t i o n techniques a p r o t o c o l s p e c i f i c a t i o n i s modelled by a system of i n t e r c o n n e c t e d modules ( e n t i t i e s ) , each of which i s an extended f i n i t e s t a t e machine (EFSM). At any time, the s t a t e of the EFSM i s d e s c r i b e d by the value of the "major s t a t e " v a r i a b l e 1 2 together with the values of a l l the l o c a l v a r i a b l e s of the machine. The module accepts c e r t a i n types of i n p u t s (events) from i t s environment. Each input may cause a s t a t e t r a n s i t i o n and an o p e r a t i o n . The o p e r a t i o n i s c o n s i d e r e d as p a r t of the t r a n s i t i o n ; I t may change the v a l u e s of the v a r i a b l e s , and may i n i t i a t e one or more outputs (events) to the environment. The o p e r a t i o n i s assumed to be atomic. The model i s n o n - d e t e r m i n i s t i c in the sense that at any s t a t e and any input i n t e r a c t i o n , many t r a n s i t i o n s may be enabled. The t r a n s i t i o n which w i l l a c t u a l l y occur i n sue case, i s e i t h e r determined by using a " p r i o r i t y " method, or i t i s l e f t to the implementor's d e c i s i o n . In the f o l l o w i n g , we b r i e f l y present three of the e x i s t i n g h y b r i d techniques : the BBN's Formal S p e c i f i c a t i o n Technique (FST), the Formal D e s c r i p t i o n Technique (FDT), anf the UNISPEX. For each one of them, we f i r s t o u t l i n e i t s main f e a t u r e s and then we give the s p e c i f i c a t i o n of the a l t e r n a t i n g b i t p r o t o c o l using the technique. At the end, we compare these three techniques. C. BBN'S FORMAL SPECIFICATION TECHNIQUE T h i s technique was developed by T. Blumer and R. Tenney at BBN i n 1982 and i s presented i n [Blumer82]. The language used by t h i s s p e c i f i c a t i o n technique i s an enhanced P a s c a l language. The P a s c a l language has been augmented to i n c l u d e i n t e r f a c e and s t a t e d e c l a r a t i o n s , a b b r e v i a t i o n s of s t a t e s 1 3 and p r e d i c a t e s , and t r a n s i t i o n d e f i n i t i o n s . A s p e c i f i c a t i o n of a p r o t o c o l c o n s i s t s of a number of e n t i t y type s p e c i f i c a t i o n s ; one f o r each d i f f e r e n t e n t i t y of the p r o t o c o l . Each e n t i t y type s p e c i f i c a t i o n c o n t a i n s the d e c l a r a t i o n s and the t r a n s i t i o n s of the e n t i t y . a. D e c l a r a t i o n s The d e c l a r a t i o n p a r t c o n t a i n s constant and type d e f i n i t i o n s , the i n t e r f a c e s , the s t a t e and p r e d i c a t e a b b r e v i a t i o n s ( i f any) and f i n a l l y , the procedure , f u n c t i o n and p r e d i c a t e d e f i n i t i o n s . I n any e n t i t y s p e c i f i c a t i o n there i s a s p e c i a l type d e f i n e d as machine. T h i s i s a r e c o r d c o n t a i n i n g a l l the l o c a l v a r i a b l e s of each i n s t a n c e of the e n t i t y d e s c r i b e d by t h i s s p e c i f i c a t i o n . The i n t e r f a c e s c o n s t i t u t e the s e r v i c e s p e c i f i c a t i o n of the p r o t o c o l e n t i t y . An i n t e r f a c e p r i m i t i v e has the form i n t e r f a c e [ d i r e c t i o n e n t i t y : SERVICE.type( P1...Pn )] where d i r e c t i o n can be to or from, i n d i c a t i n g that the i n t e r a c t i o n i s i n i t i a t e d by the e n t i t y or i t s environment; e n t i t y i s the l a y e r or peer e n t i t y , the s p e c i f i e d l a y e r i n t e r a c t s with, u s u a l l y , t h i s i s U(user) for the N+1 l a y e r , N(network) f o r the N-1 l a y e r and S(system) f o r the o p e r a t i n g system; SERVICE i s the s e r v i c e p r i m i t i v e p rovided or used by the p r o t o c o l e n t i t y ; type can be request, response,  i n d i c a t i o n , e t c . , i n d i c a t i n g the kind of s e r v i c e s ; and P1,...,Pn are the parameters i n v o l v e d a t . t h e c a l l of t h i s 1 4 s e r v i c e p r i m i t i v e . The s t a t e d e c l a r a t i o n s and a b b r e v i a t i o n s have the form s t a t e i d e n t i f i e r = (<state-id>*) where <>* means one or more occurences. The s t a t e d e c l a r a t i o n should d e f i n e the i n i t i a l and the f i n a l s t a t e of the machine. The p r e d i c a t e , procedure and f u n c t i o n d e c l a r a t i o n s are the same as i n Pascal with the exception that p r e d i c a t e s must not have s i d e e f f e c t s and f u n c t i o n s or procedures which are implementation dependent are d e c l a r e d as p r i m i t i v e . One of the procedures i n i t i a l i z e s the p r o t o c o l machine and i t i s understood to be c a l l e d when the machine needs to be i n i t i a l i z e d . b. T r a n s i t i o n s The t r a n s i t i o n p a r t d e s c r i b e s the s t a t e t r a n s i t i o n s of the p r o t o c o l e n t i t y machine. Each" t r a n s i t i o n i s t r i g g e r e d by an i n t e r f a c e event (which has the same name with an i n t e r f a c e p r i m i t i v e ) and may r e s u l t to a change of the s t a t e of the machine, as w e l l as t o changes of some v a r i a b l e s . Each t r a n s i t i o n has the form <DEST> < ( P r i o r i t y ) <ORIG> [ i n t e r f a c e - p r i m i t i v e ] ( c o n d i t i o n ) begin body end; where ORIG, DEST are the o r i g i n and d e s t i n a t i o n s t a t e ( s ) f o r the t r a n s i t i o n , and p r i o r i t y i s an in t e g e r i n d i c a t i n g the 1 5 r e l a t i v e p r i o r i t y of t h i s t r a n s i t i o n among the t r a n s i t i o n s which can be f i r e d at the same time. The i n e r f a c e p r i m i t i v e i s a "from" type i n t e r f a c e p r i m i t i v e and the c o n d i t i o n i s a boolean e x p r e s s i o n which may c o n t a i n p r e d e f i n e d p r e d i c a t e s . The body of the t r a n s i t i o n c o n t a i n s P a s c a l statements i n v o l v i n g the v a r i a b l e s of the machine. The parameters of the i n t e r f a c e p r i m i t i v e when used i n s i d e the body are denoted by [ D i r e c t i o n - e n t i t y : p a r - i d ] The body may invoke to-type i n t e r f a c e p r i m i t i v e s . In such case the parameter values are denoted as par-id=value i n the parameter l i s t of the p r i m i t i v e . The semantics of a t r a n s i t i o n are : when the p r o t o c o l machine i s at s t a t e ORIG and the i n t e r f a c e p r i m i t i v e event occurs, then i f the c o n d i t i o n i s t r u e , the body of the t r a n s i t i o n i s executed and the machine i s t r a n s f e r e d to the s t a t e DEST. In APPENDIX 1, we show the s p e c i f i c a t i o n of the a l t e r n a t i n g b i t p r o t o c o l (ABP) on a f u l l duplex channel, using t h i s technique. In t h i s s p e c i f i c a t i o n , the corresponding f i n i t e s t a t e machine does not q u i t e resemble the "communicating f i n i t e s t a t e machine"which rep r e s e n t s the same p r o t o c o l . T h i s i s because, many t r a n s i t i o n s have been combined to a s i n g l e one. Moreover, no d i s t i n c t i o n i s made between a r e c e p t i o n of an in-sequence message and an out-of-sequence one, at the t r a n s i t i o n l e v e l . T h i s d i s t i n c t i o n i s r r e a l i z e d by the program segment i n the body 1 6 of a t r a n s i t i o n . The amalgamation of t h i s kind i s p o s s i b l e i n any of the three techniques we present here, and produces a s h o r t e r and c l o s e r to the implementation s p e c i f i c a t i o n , but, i t i s not s u i t a b l e f o r v a l i d a t i o n purposes. In order to apply a v a l i d a t i o n technique ( r e a c h a b i l i t y a n a l y s i s ) , the p r o t o c o l s p e c i f i c a t i o n needs to be t r a n s l a t e d i n t o a communicating f i n i t e s t a t e machine s p e c i f i c a t i o n . If the h y b r i d s p e c i f i c a t i o n employes s t a t e and event amalgamations, such t r a n s l a t i o n i s not an obvious one. For each s p e c i f i c a t i o n , we a l s o give a s t a t e t r a n s i t i o n diagram of the s p e c i f i c a t i o n . In these s t a t e t r a n s i t i o n diagrams each arc is. l a b e l l e d by the i n t e r a c t i o n which t r i g g e r s the t r a n s i t i o n . Using Z a f i r o p o u l o s ' n o t a t i o n a' "-" means t r a n s m i s s i o n and a "+" means r e c e p t i o n of a PDU. The i n t e r a c t i o n s which are part of the o p e r a t i o n of each t r a n s i t i o n , are given i n s i d e the parentheses on each a r c . C l e a r l y , these diagrams can not thoroughly capture the a c t i v i t i e s of the p r o t o c o l machine, but they g i v e some general idea of the s p e c i f i c a t i o n . The s t a t e t r a n s i t i o n diagram of t h i s s p e c i f i c a t i o n i s shown in f i g u r e 2. D. FORMAL DESCRIPTION TECHNIQUE (FDT) I t was developed by G. Bochmann et a l . , the ISO subgroup B of ad hoc group on FDT, i n 1981. The language used by t h i s technique i s again a P a s c a l language augmented with f a c i l i t i e s f o r i n t e r a c t i o n , module and t r a n s i t i o n Figure Z State T r a n s i t i o n Diagram f o r the s p e c i f i c a t i o n . 18 d e f i n i t i o n s . The s p e c i f i c a t i o n of a p r o t o c o l c o n s i s t s of the g l o b a l d e c l a r a t i o n p a r t , the i n t e r a c t i o n s and the module(s) d e f i n i t i o n p a r t . The g l o b a l d e c l a r a t i o n s c o n t a i n c o n s t a n t s , types and v a r i a b l e s which are g l o b a l to a l l modules of the p r o t o c o l and use the same P a s c a l syntax. The other two p a r t s are b r i e f l y d i s c u s s e d now. a. I n t e r a c t i o n s Each i n t e r a c t i o n d e f i n i t i o n d e f i n e s a channel. A channel i s d e f i n e d by g i v i n g a l l the p o s s i b l e i n t e r a c t i o n p r i m i t i v e s , used by t h i s module to communicate with another module. A channel d e f i n i t i o n has the form CHANNEL <channel-id> ( < r o l e - l i s t > ) ; B y < r o l e - l i s t > : < i n t e r a c t i o n - 1 i s t > ) * where < r o l e - l i s t > i s a l i s t of the p a r t i e s use t h i s channel and t h e i r r o l e . I n t e r a c t i o n - l i s t c o n t a i n s one or more i n t e r a c t i o n s of the form < i n t e r a c t i o n - i d > (<parameter-list>); In t h i s technique i n t e r a c t i n g modules are connected by channels but the topology of a system i t i s not s p e c i f i e d by the language. b. The Module D e f i n i t i o n The module d e f i n i t i o n s p e c i f i e s one e n t i t y type. The s p e c i f i c a t i o n of a p r o t o c o l should c o n t a i n one module d e f i n i t i o n f o r each ( d i f f e r e n t type) e n t i t y i n the p r o t o c o l . 19 Each module c o n t a i n s the header, the d e c l a r a t i o n s , the f u n c t i o n and procedure d e f i n i t i o n s , the i n i t i a l i z a t i o n and the t r a n s i t i o n s . The module header has the form MODULE <module-type-id> (<channels>); where <channels> i s a l i s t of <channel> (<ro l e - i d > ) . That i s the module s p e c i f i e s a l l i t s channels through which i t communicates with i t s environment and the r o l e of the module in each channel. The d e c l a r a t i o n s , f u n c t i o n and procedure d e f i n i t i o n s are i n pure P a s c a l syntax and d e f i n e the l o c a l elements used by the module. One of the v a r i a b l e s i s e x p l i c i t l y c a l l e d "STATE" and rep r e s e n t s the "major s t a t e " of the module. The i n i t i a l i z a t i o n s e c t i o n has the form INITIALIZE <begin-statement> where <begin-statement> i s a P a s c a l block c o n t a i n i n g statements which i n i t i a l i z e the l o c a l v a r i a b l e s . The p o s s i b l e t r a n s i t i o n s of the module are d e f i n e d next. Each t r a n s i t i o n i n c l u d e s : a. the e n a b l i n g c o n d i t i o n which i n v o l v e s : the present major s t a t e (FROM c l a u s e ) , the input i n t e r a c t i o n (WHEN c l a u s e ) , the a d d i t i o n a l c o n d i t i o n (PROVIDED c l a u s e ) , and the p r i o r i t y of the t r a n s i t i o n (PRIORITY c l a u s e ) ; b. the o p e r a t i o n of the t r a n s i t i o n which i n c l u d e s : the next major s t a t e (TO c l a u s e ) , and the " a c t i o n " (BEGIN block) which may i n i t i a t e an output i n t e r a c t i o n denoted by <channel - i d > . < i n t e r a c t i o n - i d > ( < p a r a m e t e r - l i s t > ) . 20 In g e n e r a l , a t r a n s i t i o n can be d e f i n e d as : < t r a n s i t i o n > ::= / ANY < i d e n t i f i e r > : <type> DO < t r a n s i t i o n ; * * / WITH <variable> DO < t r a n s i t i o n > * / WHEN <channel~id> . < i n t e r a c t i o n - i d > < t r a n s i t i o n > * / FROM <major-state> < t r a n s i t i o n > * / TO <major-next-state> < t r a n s i t i o n > * / PROVIDED <expression> < t r a n s i t i o n > * / <block> where / d e n o t e s a l t e r n a t i v e s and <major-next-state> can be the word SAME. Now, as an example, we give the FDT s p e c i f i c a t i o n of the same p r o t o c o l ( a l t e r n a t i n g b i t ) , which i s shown i n APPENDIX2. The s t a t e t r a n s i t i o n diagram of t h i s s p e c i f i c a t i o n , i s the same with the pre v i o u s one shown on f i g u r e 2. E. UNISPEX We now o u t l i n e the main f e a t u r e s of the UNISPEX model i n t r o d u c e d by S. Vuong and D. Cowan i n 1982 [Vuong82], In t h i s model each peer e n t i t y type of a p r o t o c o l l a y e r i s rep r e s e n t e d as a P r o t o c o l Machine type. A l a y e r may have many P r o t o c o l Machine types and a number of i n s t a n c e s of each type. Then a l a y e r i s completely s p e c i f i e d by the P r o t o c o l Machine part the topology and the P r o p e r t i e s p a r t . 21 a. P r o t o c o l Machine The P r o t o c o l Machine pa r t c o n s i s t s of three s e c t i o n s : the D e c l a r a t i o n s s e c t i o n , the I n t e r f a c e s and the Event sect i o n . The D e c l a r a t i o n s e c t i o n d e f i n e s the c o n s t a n t s , data types, the v a r i a b l e s used by the p r o t o c o l machine, as we l l as, the i n i t i a l s t a t e of the machine. There are three types of v a r i a b l e s : s t a t e , i n t e r f a c e , channel v a r i a b l e s . The s t a t e v a r i a b l e s c o n t a i n only l o c a l v a r i a b l e s , as w e l l as, some h i s t o r y v a r i a b l e s used i n v e r i f i c a t i o n and i n the p r o p e r t i e s s e c t i o n . One s p e c i a l v a r i a b l e c a l l e d State i n d i c a t e s the d i f f e r e n t major s t a t e s of the machine. The i n t e r f a c e v a r i a b l e s are used i n communication with the adjacent l a y e r s , as w e l l as, with the o p e r a t i n g system, while, the channel v a r i a b l e s are used i n communication between the e n t i t i e s i n the same l a y e r . Consequently, i n t e r f a c e and channel v a r i a b l e s are shared ones. Each one of them has a d i r e c t i o n of flow a s s o c i a t e d with i t , to i n d i c a t e i f data flow _in or out the p r o t o c o l machine. The i n i t i a l s t a t e i s s p e c i f i e d by g i v i n g the i n i t i a l v alues of any v a r i a b l e . The i n t e r f a c e s e c t i o n c o n t a i n s the s e r v i c e p r i m i t i v e s , the p r i m i t i v e s and the mapping events. The s e r v i c e p r i m i t i v e s denote the s e r v i c e s t h i s l a y e r p r o v i d e s to the higher one. A c t i v a t i o n of a s e r v i c e p r i m i t i v e causes some changes i n i n t e r f a c e v a r i a b l e s which trigge'r an event. The p r i m i t i v e s together with the mapping events c o n s t i t u t e the 22 i n t e r f a c e with the lower l e v e l and the system. When a channel v a r i a b l e has changed, i t may t r i g g e r some mapping event which a c t i v a t e s the execution of a p r i m i t i v e . Mapping events are e s s e n t i a l f o r implementation purposes. The event s e c t i o n s p e c i f i e s the events o c c u r i n g as a consequence of the i n t e r a c t i o n s of t h i s machine with other ones. Thus, t h i s s e c t i o n s p e c i f i e s a l l the p o s s i b l e t r a n s i t i o n s t h i s machine can enjoy. An event has the f o l l o w i n g syntax: <event name> / <event code> / <origin> > <destination> when (<enabling predicate;-) [ <effect>] An event can f i r e only when the e n a b l i n g p r e d i c a t e i s true and the machine i s at the s t a t e <origin>. The e f f e c t of an event changes the event v a r i a b l e s which t r a n s f e r the machine to the <destination> s t a t e . Events are atomic and only one event i s executed at a time. An a r b i t r a t i o n mechanism i s understood at a lower l e v e l which a r b i t r a t e s imultaneously enabled events. b. Topology Part T h i s p a r t s p e c i f i e s the i n s t a n c e s of each P r o t o c o l Machine and how they are i n t e r c o n n e c t e d . N a t u r a l l y , the outgoing channel v a r i a b l e s of one machine are connected to the in-coming ones of the other machine. Consistency must be preserved on these c o n n e c t i o n s . 23 c. P r o p e r t i e s Part T h i s part c o n s i s t s of a set of p r e d i c a t e s d e s c r i b i n g the d e s i r e d behaviour of the l a y e r . U s u a l l y , these p r e d i c a t e s express the g l o b a l p r o p e r t i e s of the l a y e r , but l o c a l p r o p e r t i e s can be expressed a l s o . These, p r o p e r t i e s can be viewed as i n v a r i a n t a s s e r t i o n s of the l a y e r . d. The A l t e r n a t i n g B i t P r o t o c o l i n UNISPEX We now present the s p e c i f i c a t i o n of the A l t e r n a t i n g B i t P r o t o c o l in UNISPEX. Because i n UNISPEX each event ( t r a n s i t i o n ) has to s p e c i f y the PDU i n v o l v e d i n t h i s event, i t i s not p o s s i b l e here to combine the r e c e p t i o n of DATA and the t r a n s m i s s i o n of i t s ACK toa s i n g l e event as we d i d i n the other s p e c i f i c a t i o n s . Consequently, two more s t a t e s are used namely ESTAB1, ACK-WAIT1. The v a r i a b l e s used i n t h i s s p e c i f i c a t i o n are : State V a r i a b l e s s t a t e : represents the s t a t e of the f i n i t e s t a t e machine. Sent, Received : are ghost v a r i a b l e s used to record the messages sent and r e c e i v e d by t h i s s t a t i o n . SendBuf, RecvBuf : B u f f e r s h o l d i n g the messages sent but not acknowledged, and r e c e i v e d but not d e l i v e r e d to the user. Pending : a boolean v a r i a b l e showing ( i f tr u e ) that a message i s sent but not acknowledged y e t . VS, VR : the sequence number of the next message to be sent or r e c e i v e d . I n t e r f a c e v a r i a b l e s 24 MsgToSent, MsgToReceive, MsgToDeliver : The message to be sent or r e c e i v e d or d e l i v e r e d by t h i s s t a t i o n . SS, SR : the sequence numbers of the messages sent or r e c e i v e d by t h i s s t a t i o n . These are used by the lower l a y e r p r o t o c o l . Cmd : a b u f f e r used by the user to i n d i c a t e i t s request to the machine. I t s value t r i g g e r s one of the events Data Receive and Data Sent. Timer : a b u f f e r used by the system timer; i t s value t r i g g e r s the Timeout event. Channel v a r i a b l e s InReq, OutReq : b u f f e r s to i n d i c a t e to the other s i d e a r e c e p t i o n or t r a n s m i s s i o n of t h i s s i d e . InChannel, OutChannel : the messages which are to be r e c e i v e d or have been sent by t h i s s t a t i o n . These v a r i a b l e s model the t r a n s m i s s i o n medium. The p r o t o c o l s p e c i f i c a t i o n i s shown i n APPENDIX 3, while the s t a t e t r a n s i t i o n diagram i s i n f i g u r e 4. F. COMPARISON OF THE THREE SPECIFICATION TECHNIQUES As i t i s understood from t h i s p r e s e n t a t i o n and the given examples, the three techniques are e q u i v a l e n t to each other i n the sense that a s p e c i f i c a t i o n i n one technique can be t r a n s l a t e d to the other. A l l three models use s i m i l a r concepts, to s p e c i f y s e r v i c e p r i m i t i v e s and used p r i m i t i v e s of a p r o t o c o l . In BBN/FST a d i r e c t i o n i n f r o n t of the p r i m i t i v e i s used to d i s t i n g u i s h the two kinds, while FDT •DATA -DATA Timeout (+DAT +DATA where UD means g e t u s e r r e q u e s t f o r r e c e i v i n g d a t a and send the d a t a t o t h e u s e r . F i g u r e 3 . S t a t e T r a n s i t i o n Diagram f o r the U N I S P E X i f i c a t i o n Of ABP 26 uses the r o l e l i s t f o r the same purpose. In UNISPEX, a s e p a r a t i o n of the s e r v i c e p r i m i t i v e s and used ones ( j u s t p r i m i t i v e s ) i s used f o r t h i s k i nd of d i s t i n c t i o n . The t r a n s i t i o n s of the f i n i t e s t a t e machine i n a l l three models, have s i m i l a r syntax. Each t r a n s i t i o n s p e c i f i e s the o r i g i n and d e s t i n a t i o n s t a t e , the t r i g g e r i n g p r i m i t i v e , the e n a b l i n g c o n d i t i o n and the o p e r a t i o o n performed by thee t r a n s i t i o n . The "communication" between p r i m i t i v e s and t r a n s i t i o n s i s q u i t e d i f f e r e n t i n UNISPEX than i n the other two methods. In FDT, FST , t h i s "communication" i s somehow " l o g i c a l " i n the sense that i t i s understood the i n i t i a t i o n of a p r i m i t i v e may t r i g g e r the event(s) that i n c l u d e t h i s p r i m i t i v e i n i t s p r e c o n d i t i o n . In UNISPEX, the communication between p r i m i t i v e s and events i s done v i a shared channel and i n t e r f a c e v a r i a b l e s . The i n i t i a t i o n of a p r i m i t i v e changes the v a l u e s of such v a r i a b l e s which i n turn enables an event. Having d i s c u s s e d the s y n t a c t i c d i f f e r e n c e s of the methods, we now compare them, on d i f f e r e n t grounds. a. Implementation. The f i r s t two methods are s t r i c t l y implementation o r i e n t e d techniques. FDT has a l r e a d y been a u t o m a t i c a l l y implementable, while a s i m i l a r i n t e r p r e t e r f o r the other two techniques i s a c h i e v a b l e . b. M u l t i p l e channels - M u l t i p l e x i n g - S p l i t t i n g . In BBN/FST as w e l l as i n UNISPEX the s p e c i f i c a t i o n of m u l t i p l e e n t i t i e s (connections, etc.) i s done simply by m u l t i p l e c o p i e s of a s p e c i f i c a t i o n module (or P r o t o c o l Machine). The i n t e r c o n n e c t i o n between these modules are e x p l i c i t l y 2 7 s p e c i f i e d i n UNISPEX's Topology s e c t i o n , but BBN's technique does not p r o v i d e s p e c i a l f a c i l i t i e s f o r t h i s . N e v e r t h e l e s s , m u l t i p l e x i n g and s p l i t t i n g i n both methods i s more or l e s s l e f t to the implementors. In FDT, one can s p e c i f y m u l t i p l e channels as a r r a y s of channels. M u l t i p l e x i n g and s p l i t t i n g can be s p e c i f i e d e a s i e r by using the ANY c l a u s e f o r the t r a n s i t i o n s . c . V e r i f i c a t i o n - V a l i d a t i o n . The v e r i f i c a t i o n of a p r o t o c o l ( a l s o c a l l e d v a l i d a t i o n ) i n v o l v e s the proof of absence of harmful s y n t a c t i c e r r o r s as s t a t e deadlock, u n s p e c i f i e d r e c e p t i o n s , and s t a t e a m b i g u i t i e s . A l l three models are based on a f i n i t e s t a t e machine. Consequently, any p r o t o c o l s p e c i f i c a t i o n i n one of these models can be t r a n s l a t e d i n t o a FSM or i n t o a Communicating F i n i t e State Machine. Then, the p r o t o c o l can be v a l i d a t e d v i a r e a c h a b i l i t y a n a l y s i s and decomposition. The method i s thoroughly d e s c r i b e d i n [Vuong83]. The t r a n s l a t i o n of a p r o t o c o l s p e c i f i e d by these techniques i n t o a CFSM, i s not always easy f o r the s t a t e amalgamation reason mentioned b e f o r e . We c l a i m that the UNISPEX s p e c i f i c a t i o n i s more e a s i l y t r a n s l a t e d to a CFSM because of i t s s i n g l e t r a n s a c t i o n events. The other kind of v e r i f i c a t i o n we d e a l with here, i s the v e r i f i c a t i o n of the g l o b a l semantic p r o p e r t i e s of the p r o t o c o l ( i . e . the messages are d e l i v e r e d in the c o r r e c t order e t c . ) , sometimes c a l l e d i n v a r i a n t s of the p r o t o c o l . FDT and FST can l i t t l e c o n t r i b u t e to the v e r i f i c a t i o n of 2 8 p r o t o c o l s (without r e s o r t i n g to some s p e c i a l technique, as in chapter I I I ) , simply because they do not use any u s e f u l kind of IPC between p r i m i t i v e s and t r a n s i t i o n events. In UNISPEX v e r i f i c a t i o n i s a p p l i c a b l e due to the shared v a r i a b l e s . To c a r r y out such v e r i f i c a t i o n i n UNISPEX some technique f o r proving the p a r t i a l c o r r e c t n e s s of concurrent programs should be employed ( l i k e Owicki's t e c h n i q u e ) , but the i n t e r f e r e n c e of shared v a r i a b l e s make such p r o o f s lengthy. U n d e r s t a n d a b i 1 i t y . C l e a r l y FST i s the most understandable and easy to use technique among the t h r e e . FDT becomes mote complicated due to many d i f f e r e n t t r a n s i t i o n types i t p r o v i d e s , while in UNISPEX the shared v a r i a b l e s , although they p r o v i d e means f o r v e r i f i c a t i o n , they decrease the u n d e r s t a n d a b i l i t y of the s p e c i f i c a t i o n . It was s t a t e d before that some s p e c i a l methods must be employed i n order to c a r r y out a v e r i f i c a t i o n of a p r o t o c o l s p e c i f i e d i n FDT or FST. In chapter III we o u t l i n e a method fo r v e r i f i c a t i o n of p r o t o c o l s s p e c i f i e d i n FDT. S i m i l a r approach can be taken f o r the FST method. I I I . VERIFICATION OF PROTOCOLS SPECIFIED IN FDT USING TEMPORAL LOGIC A. THE UNBOUNDED SEQUENCE MODEL We a r g u e d i n t h e p r e v i o u s c h a p t e r t h a t FDT g i v e s no means f o r v e r i f i c a t i o n b c a u s e o f t h e l a c k of l o g i c a l s e m a n t i c s of t h e p r i m i t i v e s and b e c a u s e t h e c o n n e c t i o n s between t h e modules a r e n o t d e f i n e d . In o r d e r t o p r o v i d e t h e s e , we use t h e u n b o u n t e d s e q u e n c e t e m p o r a l l o g i c (USTL) method d e v e l o p e d by H a i l p e r n [ H a i l p e r n 8 0 ] . The method has been s l i g h t l y m o d i f i e d t o f i t t o FDT model. In t h e USTL t h e module u s e s h i s t o r y v a r i a b l e s ( c a l l e d h i s t o r i e s o r h i s t o r y s e q u e n c e s ) f o r e a c h t y p e of messages i t e x c h a n g e s w i t h i t s e n v i r o n m e n t . The o n l y o p e r a t i o n a l l o w e d on h i s t o r i e s i s t h e c o n c a t e n a t i o n of a new e l e m e n t a t i t s end. If a message i s s e n t out o r r e c e i v e d by t h e module, t h i s message i s c o n c a t e n a t e d t o t h e c o r r e s p o n d i n g h i s t o r y s e q u e n c e . In terms o f FDT t h i s means t h a t when an e v e n t o c c u r s ( i n p u t o r o u t p u t ) t h e n t h e message i n v o l v e d i n t h e e v e n t i s c o n c a t e n a t e d i n t h e e v e n t ' s h i s t o r y . •The f o l l o w i n g n o t a t i o n i s u s e d on h i s t o r y v a r i a b l e s : I f A and B a r e h i s t o r y v a r i a b l e s t h e n A^B means t h a t A i s an i n i t i a l s u b s e q u e n c e of B. The n o t a t i o n A=<uvz> means t h a t A i s a h i s t o r y c o n t a i n i n g t h e e l e m e n t s u , v , z , w h i l e |A| d e n o t e s t h e number of e l e m e n t s i n A. I f A=<a. >? n t h e n |A|=n+1 . 1 i=0 1 1 29 30 The c o n c a t e n a t i o n of sequences i s denoted by A=<uvxxy> = <uvxy> Since the only o p e r a t i o n allowed on any h i s t o r y i s the c o n c a t e n a t i o n , the f o l l o w i n g h o l d s : VA(n(A=X o n(A<X))) (Seq) In a d d i t i o n <a°> means that the message a i s repeated 0 or more times, while <a + > denotes 1 or more i n s t a n c e s of a. F i n a l l y , u(A) denotes that a h i s t o r y A w i l l grow unboundedly and uc(A,m) means that a message m occurs unbounded number of times in A. I f c(A,m) i s the number of occurences of m i n A, then the p r e v i o u s two a s s e r t i o n s are d e f i n e d by the formulas: u(A) = Vn(<>(|A|>n)) (u-def) uc(A,m) = Vn(<>(c(A,m)>n)) (uc-def) B. VERIFICATION OF AN FDT SPECIFICATION The p r o p e r t i e s of a module can be d i s t i n g u i s h e d i n t o : s a f e t y p r o p e r t i e s or i n v a r i a n t s , which have the form nA (where A i s a f i r s t order l o g i c formula), 1iveness p r o p e r t i e s or commitments which have the form A o B (where A,B are temporal l o g i c f o r m u l a s ) , and the s e r v i c e or event p r o p e r t i e s . The l a t t e r are a s s e r t i o n s about the s e r v i c e p r i m i t i v e s . For each s e r v i c e p r i m i t i v e (or event) there i s a pre-, post-, and l i v e c o n d i t i o n ( a s s e r t i o n ) d e s c r i b i n g the e f f e c t of the event on i t s h i s t o r y sequence. For i n s t a n c e , a SEND(m) p r i m i t i v e with h i s t o r y A has the p r o p e r t i e s SEND(m) 31 pre : A=A1 post : A-A1<m> l i v e : <>(after SEND) To apply the v e r i f i c a t i o n f o r a module s p e c i f i e d i n FDT, we f i r s t need to express the s t a t e v a r i a b l e s of the module in terms of the h i s t o r y v a r i a b l e s . Having done t h i s , the s a f e t y p r o p e r t i e s of the module can be proved from the t r a n s i t i o n s u s i n g Hoare l o g i c . In order to prove nl i t i s s u f f i c i e n t to prove that I holds i n i t i a l l y and that I i s preserved by each t r a n s i t i o n . Because the t r a n s i t i o n s are atomic, a l l we need to prove i s that i f I holds before a t r a n s i t i o n i t a l s o holds a f t e r i t . The main r u l e we need here i s the f o l l o w i n g : i f e(m) i s an event i n v o l v i n g message mi and i t s h i s t o r y v a r i a b l e i s H then : ( K H ) } e (m) (l(H-<m>) A meH} (E-Rule) where H-<m> i s the h i s t o r y r e s u l t i n g from H i f we d i s c a r d i t s l a s t element m. The l i v e n e s s p r o p e r t i e s of the module are proved from the t r a n s i t i o n a s s e r t i o n s u s i n g the axiomatic system showed in APPENDIX 5. The temporal semantics of each t r a n s i t i o n are expressed by a t r a n s i t i o n a s s e r t i o n . In g e n e r a l a t r a n s i t i o n of the form from f'romstate to t o s t a t e 3 2 when event other c o n d i t i o n begin body end i s t r a n s l a t e d i n t o the a s s e r t i o n . i n fromstate A t r a n s ( o t h e r c o n d i t i o n ) A ( a f t e r event) o <>(in t o s t a t e A post(event) A p o s t ( O l ) . . . A post(On)) where t r a n s ( o t h e r c o n d i t i o n ) i s the t r a n s l a t i o n of other c o n d i t i o n i n terms of the module h i s t o r i e s ; p o s t ( e v e n t ) , p o s t ( O i ) are the p o s t c o n d i t i o n s of the event and the output events Oi t r i g g e r e d by the t r a n s i t i o n ; and " i n " i s a s p e c i a l p r e d i c a t e which i s true i f the system i s i n the s t a t e s p e c i f i e d by i t s argument. For each module there i s one t r a n s i t i o n a s s e r t i o n f o r each FDT t r a n s i t i o n of the module. In a d d i t i o n there are some a d d i t i o n a l "complementary a s s e r t i o n s " which d e s c r i b e the behaviour of the module when an event, expected at a c e r t a i n s t a t e , does not occur ( t h i s w i l l become t r a n s p a r e n t i n the example). F i n a l l y , the g l o b a l p r o p e r t i e s of the system are proved from the p r o p e r t i e s of i t s components using the axiomatic temporal l o g i c system. C. A STOP-WAIT PROTOCOL As an example we s p e c i f y i n FDT and v e r i f y a simple data t r a n s f e r p r o t o c o l , a stop-wait p r o t o c o l with i n f i n i t e sequence number. The p r o t o c o l i s composed of three e n t i t i e s , the t r a n s m i t t e r , the network(or medium), and the r e c e i v e r . The t r a n s m i t t e r gets the next message to be sent from i t s user ( U s e r l ) , adds to i t the sequence number and sends i t to the r e c e i v e r v i a the medium. The t r a n s m i t t e r r e t r a n s m i t s the same message r e p e a t e d l y , u n t i l i t r e c e i v e s an acknowledgment f o r i t . The r e c e i v e r whenever i t r e c e i v e s the next message i t expects, i t d e l i v e r s i t to User2. Every time i t r e c e i v e s a message, i t sends an acknowledgment f o r the l a s t in-sequence message i t has r e c e i v e d . The FDT s p e c i f i c a t i o n of the p r o t o c o l i s given i n APPENDIX 7. In t h i s v e r i f i c a t i o n , we ignore the SENDack p r i m i t i v e sent by the t r a n s m i t t e r to the user i n order to inform him that i t can accept the next message. Here, we imply t h a t a b u f f e r i n g of the messages, sent by the Userl to the t r a n s m i t t e r , takes p l a c e . Consequently, the t r a n s m i t t e r r e c e i v e s the next message from the user when i t i s ready. The only o b l i g a t i o n we impose to Userl i s that he i s always w i l l i n g to send a message; that i s • noU.SENDreq(d) (U1 ) while f o r User2 no o b l i g a t i o n s are s t a t e d . The names of the h i s t o r y v a r i a b l e s used i n the proofs are i n d i c a t e d i n the diagram in f i g u r e 4 . 3^ U s e r l SEND(M) Network1 E x i s t M RECEIVE(M) SENDreq T r a n s m i t t e r RECEIVE(A) E x i s t A Network2 SEND(A) R e c e i v e r RECEIVE, mdic User2 F i g u r e 4 . System Diagram f o r the Stop-Wait P r o t o c o l . 35 1. THE NETWORK The p r o p e r t i e s of the network are given by • meRD o meSD (N1 ) • meRA o meSA (N2) • u(SD) o Exi s t M (N3) • u(SA) o E x i s t A (N4) • uc(SD,m) A u(RD) o o(meRD) (N5) • uc(SA,a) A u(RA) o o ( a e R A ) (N6) Where m, a i s any message, acknowledgment and ExistM, E x i s t A are p r e d i c a t e s that are true i f any message, acknowledgment e x i s t s i n the network. These formulas s p e c i f y a medium with minimum requirements. Nl andN2 denote that the medium does not generate messages by i t s e l f ; any message r e c e i v e d must be p r e v i o u s l y sent. The r e s t denote that the medium can destroy or c o r r u p t a f i n i t e number of messages. In p a r t i c u l a r , the l a s t two formulas s t a t e that i f the same message" i s being sent unbounded number of times, then i t w i l l e v e n t u a l l y be r e c e i v e d i f the " r e c e i v e r " keeps a c c e p t i n g messages. The system module i s viewed as a black box as the user modules do. The only p r o p e r t y we need i s : • STARTTIMER A n~STOPTIMER o oTIMEOUT (Timer) which s t a t e s that i f the timer i s set and never c a n c e l l e d then, e v e n t u a l l y a timeout w i l l be r e c e i v e d . 36 2. THE EVENT PROPERTIES If M denotes a message with id=DATA, A i s one with id=ACK, and d i s any user data , then the p r o p e r t i e s of the events a r e : SENDreq(d) pre: X=X1 post: X=X1<d> l i v e : <>(after SEND.req) RECEIVEindic(d) pre: Y=Y1 post: Y=Y1<d> l i v e : <>(after RECEIVEindic) SEND(M) pre: SD=SD1 post: SD=SD1<M> l i v e : <>(after SEND) RECEIVE(M) pre: RD=RD1 post: RD=RD1<M> l i v e : o E x i s t M o <>(after RECEIVE) SEND(A) pre: SA=SA1 post: SA=SA1<A> l i v e : <>(after SEND) ' RECEIVE(A) pre: RA=RA1 post: RA=RA1<A> 37 l i v e : o E x i s t A o <>(after RECEIVE) We now proceed to express the s t a t e v a r i a b l e s of the t r a n s m i t t e r and r e c e i v e r in terms of the h i s t o r y v a r i a b l e s . We d e f i n e : Mj =[DATA, d i , i ] =[DATA, , i ] A. =[ACK,-,i] We use M ^ f o r the messages sent by the t r a n s m i t t e r and fo r the messages r e c e i v e d by the r e c e i v e r . The main sequence of the t r a n s m i t t e r i s X, while the main sequence of the r e c e i v e r i s Y. I t i s easy to v e r i f y t h a t : i n ESTAB = |X|=0 V A | X | _ i e R A ( s t a t e D in ACR-WAIT = |X|*0 A A| X|_-, ^ R A (state2) i n ESTAB o send-seq=|X| (state3) i n ACK-WAIT D send-seq=|X|-1 (state4) data=d. send-seq resv-seq=|YI (state5) (state6) D. VERIFICATION OF THE STOP-WAIT PROTOCOL 1. SAFETY The i n v a r i a n t s of the t r a n s m i t t e r a r e : • x=<d. > ! x i 1 A SD=<M; >! N l 1=0 i 1=0 Vi<|X|-2(A i eRA) (T1) (T2) 38 T1 s t a t e s that at any time |Xj messages have been r e c e i v e d from the user and a l l these messages have been sent to the network (each one many times) in the order they have been r e c e i v e d . T2 i n c o n j u n c t i o n with T1 denotes that i f n messages have been sent, then the f i r s t n-1 must have been acknowledged. We now give the proof of T1. The proof of T2 i s q u i t e s i m i l a r . For the f i r s t t r a n s i t i o n : {T1} in ESTAB {T1} when U . S E N D r e q ( d s e n d _ s e g ) < x - < d i X|-i >=< di > l x = i 2 a s d = < m 1 >!=o~2.} {X=<d. > i x l " 1 A SD=<M! > ! X I " 2 } 1 i=0 I i=0 begin d a t a = d | x | _ 1 {(same as before) A data=d| X|_ 1 } out N.SEND(DATA, data, send-seq); {X=< d i >! X 0" 1 A S D - < M | X M > = <Mt > i X | - 2 } {T1} out S.STARTTIMER end; { T l } T r a n s i t i o n 2 does not change T1 From t r a n s i t i o n 3 we o b t a i n : {T1} 39 from ACK-WAIT to SAME when S.TIMEOUT begin {T1} out N.SEND(DATA,data,send-seq) U=<d. >{f|- 1 A S D - < M | x M > = <Mt >|f|- 1 } ( T I ) out S.STARTTIMER end {T1} The i n v a r i a n t s of the r e c e i v e r a re: • Y=<dj >|I0~1 A Vi< | Y | - 1 (Mj^  eRD) (Rl) • S A = < A T >|! 0~ 1 (R2) The p r o o f s of them are s i m i l a r to the previous ones. The s a f e t y of the system i s expressed by : • Vn(|Y|=n o |X|>n A Vi<n(d^ =d i )) (S1) which s t a t e s that i f n messages have been r e c e i v e d by User2, then these are the f i r s t n messages sent by U s e r l , and the order i s preserved. Proof of S I 1. |Y|=n Hyp 2. Vi<n(M| eRD) 1,R1 3. Vi<n(M^ eSD) 2, N1 4. Vi<n(M i =M^  A |X|>n) 3,T1 40 5. Vi<n(|X|>n A d! =d i ) 4, def of M,M' 6. S1 1,5,gen. 2. LIVENESS The t r a n s i t i o n a s s e r t i o n s f o r the t r a n s m i t t e r a r e : • i n ESTAB A |X|=k A SENDreq(d) o ( t l ) <>(in ACK-WAIT A X<d k > ASD<M^ > A STARTTIMER) • i n ESTAB A |X|=k D (t2) ( i n ESTAB A |X|=k) U n t i l - A f t e r SENDreq(d) • i n ACK-WAIT A R E C E I V E ( A j x j _ 1 ) o (t3) <>(in ESTAB A RA<A| x | - 1 > A STOPTIMER) • In ACK-WAIT A RECEIVE (A^ ) A k*|X|-1 o (t4) <>(in ACK-WAIT A RA<AR >) • i n ACK-WAIT A TIMEOUT o (t5) <>(in ACK-WAIT A SD<M|X|_1 > A STARTTIMER) • i n ACK-WAIT A |X|=k o (t6) ( i n ACK-WAIT A |X|=k) U n t i l - A f t e r (RECEIVE A| x|_ 1 ) A s s e r t i o n s t l , t 3 , t5 are deduced from the FDT t r a n s i t i o n s using s t a t e 1 s t a t e 5 and the event p r o p e r t i e s . The r e s t are the complementary a s s e r t i o n s of the module and capture the FDT's semantics, namely, i f at a s t a t e no t r a n s i t i o n s are enabled then, the system remains i n the same s t a t e . 41 S i m i l a r l y , the r e c e i v e r a s s e r t i o n s are: • |Y|=k A R E C E I V E R ) o ( r l ) <>(RD<M^ > A Y<d^ > A SA<A^ >) • |Y|=k A RECEIVE(M!^ ) A i*k o (r2) <>(RD<M^ > A SA<A k - 1 >) which correspond to the FDT t r a n s i t i o n s . The l i v e n e s s p r o p e r t i e s of the t r a n s m i t t e r a r e : • noSENDreq o u(SD) (T3) • Vk(A k e A R o | X | >k) A noSENDreq o (T4) V j ( A . e R A D uc(SD,M.., ) V <>A . . e R A ) j ]+1 ]+1 and the r e c e i v e r ' s : • u(RD) o u(SA) (R3) • Vk(M k e R D o |Y|>k) A u(RD) D 1 (R4) Vj(M^ e R D o <>(|Y|>j+1) A (uc(SA,Aj ) V <>(M\ + 1 e R D ) ) ) T3: s t a t e s that i f the user keeps sending messages to the t r a n s m i t t e r then, the t r a n s m i t t e r keeps sending to the network. T4: i f the acknowledgment of a message i s r e c e i v e d a f t e r that message has been sent then, i f the acknowledgment f o r the message j i s r e c e i v e d , the t r a n s m i t t e r keeps sending the next message u n t i l i t s acknowledgment i s r e c e i v e d . R3: i f an unbounded number of messages reach the r e c e i v e r , then an unbounded number of acknowledgments have been sent. R4: Assuming that message k does not a r r i v e u n t i l the r e c e i v e r has processed message k-1, and that messages do not 42 stop coming to the r e c e i v e r , the r e c e i v e r w i l l keep sending an acknowledgment f o r the l a s t message, u n t i l i t r e c e i v e s the next one. These commitments can be v e r i f i e d using the t r a n s i t i o n a s s e r t i o n s and the temporal l o g i c system. Because the proofs are very s i m i l a r to the ones given i n the next chapters f o r the same p r o t o c o l u sing the SETL method, they are ommited here. We only o u t l i n e the proof of T3 to give the f l a v o u r of the proof system used here. From t 1 , t2, D4 we deduce: 1. noSENDreq A i n ESTAB D <>(SD<M>) From t3,...,t6,D5 and (Timer) we o b t a i n 2. i n ACK-WAIT o no( S D ( M ) ) V <>(in ESTAB) From 1,4,Proof by cases,gen and A1: noSENDreq o n<>SD<M> which i m p l i e s T3 s i n c e n<>SD<M> o u(SD) (some message m i s concatenated i n f i n i t e number of times to SD). The l i v e n e s s of the system i s given by the formulas: • u(X) o u(SD) A u(RD) A u(SA) A u(RA) (L1) • n(u(X) A |Y j =n D <>|Y|>n) (L2) The f i r s t one s t a t e s - that i f the user keeps sending messages, a l l the h i s t o r i e s grow unboundedly. T h i s i n d i c a t e s that the system i s s t a r v a t i o n f r e e . L2 i n d i c a t e s that the system i s deadlock f r e e . That i s , i f at any time Y has n messages and the user keeps sending messages, e v e n t u a l l y , another message i s added to Y. We g i v e the proof of L1: 1. u(X) o noSENDreq Def of u 43 2. u(X) o u(SD) 1,T3,o-Trans. 3. u(X) D <>(RECEIVE(M)) 2,N3,live-REC. 4. u(X) o no(RECEIVE(M) ) 3,gen, u-def, A1 5. U ( X ) _ D _ U ( R D ) 4, u-def. 6. u(X) D u(SA) R3 7. u(X) o <>(RECEIVE(A)) 6, N4, l i v e - R E C . 8. u(X) D u(RA) 7, gen, u-def, A1. 9. L1 2 8,A I n t r . We do not inte n d to give the proof of L2 here. More vi g o r o u s p r o o f s f o r t h i s p r o t o c o l w i l l be given i n chapter IV. T h i s chapter o u t l i n e d how a v e r i f i c a t i o n technique can be a p p l i e d to an FDT s p e c i f i c a t i o n , and i t has prepared the ground f o r the SETL technique. Undoubtedly, the r u l e s used here are ad hoc r u l e s , and moreover, the use of one system for p r o v i n g i n v a r i a n t s and a d i f f e r e n t one f o r commitments, i s c l e a r l y a disadvantage. In a d d i t i o n , a l l these h i s t o r i e s not only produce a c o n f u s i o n , but they a l s o complicate the p r o o f s to a high degree. Having t h i s i n mind, we i n t r o d u c e the S i g n i f i c a n t Event Temporal Log i c technique which can be used f o r v e r i f i c a t i o n , as w e l l as, f o r s p e c i f i c a t i o n of p r o t o c o l s and which overcomes the d i f f i c u l t i e s mentioned here. IV. THE SIGNIFICANT EVENT TEMPORAL LOGIC TECHNIQUE A. THE SIGNIFICANT EVENT MODEL (SEM) The b a s i c c o n s t r u c t i o n u n i t i n a system or i n a p r o t o c o l i n p a r t i c u l a r i s the module. A module i s capable of performing c e r t a i n f u n c t i o n s and, i n i t s t u r n , i t may be composed of s e v e r a l submodules which i n t e r a c t with each o t h e r . Modules and submodules i n t e r a c t with each other and with t h e i r environment by means of events. In a module we can d i s t i n g u i s h two kinds of events : input events that i s , i n t e r a c t i o n s i n i t i a t e d by the environment and output events which are i n i t i a t e d by the module i t s e l f . In t h i s model there i s no d i s t i n c t i o n between modules and submodules; both are c a l l e d modules. The set of a l l the i n t e r a c t i o n s (input and output events) between two modules c o n s t i t u t e a communication channel or simply a channel shared by the modules. The events i n a channel shared by two c o o p e r a t i n g modules are d i r e c t l y coupled i n the sense that an output event at one end of the channel i s s i m u l t a n e o u s l y viewed as input event at the other end. Moreover, only one event can occur i n a channel at an instance of time. T h i s i s what we c a l l D i r e c t l y Coupled Events Rule (DCER). The s t a t e of a module at any i n s t a n c e of time i s d e f i n e d by the s i g n i f i c a n t event sequence (SES) denoted by a. T h i s i s the sequence o'f a l l the s i g n i f i c a n t events o c c u r r e d i n any channel of the module from i t s i n i t i a t i o n 44 45 t i l l the present time. By the term s i g n i f i c a n t event we denote an event t h a t , when i t occur s , i t changes the s t a t e of the system. A l l the p o s s i b l e s t a t e changes f o r a module are denoted by the t r a n s i t i o n s or t r a n s i t i o n semantics of the module. Consequently, an input event i s a s i g n i f i c a n t one i f at the time i t occurs, a t r a n s i t i o n i s enabled ( i t t r i g g e r s a s t a t e t r a n s i t i o n ) , while any output event i s a s i g n i f i c a n t one. The f o l l o w i n g r u l e s h o l d f o r the events of any module: a. Many input events can occur s i m u l t a n e o u s l y (at d i f f e r e n t channels) but only one of them i s r e a l i z e d by the module at a time. The r e s t remain o u t s t a n d i n g f o r the next time. The choice i s a r b i t r a r y . By the term " r e a l i z e d " we mean that an event has occured and the module has deci d e d to a c t on i t . b. I f an input event has been r e a l i z e d at a s p e c i f i c time then, i f i t i s a s i g n i f i c a n t one, i t i s concatenated to the event sequence i n the next time i n t e r v a l (meaning i t becomes p a s t ) . Otherwise, i t i s simply ignored and the system remains at the same s t a t e . c. When an input event occurs i t i s always r e a l i z e d at some f u t u r e time. d. I f a s i g n i f i c a n t input event (when r e a l i z e d ) causes some output events to occur, then these output events are concatenated to o at the same time with the input event (meaning that the t r a n s i t i o n s are at o m i c ) , and they c o n s i t u t e the c u r r e n t events of the module at that time. 46 The above r u l e s are c a l l e d Event Rules or ER . The method resembles the Event-Based method developed by F. Vogt [Vogt82], i n the sense that i t a l s o uses event sequences to encode i n f o r m a t i o n about a module. I t d i f f e r s from the Event-Based technique in many r e s p e c t s . In p a r t i c u l a r , i n SETL each module has i t s own sequence which i n c l u d e s only the s i g n i f i c a n t events occurred i n the module, and i t d e f i n e s the s t a t e of the module at any time. SETL s p e c i f i e s the module behaviour by a set of s t a t e t r a n s i t o n s which d e f i n e the next p o s s i b l e s t a t e of the module. Consequently i n v a r i a n t ( s a f e t y ) p r o o f s are f e a s i b l e in SETL. F i n a l y , the axiomatic system used i n SETL i s q u i t e d i f f e r e n t from the one used bu F. Vogt. B. SPECIFICATION LANGUAGE A p r o t o c o l , a c c o r d i n g to the ISO model, i s viewed as a set of i n t e r a c t i n g modules . Consequently, a p r o t o c o l s p e c i f i c a t i o n c o n s i s t s of the s p e c i f i c a t i o n of the p r o t o c o l modules and the channels shared among them. In SELT, the channels are s p e c i f i e d i n e x a c t l y the same way as i n ISO/FDT. A module s p e c i f i c a t i o n c o n s i s t s o f : 1. The module header which i n d i c a t e s the name of the module and the channels used by i t ( t h i s i s again i d e n t i c a l to the ISO/FDT module header); 2. The event sequence a f o r the module; and 3. The t r a n s i t i o n s . 47 The language used to s p e c i f y the t r a n s i t i o n s i s the temporal l o g i c augmented by some f u n c t i o n s on a, and some s p e c i a l p r e d i c a t e s . For the s t a t e sequence s=s Q , s 1 we use the n o t a t i o n s+n = s„ , s n „ ,. n ' n+1 and £ i s the e x i s t e n t i a l q u a n t i f i e r . The i n t e r p r e t a t i o n of a temporal formula A on s, denoted as A g i s d e f i n e d as : 1. If A i s an atomic p r e d i c a t e then A g = s 0 ( A ) ; that i s , A i s e v a l u a t e d at the c u r r e n t s t a t e . 2. (A L B) = A L B where L can be A, V, o and (~A) = ~A s s s s s 3. ( n A ) s = Vn>0 ( A g + n ) 4. (<>A) c = &n>0 (A , n ) s s+n, 5. (OA) s = A s + 1 6. (A U n t i l B) = Vn>0 [V0<i<n (~ B .. )] o A . s s+i s+n 7. (A U n t i l - A f t e r B) = (A U n t i l (A A B)) s s It i s c l e a r that U n t i l i s the only operator that we need s i n c e nA = A U n t i l f a l s e and <>A=~n~A For reasoning about the event sequences, we use the f o l l o w i n g n o t a t i o n : a=[A , ...,An ] denotes that a i s a sequence of events of kind , ... ,A n o=<e ^ >"_cjenotes that o c o n t a i n s the events (must be of * the same kind) e n , ... ,e„ i n t h i s order. In a d d i t i o n e 0 n denotes 0 or more c o n s e c u t i v e i n s t a n c e s of e, while e denotes 1 or more. + 48 The f o l l o w i n g f u n c t i o n s on the a sequence are used : \o\ r e t u r n s the number of events i n a. Note t h a t : i f o=<e1 >"_Q then|a| =n+1. P(a,Y) i s the p r o j e c t i o n f u n c t i o n on a. I t retu r n s a sequence which c o n t a i n s only the events of kind Y which are i n a and i n the same order they occur. F i n a l l y , s u f f ( a , Y ) i s the s u f f i x f u n c t i o n (as i t i s d e f i n e d by F. Vogt i n h i s event model). I t i s d e f i n e d as: a=<a 1 x y x s u f f ( o, Y) > and, P(suff(o,Y),Y)=X where X i s the empty sequence. The only o p e r a t i o n allowed to be done on a by the t r a n s i t i o n s i s the a d d i t i o n of new events. We use the n o t a t i o n a<e 1 ,...,e n > to d e f i n e the sequence r e s u l t i n g from a by c o n c a t e n a t i n g to i t the events e. ,...,e . The order of the c o n c a t i n a t e d 1 n events i s i r r e l e v a n d , but an e x p r e s s i o n of the form o<e^ , . .. ,e n ><m.| , . . . ,m^  > denotes that events e ^ occur before events m j Consequently, events e are past events, while, events m are the c u r r e n t ones. T r a n s i t i o n s , i n g e n e r a l , express the f a c t t h at i f at a c e r t a i n i n s t a n c e of time a v a l i d input event (not v i o l a t i n g the h i s t o r y a) i s r e a l i z e d , then the next time t h i s becomes "past", and the output events t r i g g e r e d by t h i s , become the l a s t " c u r r e n t " events of o. The l a s t events are considered 49 c u r r e n t and past at the same time. (This i s s i m i l a r to the not i o n of pre s e n t - p a s t events d e f i n e d by F. Vogt i n h i s event model). Consequently, each t r a n s i t i o n has the form C A [ a = a O ] A [ a t ( e ) ] D O([o = a 0<exo ] , . . . , o n >] A [o 1 ] . . .A t o „ ] ) where [ a t ( e ) ] means t h a t input event e has occu r r e d and r e a l i z e d by the module; [o=a0] means that the sequence of events a i s aO, while [ a = a < e x o ^ ,...,o n >] means that the sequene a c o n t a i n s a l l the events i n oO and the events e, o 1 ,...,o n ; C i s the e n a b l i n g c o n d i t i o n of the t r a n s i t i o n ; o ,...,o are the output events t r i g g e r e d by the t r a n s i t i o n ; and [o^ ] means that the event o^ occ u r s . Note that f o r an input event e [e] means that the event e has occurred but not yet r e a l i z e d , while [ a t ( e ) ] means that e has been r e a l i z e d by the module. Consequently, the f o l l o w i n g r u l e s h o l d : • [e] o <>[at(e)] (E-Rule) • ( C o (C U n t i l - A f t e r [ a t ( e ) ] ) ) A [e] o (TR-Rule) <>(C A [at( e ) ]) C. TEMPORAL LOGIC SYSTEM The axiomatic temporal shown i n APPENDIX 5. l o g i c system used i n SETL i s 50 D. VERIFICATION IN THE SETL TECHNIQUE The p r o p e r t i e s of a module are of two kin d s : s a f e t y p r o p e r t i e s and l i v e n e s s ones. Saf e t y p r o p e r t i e s (or i n v a r i a n t s ) have the form n l ( o ) where I i s a f i r s t order l o g i c formula. To prove ul(a) i t i s s u f f i c i e n t to prove that I holds i n i t i a l l y (when a=X) , and that i t i s preserved by each t r a n s i t i o n ; that i s , i f l ( 0 b e f o r e ) o I ( a a f t e r ) where abefore and crafter are the sequences before and a f t e r the "exec u t i o n " of a t r a n s i t i o n , (I-Rule) . T h i s r u l e comes from the f a c t that t r a n s i t i o n s are c o n s i d e r e d to be atomic, the i n t e r p r e t a t i o n of 0 (next s t a t e ) , and the theorem Th1. Li v e n e s s p r o p e r t i e s (or commitments) have the form A o B where A and B are temporal l o g i c formulas. These p r o p e r t i e s are proved from the t r a n s i t i o n s using the axiomatic system. In the above proofs we assume that the t r a n s i t i o n s s p e c i f i e d i n the t r a n s i t i o n s e c t i o n of the module s p e c i f i c a t i o n d e f i n e a l l the p o s s i b l e changes the event sequence of the module can a t t a i n . I f at some s t a t e none of them i s enabled then the event sequence remains the same u n t i l some fut u r e s t a t e at which some t r a n s i t i o n i s enabled.This assumption ( c a l l e d the U n s p e c i f i e d T r a n s i t i o n s Assumption or UTA) i s used i n order to leave u n s p e c i f i e d the t r a n s i t i o n s (axioms) which does not change the event sequence. 51 F i n a l l y , the g l o b a l p r o p e r t i e s of a system are proved from the p r o p e r t i e s of i t s components using the axiomatic system. Note: The p r o o f s given i n t h i s t h e s i s f o r the p r o t o c o l s s p e c i f i e d i n SETL are not e x a c t l y formal p r o o f s . They are s i m i l a r to the p r o o f s given i n [Hailpern80] and i n [Vogt82]. In order to have formal p r o o f s a complete system of axioms ( t r a n s i t i o n s ) must be given f o r each module as w e l l as f o r the event sequences and t h e i r o p e r a t i o n s . N e v e r t h e l e s s , the given p r o o f s demonstrate the f l a v o u r of t h i s technique and allow us to remain c l o s e to the ISO/FDT s p e c i f i c a t i o n s . .E. TRANSLATION FROM FDT TO SETL In FDT the s t a t e of a module i s d e f i n e d by the values of the "major s t a t e " v a r i a b l e and some other v a r i a b l e s c a l l e d s t a t e components (e.g. sequence number, e t c . ) . These s t a t e components need to be t r a n s l a t e d i n SETL using the event sequence a and the d e f i n e d f u n c t i o n s . In some cases s p e c i a l f u n c t i o n s on a must be d e f i n e d i n order to express some v a r i a b l e s (as c r e d i t s a v a i l a b l e or f i n i t e sequence no.) as f u n c t i o n s of a. T r a n s i t i o n s can be e a s i l y t r a n s l a t e d . Each FDT t r a n s i t i o n has i n general the form : from fromstate to t o s t a t e when event e n a b l i n g c o n d i t i o n 52 t r a n s i t i o n body. T h i s i s t r a n s l a t e d to t r a n s l a t e ( f r o m s t a t e , e n a b l i n g c o n d i t i o n ) A[a=aO] A [ a t ( e v e n t ) ] o 0([a=aO<eventxout events>] A [out ev e n t s ] ) where t r a n s ( f r o m s t a t e , e n a b l i n g c o n d i t i o n ) i s the c o n d i t i o n that r e s u l t s from t r a n s l a t i n g fromstate and e n a b l i n g c o n d i t i o n i n SETL terms; and out events are the events i n i t i a t e d by the body. S i m i l a r r u l e s can be deduced f o r the other t r a n s i t i o n types. For v e r i f i c a t i o n purposes, i n SETL we need i n a d d i t i o n to the e n t i t y s p e c i f i c a t i o n s , the s p e c i f i c a t i o n s of a l l the other modules i n v o l v e d i n the system ( i . e . network module, user modules, op. system module, e t c . ) . These s p e c i f i c a t i o n s are c a l l e d " A d d i t i o n a l Modules". For each, one of these modules only t h e i r p r o p e r t i e s ( s a f e t y and l i v e n e s s ) need to be s p e c i f i e d and they are given i n the s e c t i o n c a l l e d " A d d i t i o n a l Modules". In the r e s t of t h i s chapter, we give two exambles f o r the SETL technique. Using SETL, we s p e c i f y and v e r i f y the stop-wait and the a l t e r n a t i n g b i t p r o t o c o l s . F. A STOP-WAIT PROTOCOL The f u n c t i o n i n g of t h i s p r o t o c o l was presented i n the pr e v i o u s chapter. The SETL s p e c i f i c a t i o n of the p r o t o c o l i s given i n APPENDIX 6 while APPENDIX 7 c o n t a i n s the FDT s p e c i f i c a t i o n f o r the same p r o t o c o l . The a b b r e v i a t i o n s ( s t a t e 1 ) , ( s t a t e 2 ) i n the SETL s p e c i f i c a t i o n give a h i n t f o r the t r a n s l a t i o n between the two s p e c i f i c a t i o n s . In a d d i t i o n , we need to express the other s t a t e components namely send-seq and recv-seq with SETL formulas. T h i s i s achieved by : in ESTAB o send-seq = |us(o)| in ACK-WAIT o send-seq = |us(a)|-1 and recv-seq = | u r ( a ) | Having s t a t e d t h a t , the t r a n s l a t i o n should be t r a n s p a r e n t , but some e x p l a n a t i o n s must be given f o r the p r o p e r t i e s of the a d d i t i o n a l modules. In the SETL s p e c i f i c a t i o n s : (U1), s t a t e s that the u s e r l i f i t sends a message, i t sends i t a f t e r i t r e c e i v e d an i n d i c a t i o n that the p r e v i o u s one was indeed d e l i v e r e d to the other user. (U2) s t a t e s the w i l l i n g n e s s of u s e r l to send a message a f t e r the l a s t acknowledgment. (Timer) gi v e s the l i v e n e s s property of the timer. That i s , i f the timer i s set a f t e r the l a s t TIMEOUT or STOPTIMER then a TIMEOUT i s expected. The Network module d e s c r i b e s the p r o p e r t i e s of a medium with minimum requirements. T h i s medium may l o s e or dest r o y or c o r r u p t a f i n i t e number of messages (N3, N4, N5, N6), but can not generate messages by i t s e l f (N1,N3). Moreover, t h i s medium i s not n e c e s s a r i l y a FIFO one. I t i s assumed that message c o r r u p t i o n i s d e t e c t e d by a l o w e r - l e v e l mechanism and c o r r u p t e d messages are d i s c a r d e d . 54 In t h i s s p e c i f i c a t i o n we use the pseudo-functions data, i d , seq, which i f a p p l i e d to any event, they r e t u r n the value of the coresponding f i e l d of the message of the event. We now are ready to proceed i n the v e r i f i c a t i o n of the p r o t o c o l . G. VERIFICATION OF THE STOP-WAIT PROTOCOL For t h i s p r o t o c o l we want to prove: F i r s t , that i f any messages are d e l i v e r e d to User2, these are the messages sent by Userl and they are d e l i v e r e d i n the order they were sent ( s a f e t y ) . And second, t h a t i f Userl keeps sending messages, at some f u t u r e time messages w i l l indeed be d e l i v e r e d to User2 ( 1 i v e n e s s ) . In order to prove the above p r o p e r t i e s we need f i r s t to s t a t e and prove the i n v a r i a n t s and commitments of the sender ( c o n s i s t i n g of the t r a n s m i t t e r and the system module) and the r e c e i v e r . Note : In the pr o o f s f o r t h i s p r o t o c o l as w e l l as f o r the a l t e r n a t i n g b i t p r o t o c o l every term i s understood to be enc l o s e d i n '[ ] ' . Note : S i n c e t h e r e i s not c o n f u s i o n , we use a f o r both Sender and R e c e i v e r . 1. SENDER The s a f e t y s p e c i f i c a t i o n s of the sender are given by the i n v a r i a n t s : 55 • n(us(a)=<us i >|=g ( a ) ' 1 A < T 1 > sd(a)=<sd! > | ^ U ) 1 _ 1 ) . n(r a ( a ) = < r a i > l ^ ( f f ) ' " 2 ) (T2) In the i n v a r i a n t p r o o f s we use a to denote the sequence before the execution of a t r a n s i t i o n and anext to denote the sequence at the next s t a t e ; that i s a f t e r executing a t r a n s i t i o n . Proof of T1 In t h i s proof T1 r e f e r s to the formula T1 without n. 1. i n ESTAB A at(u s ) A T1(a) o -Tl(anext) t l s i n c e us(anext)=us(a)<us, / \ i > |us(a) | and|us(a)| =|us(anext)| -1, and s d i , . A, , e anext j us(anext) |- 1 2. i n ESTAB A at(u s ) A T l ( a ) o 0 ( T l ( a ) ) 1, O-i n t e r p . 3. i n ACK-WAIT A a t * r a | u s ( f f ) | _ ! A T 1 ( c ) o t2, O - i n t . T1(anext) o 0(T1(a)) 4. i n ACK-WAIT A at(TIMEOUT) A T l ( a ) o t3, O - i n t . T1(anext) o 0(T1(a)) 5. T1(a) o 0T1(a) 1 , ... ,4, UTA 6. n(T1(a) o 0T1(a)) 5, gen. 7. T l ( a ) o nT1(a) T h l . 8. T1(a) s i n c e T1(X) i s tr u e 9. nT1(a) 7,8,mp. 56 Proof of T2 The proof i s q u i t e s i m i l a r to the pr e v i o u s one. The l i v e n e s s p r o p e r t i e s of the t r a n s m i t t e r are expressed by the commitments: • We d e f i n e : UC = n((a=X) V (ua e s u f f ( a , u s ) ) o o u s ) • UC o n o s d (T3) • V k ( r a k o |us(a)|>k+l) o V k ( r a R o <>(ra f e ea)) (T3 1) • V k ( r a k e a o|us(o)| >k+l)) A UC o (T4) V j ( r a j eoo n<>sd^ + 1 V <>(ra_j + 1 eo) ) To prove these commitments, we need some p r o p e r t i e s f o r the sender deduced by a p p l y i n g the UTA and (Timer). These a r e : • i n ESTAB o in ESTAB U n t i l - A f t e r a t ( u s ) ( t p l ) • i n ACK-WAIT o (tp2) in ACK-WAIT U n t i l - A f t e r a t ( r a , / \ i , ) |us(o)|- 1 • i n ACK-WAIT A ~ a t ( r a , , \\ , ) o oTIMEOUT (tp3) |us(o) I - I c • ua e 'suff(a,us) = r a | u s ( a ) | e ° (tp4) • n ( i n ESTAB V i n ACK-WAIT) (tp5) tp1, tp2 are deduced from the f a c t s that i n ESTAB A (~at(us) o 0 ( i n ESTAB), and in ACK-WAIT A ~ a t ( r a . , . ) o 0 ( i n ACK-WAIT) I us(o) I -1 the UTA and the axiom A6. tp3 can be deduced from the f a c t that i n ACK-WAIT A ~ a t ( r a • , , ) o 0(SETTIMER e |us(o) I -1 suff(a,[STOPTIMER,TIMEOUT]). 57 tp4 comes from the f a c t that ua and ra , / \ i , are always |us(a)|-1 1 added to o at the same s t a t e ( t 2 ) . We now give the pr o o f s of the commitments. Proof of T3 1 . UC 2 . i n ESTAB o o u s 3. i n ESTAB o <>(in ESTAB A at ( u s ) ) 4. i n ESTAB o o s d 5. i n ACK-WAIT o n ( i n ACK-WAIT A ~ a t ( r a | u s U ) | - 1 ) } V <>(in ACK-WAIT A • a t ( r a | u s U ) | - 1 } ) 6. i n ACK-WAIT o n o ( i n ACK-WAIT A at(TIMEOUT)) V <>(in ACK-WAIT A ra , , . ) I u s ( a ) |- 1 7. i n ACK-WAIT o n o s d V o ( i n ESTAB) 8. i n ACK-WAIT o o s d 9. o s d 10. n o s d 11. UC o n o s d Proof of T3' 1. V k ( r a k D |us(a)| ^ k+1) 2. r a ^ A r a ^ /a o |us(a)|=k+1 Hyp 1, tp4, s t a t e l 2, tp1, TR-Rule 3, t1,Th , I-Trans tp2, A8, o-trans 5, tp3, TR-Rule 6,t2,t4 7,4 4,8, Proof by Cases, tp5 9, gen 1,10,D3. Hyp 1 ,T2 58 3. r a ^ A r a ^ /a o in ACK-WAIT A r a R A |us(o)|=k+1 4. r a ^ A r a ^ /a a <>(rajj, eo) 5. r a ^ A r a ^ ea o <>(ra^ ea) 6. r a ^ o <>(rajj. eo) 7. T3' Proof of T4 1 . UC 1'. i n ESTAB o <> us 2. V j ( r a R eo o |us(a) |>k+1) 3. ra_j eo o r a ^ eo A ( r a j + ^ eo V r a j + i 4. r a ^ eo A ra j + 1 /a o |us(o)|=j+1 V |us(a)|=j+2 5. |us(a)|=j+1 A r a ^ eo o i n ESTAB A |us(a)|=j+1 6. i n ESTAB A |us(a)|=j+1 o <>(in ACK-WAIT A |us(a)|=j+2) 7. i n ACK-WAIT A |us(a)|=j+2 o n o ( i n ACK-WAIT A |us(a)|=j + 2 A at(TIMEOUT)) V <>(in ACK-WAIT A a t ( r a | u s ( a ) | - 1 } ) 2, state2 3, t2, tp2, TR-Rule 4,5,Proof by Cases Hyp 1, tp4, s t a t e l Hyp 2, sub,T2 s t a t e 1 t p l , 1', TR-Rule, T1, D1,o-Trans tp2, A8, tp3 59 8. <>(in ACK-WAIT A us(a)=j+2)o 7, D1, t2,t3,TR-Rule no(sd_j + 1 ) V <>(raj + 1 eo) 9. |us(a)|=j+1 A r a ^ eo o n o ( s d j + 1 ) V <>(ra^ + 1 eo) 10. |us(a)|=j+2 A r a ^ + 1 /a o i n ACK-WAIT A |us(a)|=j+2 11. |us(a)|=j + 2 A ra_j + 1 /a o n o ( s d j + 1 ) V <>(r3j + 1 eo) 12. r a j eo A r&^ + ^ i o o n o ( s d j + 1 V <>(raj + 1 eo) 13. r a j + 1 e o D < > ( r a j + 1 ea) 14. r a j eo o n<>(sdj + 1 V < > ( r a j + 1 eo) 15. T4 5, 6, 7, 8, o-Trans state2 10, 7, t2, t3 4,9,11,Proof by Cases, o-Trans 3,12,13, Proof by Cases, o-Trans 1 , 2,14,D3, o to A Trans 2. RECEIVER The s a f e t y p r o p e r t i e s of the r e c e i v e r are : • n(ur(a)=<ur i ^ Q ^ ' " 1 A V i s | ur Co) | - 1 ( rd. ea)) (R1 ) • n(sa(a)= < s a ! > j = o ( a ) | ~ 1 •> (R2) and i t s l i v e n e s s commitments a r e : • n o r d o n o s a (R3) • V k ( r d k o <>(rd k ea)) (R3') 60 • n ( r d k o |ur(a)|>k) A n o r d o (R4) V j ( r d j ea o (<>(|ur(a)|>j+1) A ( n o saj V <>(rdj + 1 ea)))) The p r o o f s of these formulas are s i m i l a r to the p r o o f s f o r the sender p r o p e r t i e s and they are omitted. 3. SAFETY OF THE SYSTEM The s a f e t y of the system i s expressed by : • n(ur(a)=<ur i > i = 0 0 ( S 1^ Vi<n((us^ ea) A data(us^ )=data(ur^ ))) which s t a t e s that i f n+1 messages have been r e c e i v e d by the user2 these are the f i r s t n+1 messages.sent by u s e r l and the order i s preserved. Proof of S1 1. UR = ur(a)=<ur. > i = o 2. UR o V<n((rd i ea) A data {ur^ ) = d a t a ( r d i )) R1 def ur, dr 3. UR o V i < n ( ( s d i ea) A d a t a ( s d i )=data(ur i )) 2, N1 4. UR o V i < n ( ( u s i ea) A d a t a ( u r i )=data(us i )) T1, def sd, us Since U1 holds i m p l i e s that the uSj 's i n a are the only messages the u s e r l has sent. 61 4. LIVENESS OF THE SYSTEM The l i v e n e s s of the system i s given by: • n o s d A a o r d A n o s a A n o r a (L1) • n(|ur(a)|=n o <>(|ur(a)|>n)) (L2) The f i r s t formula denotes that the system i s s t a r v a t i o n f r e e ; t h at i s , i n f i n i t e l y many messages are t r a n s f e r e d through each one of the four system channels.The second formula expresses the system l i v e n e s s ; that i s , at any time i f user2 has r e c e i v e d n messages then he w i l l d e f i n a t e l y r e c e i v e the next message at some f u t u r e p o i n t . We now g i v e the p r o o f s of L1 and L2. Proof of LI 1. UC U1, tp4 2. n o s d 1, T3, mp 3. o r d 2, N5, mp 4. n o r d 3, gen 5. n o s a 4, R3, mp 6. o r a 5, N6, mp 7. n o r a 6, gen 8. L1 2, 4, 5, 7 A - I n t r Proof of L2 F i r s t we prove the hypotheses of T4, T3' and R4 : 1. r a ^ V r a k eo o sa^ eo N2 2 . s a k eo o |ur(a) \> k + 1 R2 3. |ur(a)|>k+1 o r d R eo R1 4. r d k eo o s d k eo N1 62 5. s d k eo o |us(o)|>k+1 6. V k ( r a R V r a k eo o |us(o)|>k+1) 7. |us(a)|>k+1 o r a k - 1 eo 8. ^ a ^ . i £ o ^ s a k - 1 e o 9. s a k _ 1 eo o |ur(o)|>k 10. V k ( r d R V r d k eo o |ur(a)|>k) T1 1 , . . . ,5, o-Trans, gen T2 N2 R2 4,5,7,8,9,o-Trans, gen Now we prove L2: 11. V j ( r a ^ eo o n o ( s d j . + 1 ) V < > ( r a j + 1 eo)) 6, U1, T4, mp 12. V j ( r d j eo D <>( |ur(a) |>j + 1 ) A ( n o s a j V <>(rdj + 1 eo))) 13. |ur(c)|=n o r d n - 1 eo L1, 10, R4, mp R1 14. |ur(a)|=n o n o s a n _ 1 V <>(rd eo) n 13, 12, sub, D-Trans 15. n o s a n _ 1 o o ( r a eo) N6, U1, T3', o-Trans 16. <>(ra . eo) o n o s d V n-1 n <>(ra eo) n 11,sub,D1,Th6,Th15 17. n o sd o <>(rd eo) n n 18. <>(rd n eo) o o ( | u r ( o ) \>n+1) N3, R3' 12, sub 6 3 19. <>(ra„ eo) o <>(sa eo) n n N2, D1 20. <>(sa n eo) o <>(|ur(o)|>n+1) 21 . L2 R2, D1 14, , 20, Proof by Cases, gen. H. THE ALTERNATING BIT PROTOCOL As a second example, we g i v e the s p e c i f i c a t i o n and v e r i f i c a t i o n of the a l t e r n a t i n g b i t p r o t o c o l . T h i s p r o t o c o l i s simple enough but not a t r i v i a l one, and i t i s regarded as a c l a s s i c a l example in any t e c hnique. Here, t r y i n g to be c l o s e to the FDT s p e c i f i c a t i o n f o r the same p r o t o c o l (given p r e v i o u s l y ) , we s p e c i f y the p r o t o c o l on a f u l l duplex channel. Moreover, a b u f f e r i s used to s t o r e the in-coming messages i n s t e a d of d e l i v e r i n g them immediately to the user. The SETL s p e c i f i c a t i o n of the p r o t o c o l i s given i n APPENDIX 8. F i r s t , note that we do not use t h i s time the flow c o n t r o l mechanism (on the sending user) used i n the stop-wait p r o t o c o l . In t h i s case we want to prove that the user-messages , the e n t i t y r e c e i v e d when i t was ready to r e c e i v e (when i t was i n ESTAB s t a t e ) , have been c o r r e c t l y t r a n s m i t t e d and d e l i v e r e d to the other user. Consequently, here we imply that the user sends messages only when the system i s i n ESTAB s t a t e , and the only commitment we need f o r the user, i s that he i s always w i l l i n g to send and r e c e i v e messages (U1, U2). 64 We assume that the b u f f e r , used by the e n t i t y i s manipulated by the o p e r a t i n g system. The o p e r a t i o n s on the b u f f e r are expressed as events (or messages) i n the system channel. Another way to d e f i n e the b u f f e r i s by using an a b s t r a c t data type. Then, the b u f f e r s t a t e c o u l d be d e f i n e d by the sequence of o p e r a t i o n s . The b u f f e r p r o p e r t i e s are s p e c i f i e d by the a b b r e v i a t i o n s b f 1 , bf2 and the formulas B1 to B6 i n the system module. The b u f f e r i s not empty i f the number of data s t o r e d i n i t i s g r e a t e r than the number of data removed ( b f l ) , w hile, i f the number of data in i t i s l e s s than i t s c a p a c i t y , the b u f f e r i s not f u l l ( b f 2 ) . B1 s p e c i f i e s that the b u f f e r i s a FIFO one; the i t h r e t r i e v a l g i v e s the data s t o r e d by the i t h " s t o r e " o p e r a t i o n . The other formulas give the l i v e n e s s p r o p e r t i e s of the b u f f e r . Note that the s t o r e event i s a b l o c k i n g one, i f the b u f f e r i s f u l l . Since i n SETL we can not have b l o c k i n g output events, i f such an event i s i n i t i a t e d by a t r a n s i t i o n , the negation of i t s b l o c k i n g c o n d i t i o n (here B u f - n o t - f u l l ) i s added to the c o n d i t i o n of the t r a n s i t i o n ( t 4 ) . The network module has the same p r o p e r t i e s with the p r e v i o u s one with the a d d i t i o n of the FIFO requirements. Because the p r o t o c o l uses only one b i t f o r sequence numbers, a delayed o l d message with sequence number d i f f e r e n t from the sequence number of the l a s t message, i s i n t e r p r e t e d as the next c o r r e c t message and i t i s accepted. T h e r e f o r e , t h i s requirement i s v i t a l f o r the p r o t o c o l v e r i f i c a t i o n . The f u n c t i o n msg used in t h i s module takes as argument an event 65 and r e t u r n s the message i n v o l v e d i n i t . The network as s p e c i f i e d here i s connected to two i d e n t i c a l p r o t o c o l e n t i t i e s E and E'. When we r e f e r to the sequence, events, p r o p e r t i e s e t c . of the second e n t i t y we use a (') to d i s t i n g u i s h them from the corresponding ones of E. I t i s t r a n s p a r e n t here t h a t , f o r v e r i f i c a t i o n purposes, the topology of the system should be s p e c i f i e d a l s o . Although a syntax s i m i l a r to the UNISPEX topology syntax i s a p p l i c a b l e here, t h i s s u b j e c t i s f o r f u r t h e r study. T h e r e f o r e , the n o t a t i o n mentioned i n t h i s paragraph, i s used i n order to overcome the lack of topology s p e c i f i c a t i o n . The t r a n s i t i o n semantics f o r the e n t i t y are exact t r a n s l a t i o n s of the FDT t r a n s i t i o n s with the exce p t i o n of the l a s t two, which are combined i n t o a s i n g l e t r a n s i t i o n i n the FDT s p e c i f i c a t i o n . T h e a b b r e v i a t i o n s used i n t h i s s p e c i f i c a t i o n give a h i n t f o r the t r a n s l a t i o n of the s t a t e components. Note that here because V i > 0 ( a r ^ =ar ), the use of the s u f f f u n c t i o n i s compulsory in the s t a t e a b b r e v i a t i o n s . We now proceed to v e r i f y t h i s p r o t o c o l . Again i n the pr o o f s e'very term i s understood to be encl o s e d i n '[ ] ' . I. VERIFICATION OF THE ALT. BIT PROTOCOL 1 . ENTITY SAFETY The s a f e t y p r o p e r t i e s of each e n t i t y are given by the i n v a r i a n t s : 66 • us(a)=<u S i >1^ U)|_1 A sd(a)=<sd! > I^ U ) I _ 1 . <ra. > ! ^ U ) I ' 2 £ ra(a) < <ra. > l^ ( f f ) l _ 1 . saU)=<saT >{^ U ) I ' 1 • e i c s ( r d ( a ) )=<rd i > j ! ? o ( a ) ' ~ 1 A bs(a)=<b S i > j ^ U ) | _ 1 . br(a)=<br i > | ^ U ) | " 1 A ur<a)«<ur. > ! ^ U ) | " 1 (11 ) (12) (13) (14) (15) The f u n c t i o n e i c s i s to be d e f i n e d a f t e r the proof of 12, t1, s t a t e l These i n v a r i a n t s are analogous to the i n v a r i a n t s of the stop-wait p r o t o c o l , and t h e i r proofs are s i m i l a r to the pre v i o u s ones. We only give the proof of 12, f o r we co n s i d e r i t more c h a l l e n g i n g . Again, we denote by a, anext the sequence before and a f t e r a t r a n s i t i o n and by p r e ( t i ) the p r e c o n d i t i o n of t r a n s i t i o n i . Proof of 12 1. p r e ( t l ) A 12(a) o ra(o)=<vai > { U o ( a ) ' ~ 1 2. p r e ( t 1 ) A 12(a) D ra(cnext)=<ra. >|us(anext)|-2 s i n c e : |us(a)| = |us(anext)|- 1 3. p r e ( t l ) A 12(a) o 12(anext) o 0 ( l 2 ( a ) ) 4. p r e ( t 2 ) A 12(a) o ra(o)=<tai > } U o U ) ' " 2 5. p r e ( t 2 ) A 12(a) o ra ( a n e x t ) = < r a i > I U ^ U ) | " 1 s i n c e : I us(a) I = I us(anext) I and ra, / \ i . 1 1 1 1 j u s ( a ) j - 1 2, O-Int. t2, state2 67 6. p r e ( t 2 ) A 12(a) o I2(anext) o 0 ( I 2 ( a ) ) 5, O-Int. 7. p r e ( t i ) A 12(a) o 0 ( l 2 ( a ) ) f o r i=3 , • • , 1 s i n c e they don't change n e i t h e r us(a) nor r a ( a ) . 8. n ( l 2 ( a ) o 0 ( l 2 ( a ) ) ) 3,6,7, UTA, gen 9. 12(a) o n ( I 2 ( a ) ) 8,Th1 10. 12(a) s i n c e I2(X)=true. 1 1 . nI2(a) 9,10, mp Now we d e f i n e the s p e c i a l f u n c t i o n e i c s (events in c o r r e c t sequence) : DEF: I f a i s a sequence of events of the same kind then e i c s ( a ) i s d e f i n e d as : 1 . ( e i c s ( a ) ) Q = a Q 2. i f ( e i c s ( a ) ) ^ =a^ then ( e i c s ( a ) ) ^ + 1 =a^ where: k>j and seq(a, )=(seq(a. +l)mod2 and K 3 VI, j<l<k ( seq ( o-^ )=seq(a^ ) . I n f o r m a l l y , e i c s c o n t a i n s every event i n a which has a d i f f e r e n t sequence number from i t s predecessor and the order i s p r e s e r v e d . Using t h i s f u n c t i o n , and the i n v a r i a n t s we can deduce: 2. SYSTEM SAFETY Because we have a f u l l duplex channel, we must prove that t r a n s m i s s i o n i s s a f e to both d i r e c t i o n s . Here, we deal • | r a ( o ) | <|us(a)| = | e i c s ( s d ( a ) ) | <|ra(a)| +1 • | e i c s ( s a ( a ) ) | =|bs(a)| = | e i c s ( r d ( a ) ) | (16) (17) 68 only with the d i r e c t i o n E-->E'. The s a f e t y proof f o r the other d i r e c t i o n i s i d e n t i c a l . The s a f e t y of the system i s given by: • V n ( | u r ' U ' ) | =n o |us(a)| >n A (S1) Vi<n (data (ur !^  ) = data(us^ )) which s t a t e s that i f n messages have been d e l i v e r e d to the user of E', these are the f i r s t n messages send by the user of E, and the order i s preserved. Before p r o v i n g S1 we s h a l l prove some other p r o p e r t i e s needed i n S1 proof. F i r s t we want to prove: • | e i i c s ( r d ' ( a ' ) ) | < | e i c s ( s d ( a ) ) | < (S2) | e i c s ( r d ' ( a ' ) ) | +1 • |ra (a)| < | e i c s ( s a * ( a ' ) ) | <|ra(o)| +1 (S3) that i s , the number of messages (or acknowledgments) r e c e i v e d by one s i d e i s at l e a s t one l e s s than the number of d i f f e r e n t messages (or acknowledgments) sent by the other-s i d e . Proof of S2 1. | e i c s ( r d ' ( a ' ) ) | ^ | e i c s ( s d ( a ) ) | N1, N2, def e i c s 2. | e i c s ( s d ( a ) ) | <|ra (a)| +1 16 3. | r a ( o ) | < | e i c s ( s a * ( o ' ) ) | N1 ' , N2', def e i c s 4 . | e i c s ( s a ' ( a ' ) ) | = | e i c s ( r d ' ( a ' ) ) | 17 5. S2 1,2,3,4,<trans The proof of S3 i s s i m i l a r . Next, we want to prove: 69 • V n ( | e i c s ( r d ' ( a ' ) ) | =n o (S4) Vi<n(msg(rd^ )=msg(sd^ )) that i s , the i t h message r e c e i v e d by E' i s the i t h d i f f e r e n t message sent by E. We s h a l l prove i t by i n d u c t i o n on n. Note that i n i t i a l l y (n=0) i t i s t r u e . We suppose that i t i s true f o r n; then the i n d u c t i o n step i s : 1. | e i c s ( r d ' ( a ' ) ) | =n+1 Hyp 2. Vi<n(msg(rd^ )=msg(sd^ )) Hyp 3. n+1<|eics(sd(a))| <n+2 ' 1, S2 4. msg(rd^ )=msg(sd n ) V 2,3,N1 msg(rd^ )=msg(sd n + 1 ) 5. msg(rd^ )=msg(sd n ) Because Vn(n mod 2 * n+1 mod 2) 6. S4 1,2,5 The l a s t p r o p e r t y we need i s : • V n | u r ' ( o ' ) | =n o | b s ' ( a ' ) | >n A (S5) Vi<n(data(ur^ )=data(bs^ ) that i s , the i t h message d e l i v e r e d , i s the i t h message s t o r e d i n the b u f f e r . Proof of S5 1. |ur'U')| = n o | b r * ( a ' ) | =n A 15',def Vi<n(data(ur^ )=data(br^ )) ur,br 2. | u r ' ( f f ' ) | =n o | b s ' ( o ' ) | >n A 1,B1 Vi<n(data(ur^ )=data(bs! )) 70 F i n a l l y , we prove SI: Proof of S1 1. | u r ' U ' ) | =n o | b s ' ( a ' ) | ^n A Vi<n(data(urV )=data(bs! )) 2. | u r ' ( a ' ) | =n o | e i c s ( r d ' ( a ' ) ) | >n A Vi<n(data(ur^ )=data(rd^ )) 3. | u r ' ( a * ) | =n o | e i c s ( s d ( a ) ) | > n A Vi<n(data(ur^ )=data(sd i )) 4. SI 3. ENTITY LIVENESS The l i v e n e s s commitments of the e n t i t y are: • n o u s o n o s d • n o u s o V n ( | r a ( a ) | =n o ( n o s d V <>(|ra(a)| = h + l ) ) ) • n o r d A n o u q o Vn( | e i c s ( r d ( a ) ) | =n o <>(|bs(a)| >n) A ( n o s a 1 V o ( | e i c s ( rd( c;) ) | =n+1))) • n o r d A n o u q D n o s a • n o u q o (ob.r o < > u r | u r ( a ) | e a ^ • V k ( | r a ( a ) | =k A <>ra. o <>(|ra(a)| =k+D) S5 1 , 14', def bs,rd, o-Trans 2,S2,S4, o-Trans 3,11,def sd,us, o-Trans (C1 ) (C2) (C3) (C4) (C5) (C6) 71 • n o u q o Vk( | e i c s ( r d ( a ) ) | =k A <>rd k o (CI) < > ( | e i c s ( r d ( a ) ) | =k+l)) In the pr o o f s of these commitments, we need some p r o p e r t i e s deduced from the t r a n s i t i o n s , the system module and the UTA. These a r e : • i n ESTAB V i n ACK-WAIT (pO) • i n ESTAB 3 i n ESTAB U n t i l - A f t e r a t ( u s ) (p1) • i n ACK-WAIT o (p2) in ACK-WAIT U n t i l - A f t e r a t ( r a , , »• , ) |us\a) |- 1 • i n ACK-WAIT A ~ a t ( r a j u g ^ p ) | _ 1 ) 3 oTIMEOUT (p3) • |bs(a)| =n A B u f - n o t - f u l l 3 (p4) (|bs(a)| =n A B u f - n o t - f u l l ) U n t i l - A f t e r a t ( r d n ) • |bs(a)| =n o|bs ( a ) | =n U n t i l - A f t e r B u f - n o t - f u l l (p5) The f i r s t three are the same as i n the stop-wait p r o t o c o l , while the l a s t two come from the f a c t that |bs(o)| =n A B u f - n o t - f u l l A ~ a t ( r d n ) 3 0( |bs(a)| =n A B u f - n o t - f u l l ) , the UTA and A6. The p r o o f s of commitments C1,C2,C6 are s i m i l a r to the pr o o f s of T3, T4, T3' i n the p r e v i o u s example,and they are omitted. Here, we only prove C3 and C5. C4 comes from the f a c t t h a t , i f there are i n f i n i t e l y many incoming messages and the user i s always w i l l i n g to r e c e i v e (then the b u f f e r i s not f u l l ) , then one of the t r a n s i t i o n s t4, t5 i s enabled i n f i n i t e l y many times. C7 i s deduced from the f a c t that i f the b u f f e r i s not f u l l and the c o r r e c t message has a r r i v e d , 72 then i t w i l l e v e n t u a l l y be accepted. Proof of C3 1 . n o r d A n o u q 2. n o r d 3. n o B u f - n o t - f u l l 4. | e i c s ( r d ( a ) ) | =n o|bs ( a ) | =n 5. |bs ( a )| =n o <>(|bs (a)| >n) 6. |bs ( a ) | =n o <>(|bs (a )| =n A -B u f - n o t - f u l l ) 7. |bs( a )| =n D o n ( | b s ( a ) | =n A B u f - n o t - f u l l A ~ a t ( r d n )) V <>(|bs(a)|. =n A B u f - n o t - f u l l A a t ( r d n )) 8 . ] e i c s ( rd( a) ) | =n A n o r d o ( o n ( l b s ( o ) l =n A ~ a t ( r d )) A 1 1 n n o r d ) V (<>(|bs(o)| =n A B u f - n o t - f u l l A a t ( r d n ) ) A n o r d ) 9. | e i c s (rd( a)) | =n A n o r d o n o ( | b s ( a ) | =n A a t ( r d ^ where i#n)) V " <>(|bs(a)| =n A B u f - n o t - f u l l A a t ( r d n )) 1 0 . | e i c s (rd( o)) \ =n A n o r d o n o s a n _ 1 V <>( | e i c s ( r d ( o ) ) | =n+1) Hyp 1 , A E l i m 1, A E l i m , B5 14 p5,3,D4 6,p4,A8,D1, o Trans 4 , . . . , 7 , D Trans 8,E-Rule,Th21 9, t4, t 5 , 14 73 1 1 . C3 Proof of C5 1 . n o u q 2. n o b q 3. Buf-not-empty o A bq) 4. <>Buf-not-empty 5. <>Buf-not-empty C5 <>(Buf-not-empty o o b r o o u r 1,4,5,10, o to A Trans Hyp 1, E-Rule,t6 2, B3, D4 3, B2, D1 4, E-Rule, T7, Th2 1,5,D3 4. SYSTEM LIVENESS T h e - l i v e n e s s of the system i s expressed by: • n o s d A n o r d ' A n o s a ' A n o r a (L1 ) • V n ( | u r ' ( f f ' ) | =n o o | u r ' ( a ' ) | >n) (L2) The s t a r v a t i o n - f r e e c o n d i t i o n L1 can be deduced from U1,U2,C1,C4,N3,N3'. I t s proof i s i d e n t i c a l to L1 proof i n stop-wait p r o t o c o l . L2 expresses the f a c t that at any time the "next" message w i l l e v e n t u a l l y be d e l i v e r e d to the user of E'. Before proving L2, we prove that the b u f f e r s t o r e o p e r a t i o n s grow unboundedly, that i s : • V n ( | b s ' ( a ' ) | =n o o ( | b s ' ( a ' ) | >n)) (L3) Proof of L3 1. V i ( | r a ( a ) | =i o n o s d . V <>( U1,C2,mp | r a ( a ) | =i + D ) 2. V i ( | e i c s ( r d ' U ' )) | =i o <>(|bs' (a' ) | >i) A ( n o s a ! . , V <>( | e i c s ( r d ' (o'))\ = i + l ) ) ) 3. | b s ' ( a ' ) | =n o | e i c s ( r d ' ( a ' ) ) | =n 4. | b s ' ( a ' ) | =n o a o s a ^ V <>( j e i c s l r d ' (a') ) | =n+1 ) 5. | b s ' ( a ' ) | =n o | e i c s ( s a ' ( a ' ) ) | =n 6. |bs ' ( a ' ) | =n o n-1<|ra(a)| <n 7. n o s a ' , o o r a , n-1 n-1 8. |bs'U')| =n A n o s a ^ o <>(|ra(a ) | =n ) 9. |bs ' ( a ' ) | =n A n o s a ^ o n o s d V <>(|ra(o)| =n+1) n 1 1 10. n o s d o o r d ' n n 1 1 . | bs * ( a' ) | =n A n o s a ^ o ( n o s d o <>( l e i c s ( r d ' ( a ' ) ) I n 1 1 =n+1)) 12. <>(| ra (a )| =n+1) o < > ( | e i c s ( s a ' ( a ' ) ) | >n+1) 13. <> (|ra (a )| =n+l) o <>(|bs'(a')| >n+'1 ) 14. l b s ' ( a ' ) I =n A n o s a ' . o 1 1 n-1 <>(|bs'(a')| >n+1) L I , U2, C3', mp 17' 3,2,sub, A E l i m 17' 5, S3 N4' 6,7,C6 8,1,sub,D1, Th4, Th15, Th6 N4 9,10,3,C7' S3, D1 12, 17' 9,11,13, V I n t r . to A Trans 75 15. < > ( | e i c s ( r d ' ( a ' ) ) | =n+1) o <>(|bs'(a')| >n+1) 16. | b s ' ( a * ) | =n o <>(|bs*(a*)| >n+1) 17. L3 We now are ready to prove L2. Proof of L2 1. u r ' ( a ' ) | =n => b r ' ( a ' ) | =n 2. | u r ' ( a ' ) | = n D b s ' ( a ' ) | >n 3. u r ' ( a ' ) | =n 0 <>(|bs'(a')| >n) 4. | u r ' ( a ' ) | =n 0 <>Buf-not-empty' 5. | u r ' ( a ' ) | =n 0 <>(br') 6. | u r ' ( a ' ) | = n 0 <>(ur' ea) n 7. | u r ' ( a ' ) | =n 0 <>(|ur'(a')| >n) 8. L2 2,sub, A E l i m 4,14,15, V I n t r . , o to A Trans 16, gen 15 1, B1, D Trans 2, L3, o Trans 1,3,bf1 4, U2',B3', D4,B2,D1 5, U2', C5' 6, def a 7, gen V. CONCLUSIONS In t h i s t h e s i s , the meaning of the p r o t o c o l s p e c i f i c a t i o n and the most popular s p e c i f i c a t i o n methods were b r i e f l y d i s c u s s e d . In p a r t i c u l a r , three h y b r i d techniques, ISO/FDT, BBN/FST and UNISPEX, have been reviewd to some g r e a t e r extend and the A l t e r n a t i n g B i t P r o t o c o l was s p e c i f i e d i n each one of them f o r comparison reason. From t h i s review was concluded that the h y b r i d models, while o f f e r a great e x p r e s s i v e power and are c l o s e to the implementation l e v e l , most of them (except UNISPEX) do not pro v i d e the means f o r v e r i f i c a t i o n of the s p e c i f i e d p r o t o c o l . In order to apply such v e r i f i c a t i o n , the " t r a n s l a t i o n " of the h y b r i d s p e c i f i c a t i o n to some other model i s necessary. Such t r a n s l a t i o n was o u t l i n e d i n chapter I I I . An ISO/FDT s p e c i f i c a t i o n was taken and i t was " t r a n s l a t e d " i n t o an unbounded s t a t e temporal l o g i c . Even though t h i s v e r i f i c a t i o n i s not complete, i t r e v e a l e d that temporal l o g i c i s very promising i n p r o v i n g the l i v e n e s s p r o p e r t i e s of a system but somehow poor i n i n v a r i a n t p r o o f s . F i n a l l y , i n chapter IV a new method f o r the s p e c i f i c a t i o n and v e r i f i c a t i o n of p r o t o c o l s was proposed, c a l l e d SETL. Two data t r a n s f e r p r o t o c o l was s p e c i f i e d and v e r i f i e d i n SETL: a stop-wait p r o t o c o l and a v e r s i o n of the a l t e r n a t i n g b i t p r o t o c o l . The l a s t example r e v e a l e d how the method can be used f o r s p e c i f y i n g a b s t r a c t data types as w e l l . SETL, although i t uses the temporal l o g i c as the 76 77 s p e c i f i c a t i o n language, i t i s very s i m i l a r to the ISO/FDT. The t r a n s l a t i o n between these two methods i s simple enough to be automated. SELT can be viewed as an a b s t r a c t i o n of any t r a n s i t i o n o r i e n t e d technique. I t supports i n v a r i a n t , as w e l l as, l i v e n e s s p r o o f s . We c l a i m that any property of a p r o t o c o l s p e c i f i e d in SETL, can be proved by using i t s axiomatic system. We b e l i e v e t h a t , i f the method becomes more formal, a semi-automated v e r i f i c a t i o n t o o l can be implementable. We accept that the v a l i d a t i o n of a temporal formula (or even f i r s t order formula), i s an NP-complete problem. What we propose here i s a v e r i f i c a t i o n t o o l , s i m i l a r to AFFIRM, i n which the p r o o f s are guided by the user. I t i s c l e a r that i n v a r i a n t p r o o f s can be automated. The s i m i l a r i t y of the l i v e n e s s proofs f o r the given examples i n d i c a t e that i f some more compact d e r i v e d r u l e s c o u l d be invented and a formal axiomatic system f o r the event sequences c o u l d be p r o v i d e d , semi-automation c o u l d be r e a l i z a b l e . We delay purposely these a d d i t i o n s u n t i l we have some experience i n using SETL to s p e c i f y a connection o r i e n t e d p r o t o c o l . REFERENCES [Ansart83] J . Ansart, V. C h a r i , M. Neyer, 0. R a f i q , D. Simon, "Description, S i m u l a t i o n and Implemenat ion of P r o t o c o l s using PDIL", Proc. ACM SIGCOMM Conf., p101 - 120, Mar 1983. [Ansart82] J . Ansart, 0. R a f i q , V. C h a r i , " P r o t o c o l D e s c r i p t o n and Implementation Language", P r o t o c o l S p e c i f i c a t i o n T e s t i n g and V e r i f i c a t i o n , Sunshine(ed.), North-Holland, 1982, pi 01 - 112. [Ben80] M. Ben, "Temporal L o g i c Proofs of Concurrent Programs",ACM TOPLAS, 1980. [Be r t h e l o t 8 2 ] G. B e r t h e l o t , R. T e r r a t , " P e t r i Nets Theory f o r the Cor r e c t n e s s of P r o t o c o l s " , Prot. Spec. T e s t . Ver., Sunshine(ed.), North-Holland, 1982, p43-62. [ B i l l i n g t o n 8 2 ] J . B i l l i n g t o n , " S p e c i f i c a t i o n of the Transport S e r v i c e using Numerical P e t r i Nets", P r o t . Spec. T e s t . Ver., Sunshine(ed.), North-Holland, 1982, p77-100. [Blumer82a] T. Blumer, J . Burrus, "Generating a S e r v i c e S p e c i f i c a t i o n of a Connection Management P r o t o c o l " , P r o t . Spec. T e s t . Ver., Sunshine(ed.), North-Holland,1982, p161 - 170 . [Blumer82] T. Blumer, R. Tenney, "A Formal S p e c i f i c a t i o n Technique and Implementation Method f o r P r o t o c o l s " , Computer Networks, V6, 1982, p 2 0 l - 2 l 7 . [Bochmann78] G. Bochmann, " F i n i t e State D e s c r i p t i o n of Communication P r o t o c o l s " , Computer Networks, V2, 1978, P361-372. [Bochmann80] G. Bochmann, "A General T r a n s i t i o n Model f o r P r o t o c o l s and Communication S e r v i c e s " , IEEE Trans, on Comm., V28, N4, Apr. 1980, p643-650. [Bochmann82] G. Bochmann, K. Raghunathan, "Example D e s c r i p t i o n of the Transport S e r v i c e " , C o n t r i b u t i o n to the meeting of the Subgroup B of the ISO TC97/SC16/WG1 ad hoc group on FDT, Jun 1982. [Bochmann80a] G. Bochmann, C. Sunshine, "Formal Methods i n Communication P r o t o c o l Design", IEEE Trans. on Comm., V28, N4, Apr 1980, p624-631. [Bochmann82a] G. Bochmann, E. Cerny, M. Gagne, C. J a r d , A. L e v e i l l e , C. L a c a i l l e , M. Maksud, K. Raghunathan, B. Sa r i k a y a , "Some Experience with the Use of Formal 78 79 S p e c i f i c a t i o n s " , P r o t . Spec. T e s t . Ver., Sunshine(ed.), North-Holland 1982, p171-185. [Clipsham76] W. Clipsham, M. Narraway, "Datapac Network Overview ", T h i r d I n t r n . Conf. on Comp. Comm., Toronto, Canada, Aug. 1976. [ D i V i t o 8 2 ] - — B . D i V i t o , " I n t e g r a t e d Methods f o r P r o t o c o l S p e c i f i c a t i o n and V e r i f i c a t i o n " , P r o t . Spec. T e s t . Ver., Sunshine(ed.), North-Holland, 1982, p411-433. [Gouda78] M. Gouda, E. Manning, "How to D e s c r i b e P r o t o c o l s " , U n i v e r s i t y of Waterloo CCNG E-Report E-76, Mar. 1978. [Hailpern80] B. H a i l p e r n , " V e r i f y i n g Concurrent Processes Using Temporal L o g i c " , PhD T h e s i s , T e c h n i c a l Report 195, Computer Systems Laboratory, S t a n f o r d Univ., Aug. 1980. [Hailpern80a] B. H a i l p e r n , S. Owicki, " V e r i f y i n g Network P r o t o c o l s Using Temporal L o g i c " , NBS Treds and Appl. Symp. May 1980, pl8-28. [ H a i l p e r n 8 l ] B. H a i l p e r n , S. Owicki, "Modular V e r i f i c a t i o n of Computer Communication P r o t o c o l s " , IBM Recearch Report RC 8726, 1981 . [Hoare78] C. Hoare, "Communicating S e q u e n t i a l Processes", CACM, Aug. 78, V21 N8, p666-677. [IS081] DIS 7499, "Data P r o c e s s i n g Systems - Open Systems I n t e r c o n n e c t i o n - Basic Reference Model", Computer Networks 5,1981, p81-118. [ l S 0 8 l a ] ISO, "A FDT based on an Extended State T r a n s i t i o n Model", Working D r a f t , Boston, Dec.1981. [IS082] ISO, "Reference Model of Open System I n t e r c o n n e c t i o n " , ISO/TC97/SC16, D r a f t ISO/DIS 7498, 1982. [IS084] ISO TC97/SC16/WG1 Subgroup B, "A FDT Based on an Extended S t a t e T r a n s i t i o n Model", March 1984. [Kurose82] J . Kurose, Y. Yemini, "The S p e c i f i c a t i o n and V e r i f i c a t i o n of a Connection Establishment P r o t o c o l Using Temporal L o g i c " , P r o t . Spec. T e s t . Ver., Sunshine(ed.), North-Holland 1982, p43~62. [Landw82] L. Landweber, M. Solomon, "The Use of M u l t i p l e Networks i n CSNET", Proc. of Compcon Spr i n g 1982. [Manna8L] Z. Manna, A. P n u e l i , " V e r i f i c a t i o n of Concurrent Programs, Part I I : Temporal Proof P r i n c i p l e s " , T e c h n i c a l Report CS-81-843, Computer Science, S t a n f o r d Univ. 1981. 80 [Manna8la] Z. Manna, P. Wolper, "Synth e s i s of Communicating Processes from Temporal Log i c S p e c i f i c a t i o n s " , T e c h n i c a l Report CS-81-872, Computer Science, S t a n f o r d Univ, 1981. [McQuillan77] J . M c Q u i l l a n , D. Walden "The ARPA Network Design D e c i s i o n s " , Computer Networks 1, 1977,p243-289. [Owicki82] S. Owicki, L. Lamport, "Proving L i v e n e s s P r o p e r t i e s of Concurrent Programs", ACM Trans on Prog. Lang. 4,1982, p455~495. [Pnueli77] A. P n u e l i , "The Temporal Logic of Programs", The 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode I s l a n d , IEEE 1977, p46-57. [Pnueli79] A. P n u e l i , "The Temporal Semantics of Concurrent Programs", The I n t e r n a t i o n a l Symposium on the Semantics of Concurrent Computation, E v i a n , J u l y 1979. [Pouzin82] L. Pouzin, "The Cyclades Network", Monograph S e r i e s of the I n t e r n a t i o n a l C o u n c i l f o r Computer Communications, V2, North-Holland, 1982. [Rudin78] H. Rudin, C. West, P. Z a f i r o p u l o , "Automated P r o t o c o l V a l i d a t i o n : One Chain of Development", Computer Networks, V2, 1978, p373-380. [Schwarts82] R. Schwarts, P. M e l l i a r - S m i t h , "From State Machines to Temporal L o g i c : S p e c i f i c a t i o n Methods for P r o t o c o l Standards", P r o t . Spec. T e s t . Ver., Sunshine(ed.), North-Holland, 1982. [Schwartz83] R. Schwarts, P. M e l l i a r - S m i t h , F. Vogt, " I n t e r v a l Logic:A H i g h e r - L e v e l Temporal Log i c f o r P r o t o c o l S p e c i f i c a t i o n " , P r o t . Spec. T e s t , Ver, North-Holland 1983, p3-17. [Schwabe8l] D. Schwabe, "Formal Techniques f o r the S p e c i f i c a t i o n of P r o t o c o l s " , PhD T h e s i s , U n i v e r s i t y of C a l i f o r n i a , Los Angeles 1981. [Sidhu83] P. Sidhu, "Protocol* V e r i f i c a t i o n v i a Executable L o g i c S p e c i f i c a t i o n s " , P r o t . Spec. T e s t . Ver., Radin, WesUeds.), North-Holland, 1983, p237-248. [Sunshine82] C. Sunshine, D. Thompson, R. E r i c k s o n , S. Gerhart, D. Schwabe, " S p e c i f i c a t i o n and V e r i f i c a t i o n of Communication P r o t o c o l s i n AFFIRM using S t a t e T r a n s i t i o n Models", IEEE Trans, on S o f t . Eng., V8 N5 1982, p460-489. [Vogt82] F. Vogt, "Event-Based Temporal Log i c S p e c i f i c a t i o n s of S e r v i c e s and P r o t o c o l s " , P r o t . Spec. T e s t . Ver., Sunshine(ed.), North-Holland, 1982. 81 [Vuong82] S. Vuong, D. Cowan, "UNISPEX - A U n i f i e d Model f o r P r o t o c o l S p e c i f i c a t i o n and V e r i f i c a t i o n " , U n i v e r s i t y of Waterloo T e c h n i c a l Report CS-82-52, Nov. 1982, or, INFOCOM Conference, San F r a n c i s c o , A p r i l 1984. [Vuong83] S. Vuong, D. Cowan, "Automated P r o t o c o l V a l i d a t i o n V i a R e s y n t h e s i s : The X.75 Packet L e v e l as an Example", J o u r n a l of Telecommunication Networks, Summer Issue, 1983. [ Z a f i r o p u l o 7 9 ] P. Z a f i r o p u l o , H. Rudin, D. Cowan, "Towards S y n t h e s i z i n g Synchronous Two Process I n t e r a c t i o n s " , IEEE-NBS Computer Networking Symposium, 1979, p.169-175. [ Z a f i r o p u l o 8 2 ] P. Z a f i r o p u l o , C. West, H. Rudin, D. Cowan,D. Brand, " P r o t o c o l A n a l y s i s ans S y n t h e s i s Using a State T r a n s i t i o n Model", Computer Network A r c h i t e c t u r e s and P r o t o c o l s , 1982. APPENDIX 1 A l t e r n a t i n g B i t P r o t o c o l S p e c i f i c a t i o n i n BBN's FST { D e c l a r a t i o n s } const retran-time=10; { r e t r a n s m i s s i o n time} empty=0; {buffer empty} null=0; { n u l l data} type id-type=(DATA,ACK); { p r o t o c o l data units} t i m e r - t y p e = ( r e t r a n s m i t ) ; ndata-tupe=record { p r o t o c o l data u n i t s t r u c t u r e } i d : i d - t y p e ; data :data-type; seq :seq-type end; msg-type=record {message s t r u c t u r e } msgdata :data-type; msgseq :seq-type end; machine=record { e n t i t y c o n t r o l s t r u c t u r e } send-seq :seq-type; recv-seq :seq-type; send-buffer : b u f f e r - t y p e ; r e c v - b u f f e r : b u f f e r - t y p e ; send-msg :msg-type; recv-msg :msg-type end; var ecs rmachine; {code has i m p l i e d "with ecs do"} i n t e r f a c e [ f r o m U:SEND.request( UData:data-type ) ] ; i n t e r f a c e [ f r o m U:RECEIVE.request]; i n t e r f a c e f t o U:RECEIVE.response( UData:data-type ) 3 ; i n t e r f a c e [ t o N:DATA.request( NData:ndata-type ) ] ; i n t e r f a c e f t o S:TIMER.request( Name:timer-type; Time:int-type ) ] ; i n t e r f a c e [ f r o m S:TIMER.response( 82 83 Name:t i m e r - t y p e ) ] ; s t a t e either=(ACK-WAIT,ESTAB); i n i t i a l = E S T A B ; final=NONE; p r e d i c a t e Ack-OK; b e g i n ( [ f r o m N:NData.id]=ACK)and ( [ f r o m N:NData.seq]=send-seq) end; pr o c e d u r e p r o c e d u r e f u n c t i o n p r o c e d u r e p r o c e d u r e p r o c e d u r e p r o c e d u r e p r o c e d u r e f u n c t i o n f u n c t i o n p r o c e d u r e beg i n send r e c v send r e c v end; s t o r e ( b u f : b u f f e r - t y p e ; m s g : m s g - t y p e ) ; r e m o v e ( b u f : b u f f e r - t y p e ; i s e q : s e q - t y p e ) ; r e t r i e v e ( b u f : b u f f e r - t y p e ) : m s g - t y p e ; i n c r - s e n d - s e q ; i n c r - r e c v - s e q ; send-data (msg:msg-type); send-ack (msg:msg-type); d e l i v e r - d a t a ( m s g : m s g - t y p e ) ; n e t - d a t a ( m i d : i d - t y p e ; mseq:seq-type; mdata:data-type) : n d a t a - t u p e ; buf f e r - e m p t y ( b u f : b u f f e r - t y p e ) : b o o l e a n ; i n i t i a l i z e - m a c h i n e ; - s e q : = 0 ; -seq: = 0 ; -buf fer:=empty; -buf fer:=empty; pr i m i t i v e ; p r i m i t i v e ; p r i m i t i v e ; f o r w a r d ; f o r w a r d ; f o r w a r d ; f o r w a r d ; f o r w o r d ; pr i m i t i v e ; pr i m i t i v e ; { T r a n s i t i o n s } <ACK-WAIT> < <ESTAB> [f r o m U:SEND.request] b e g i n send-msg.msgdata:=[from U:UData]; send-msg.msgseq;=send-seq; s t o r e ( s e n d - b u f f e r , s e n d - m s g ) ; send-data(send-msg); [ t o S:TIMER.request(Name:=retransmit, T i m e : = r e t r a n - 1 i m e ) ] ; end; <ACK-WAIT> < <ACK-WAIT> [from S:TIMER.response] ( [ f r o m S:Name]=retransmit) b e g i n send m s g : = r e t r i e v e ( s e n d - b u f f e r ) ; send-data(send-msg); [ t o S:TIMER.request(Name:=retransmit, T i m e : = r e t r a n - t i m e ) ] ; end; 84 <ESTAB> < <ACK-WAIT> [from N:DATA.response] (Ack-OK). begin remove(send-buffer,[from N: NData.seq]); incr- s e n d - s e q ; end; <same-state> < <either> [from N:DATA.response] ([from NrNData.id]=DATA) begin (always ACK data; s t o r e i f expected sequence number} recv-msg.msgdata:=[from NrNData.data]; recv-msg.msgseq:=[from N:NData.seq]; send-ack(recv-msg); i f [from NrNData.seq]=recv-seq then begin s t o r e ( r e c v - b u f fer,recv-msg); i n c r - r e c v - s e q ; end; end; <same-state> < <either> [from U:RECEIVE.request] (not b u f f e r - e m p t y ( r e c v - b u f f e r ) ) begin r e c v - m s g : = r e t r i e v e ( r e c v - b u f f e r ) ; d e l i v e r - d a t a ( r e c v - m s g ) ; remove(recv-buf fer,recv-msg.msgseq); end; procedure i n c r - r e c v - s e q ; begin recv-seq:=(recv-seq+1)mod 2; end; procedure send-data(msg:msg-type); begin [t o N:DATA.request ( NData:=net-data(DATA,msg.msgseq, msg.msgdata)]; end; procedure send-ack(msg:msg-type); begin [to N:DATA.request( NData:=net-data(ACK, msg.msgseq, n u l l ) ) ] ; end; procedure deliver-data(msg:msg-type); begin [to U:RECEIVE.response(UData:=msg.msgdata)]; end; { D e s c r i p t i o n of P r i m i t i v e Procedures} 8 5 procedure s t o r e ( b u f : b u f f e r - t y p e ; msg:msg-type); p r i m i t i v e ; I t s t o r e s the s p e c i f i e d message in the s p e c i f i e d b u f f e r . procedure remove(buf:buffer-type; i s e q : s e q - t y p e ) ; p r i m i t i v e ; Remove the given message from the s p e c i f i e d b u f f e r . f u n c t i o n r e t r i e v e ( b u f : b u f f e r - t y p e ) : m s g - t y p e ; p r i m i t i v e ; R e t r i e v e the f i r s t message from the s p e c i f i e d b u f f e r . f u n c t i o n net-data(msgid:id-type; mseq:seq-type; mdata:data-type):ndata-type; p r i m i t i v e ; C o n s t r u c t a p r o t o c o l data u n i t from the s p e c i f i e d data, sequence number and i d e n t i f i e r . f u n c t i o n b u f f e r - e m p t y ( b u f : b u f f e r - t y p e ) : b o o l e a n ; p r i m i t i v e ; Returns t r u e i f the s p e c i f i e d b u f f e r i s empty. APPENDIX 2 A l t e r n a t i n g B i t P r o t o c o l S p e c i f i c a t i o n i n FDT c o n s t r e t r a n - t i m e = . . . ; empty=...; n u l l = . ..; t y p e d a t a - t y p e = . . . ; s e q - t y p e = . . . ; i d - t y p e = ( D A T A , ACK); t i m e r - t y p e = ( r e t r a n s m i t ) ; n d a t a - t y p e = r e c o r d i d : i d - t y p e ; d a t a : d a t a - t y p e ; seq : s e q - t y p e end; m s g - t y p e = r e c o r d d a t a : d a t a - t y p e ; s e q : s e q - t y p e end; buf f e r - t y p e = . . . ; (*Channel d e f i n i t i o n s * ) C h a n n e l E n t i t y U s e r ( U s e r , P r o v i d e r ) ; By U s e r : S E N D - r e q u e s t ( U D a t a : d a t a - t y p e ) ; R E C V - r e q u e s t ( ) ; By P r o v i d e r : R E C V - r e s p o n s e ( U D a t a : d a t a - t y p e ) ; C h a n n e l E n t i t y N e t w o r k ( U s e r , P r o v i d e r ) ; By U s e r : D A T A - r e q u e s t ( N D a t a : n d a t a - t y p e ) ; By P r o v i d e r : D A T A - r e s p o n s e ( N D a t a : n d a t a - t y p e ) ; C h a n n e l E n t i t y S y s t e m ( U s e r , P r o v i d e r ) ; By U s e r : TIMER-request(Name : t i m e r - t y p e ; Time : i n t ) ; By P r o v i d e r : TIMER-response(Name:t i m e r - t y p e ) ; (*Module d e f i n i t i o n s * ) Module A B P - e n t i t y ( U : E n t i t y U s e r ( P r o v i d e r ) ; N : E n t i t y N e t w o r k ( U s e r ) ; S : E n t i t y S y s t e m ( U s e r ) ) ; 86 87 var send-seq : seq-type; recv-seq : seq-type; send-buf : b u f f e r - t y p e ; recv-buf : b u f f e r - t y p e ; send-msg : msg-type; recv-msg : msg-type; S t a t e s e t (ESTAB, ACK-WAIT); procedure i n c r - s e n d - s e q ; (* Same as before *) procedure i n c r - r e c v - s e q ; (* " " " *) f u n c t i o n n e t - d a t a ( i d : i d - t y p e ; seq:seq-type; data:data-type : ndata-type; begin ... end; procedure send-data(msg:msg-type); begin out N.DATA-request(net-data(DATA, msg.seq, msg.data ) ) ; end; procedure send-ack(msg:msg-type); begin out N.DATA-request(net-data(ACK, msg.seq, n u l l ) ) ; end; (*Buffer f u n c t i o n s same as i n FST*) i n i t i a l i z e begin state:=ESTAB; send-seq:=0; recv-seq:=0; c l e a r ( s e n d - b u f ) ; c l e a r ( r e c v - b u f ) ; end; (* T r a n s i t i o n s *) from ESTAB when U.SEND-request(UData) to ACK-WAIT begin send-msg.data:=UData; send-msg.seq:=send-seq; store(send-buf, send-msg); send-data(send-msg); out S.TIMER-request(retransmit, r e t r a n - t i m e ) ; end; from ACK-WAIT 88 when S.TIMER-response(Name) pr o v i d e d Name=retransmit to same begin send-msg:=retrieve(send-buf); send-data(send-msg); out S.TIMER-request(retransmit, r e t r a n - t i m e ) ; end; when N.DATA-response(NData) p r o v i d e d NData.id=ACK and NData.seq=send~seq to ESTAB begin remove(send-buf, NData.seq); incr-send-seq; end; from ESTAB, ACK-WAIT when N.DATA-response(NData) pro v i d e d NData.id=DATA to same begin recv-msg.data:=NData.data; recv-msg.seq:=NData.seq; send-ack(recv-msg); i f NData.seq=recv-seq then begin s t o r e ( r e c v - b u f , recv-msg); i n c r - r e c v - s e q ; end end; when U.RECV-request() pro v i d e d not empty(recv-buf) to same begin recv-msg:=retr i e v e ( r e c v - b u f ) ; out U.RECV-response(recv-msg.data); remove(recv-buf, recv-msg.seq); end; A l t e r n a t i n g APPENDIX 3 B i t P r o t o c o l U N I S P E X i f i c a t i o n PROTOCOL MACHINE (ABPStation) D e c l a r a t ion Needs[Integer,Boolean,Bit,SequenceType,Message, QueueOfMessage] Type Request[DATA, ACK, n u l l ] , T i m e r T y p e f r e t r a n s m i t , n u l l ] , SystResponse[timeout, n u l l ] ; V a r i a b l e s [ S t a t e :: S t a t e : [ESTAB, ACK-WAIT, ESTAB1, ACK-WAIT1], SendBuf, RecvBuf : QueueOfMessage, Sent,Received : QueueOfMessage, VS, VR : SequenceType, Pending : Boolean; I n t e r f a c e : : MsgToSend, MsgReceived, MsgToDeliver : Message, SS, SR : SequenceType, Cmd : [send, r e c e i v e , n u l l ] , Timer : SystResponse; Channel :: InReq, OutReq : Request, InChannel, OutChannel : QueueOfMessage; I n i t i a l S t ate [ state:=ESTAB and Cmd:=null and InReq:=OutReq:=null and Sent:=Received:=empty and SendBuf:=RecvBuf:=empty and Pending:=false and VS:=VR:=0 and InChannel:=OutChannel:=empty and Timer:=null; ] I n t e r f a c e s S e r v i c e P r i m i t i v e s [ Send(UData:Message) when (Cmd=null and Pending=false) [ Cmd:=send; MsgToSend:=UData; ] 89 9 0 Receive(UData:Message) when (Cmd=null and RecvBuf o=empty) [ Cmd:=receive when (Cmd=null) [ UData:=MsgToDeliver ]; ] ] P r i m i t i v e s [ ToNet(Type:Request; Seq:SequenceType; Msg:Message) FromNet(Type:Request; Seq:SequenceType; Msg:Message) /* System P r i m i t i v e s */ TimerRequest(Name:TimerType; Time:Integer) TimerResponse(Name:TimerType) ] Mapping Events [ SendMsg when (OutReq o=null) [ ToNet(OutReq, SS, MsgToSend); OutReq:=null; ] MsgReceive when (InReq=null and FromNet(Type,Seq,Msg)) [ InReq:=Type; SR:=Seq; MsgReceived:=Msg; ] MsgLost when (InReq=null and FromNet(Type,Seq,Msg)) [ InChannel:=Remove(InChannel); ] /* One of the l a s t two events can be executed at each time. I f one i s executed the other i s excluded. */ SetTimer when (OutReq=DATA) [ Timer:=null; TimerRequest(retransmit,TC); ] TimerResponse when (TimerResponse(retransmit)) [ Timer:=timeout; ] Events [ SendData /-DATA/ ESTAB > ACK-WAIT when (Cmd=send and OutReq=null) [ Sent:=Add(Sent, MsgToSend); OutChannel:=Add(OutChannel, MsgToSend); Pending:=true; SS:=VS; OutReq:=DATA; Cmd:=null; ] ReceiveData /+DATA/ ESTAB > ESTAB1 or ACK-WAIT > ACK-WAIT1 when (InReq=DATA and SR=VR) [ Received:=Add(Received, MsgReceived); InChannel:=Remove(InChannel); RecvBuf:=Add(RecvBuf, MsgReceived); VR:=Increment(VR); ] R e c e i v e D u p l i c a t e /+DATA/ ESTAB > ESTAB1 or ACK-WAIT > ACK-WAIT1 When (InReq=DATA and SR o=VR) [ InChannel:=Remove(InChannel); 3 Timeout / timeout / ACK-WAIT > ACK-WAIT When (Timer=timeout and Pending=true and OutReq=null) [ MsgToSend:=Retrieve(SendBuf); SS:=VS; OutChannel:=Add(OutChannel, MsgToSend); OutReq:=DATA; 3 SendAck / -ACK / ESTAB1 > ESTAB or ACK-WAIT1 > ACK-WAIT When (OutReq=null and InReq=DATA) [ SS:=SR; MsgToSend:=empty; OutReq:=ACK; InReq:=null; 3 ReceiveAck /+ACK/ ACK-WAIT > ESTAB When (InReq=ACK and SR=VS.) [ VS:=Increment(VS); Pending :=false; SendBuf:=Remove(SendBuf); InReq:=null; 3 D e l i v e r D a t a / n u l l / ANY > SAME When (Cmd=receive and RecvBufo=empty) [ MsgToDeliver:=Remove(RecvBuf); Cmd:=null; 3 TOPOLOGY [ Instances S t a t i o n : A r r a y ( S i d e ) of ABStation Connect ions S t a t i o n ( i ) . O u t R e q <--->-Station(OppSide(i)).InReq S t a t i o n ( i ) . O u t C h a n n e l < > S t a t i o n ( O p p s i d e ( i ) ) . I n C h a n n e l ; PROPERTIES [ /* Messages are r e c e i v e d i n c o r r e c t order */ S e n t ( i ) = i f ( P e n d i n g ( i ) = f a l s e ) then R e c e i v e d ( O p p S i d e ( i ) ) e l s e Append(Received(OppSide(i)) , SendBuf(i) LengthdnChannel ( i ) ) <= 1; ] APPENDIX 4 Axioms and Derived Rules of Standard L o g i c A L A If l-B If [T F If If If I f If If If If If If If (Ao then A f-B and A f-B ~A (-B then f-B (-A then f-AVB A(-C and B|-C and [-AVB then |-C -A and |-B then |-AAB -AAB then f-A A |-B then f-AoB |-A and |-AoB then |-B A(-B and A(-~B then (-~A A then |- A A then |-A AoB and (-BoA then (-A=B A=B then |-AoB B o O ) = ((AAB)oC) ((AVB)A(~A)) o B ((AoB)A(~B)) o (~A) ((AoC)A(BoC)) = ((AVB)oC) ((AoB)A(BoC)).o (AoC) ((A=B)A(B=C)) o (A=C) (AoB) = (~AVB) ~(AVB) = (~AA~B) "(AAB) = (~AV~B) (AoB) = (~Bo~A) (AAB) = (BAA) (AVB) = (BVA) (A^B) = (B^A) Assump Axiom Assump I n t r o Assump E l i m T Axiom F Axiom V I n t r V E l i m A I n t r A E l i m o I n t r o E l i m ~ I n t r ~~ I n t r E l i m = I n t r = E l i m o to A Trans V E l i m o E l i m Proof by Cases o Trans = Trans o to V Trans DM DM' CP A Commut V Commut = Commut 93 APPENDIX 5 The Temporal L o g i c System AXIOMS A1. n(poq)o(nponq) A2. O(poq)o(OpoOq) A3. npopAOpAOnp A4. np= <>~p A5. ~Op=0~p A6. n(pA~qoOp)o(pop U n t i l - A f t e r q) A7. p U n t i l q = q V (p A 0(p U n t i l q)) A8. p U n t i l q o n(p A ~q) V <>q A9. p U n t i l - A f t e r q = p U n t i l (p A q) INFERENCE RULES R1, ( t a u t ) . I f p i s a ( s u b s t i t u t i o n of a) p r o p o s i t i o n a l t a u t o l o g y then |-p. R2, (mp) . I f |-p and |-poq then |-q. R3, (gen). I f |-p then (-ap. DERIVED RULES D1 . I f k> then f-Mp where M i s n or <> or 0 D2. If [poq then |- MpoMq D3. If p|-q then |-npoq. Deduction theorem (ded) D4. If |- p 3 (p U n t i l - A f t e r q) and |-<>q then \- p o <>(pAq) (U-<> Rule) D5. If (- p o (p U n t i l - A f t e r q) and |- A ~q o o r then (- p o n o ( p A r ) V o ( p A q ) ( U - n o Rule) D6. If [• p o (p U n t i l - A f t e r q) and |- n~q then [• p D n(pA~q) (U~n Rule) THEOREMS Th1. n(poOp) o (ponp) Th2. Op o o p Th3. n(p A q) = np A nq Th4. <>(p V q) = o p V <>q Th5. nnp = np Th6. o o p = o p Th7. 0(p A q) = Op A Oq Th8. Op V oq = 0(p V q) Th9. <>(p A q) o o p A o q ThlO. np V nq o n(p V q) Th11. p A Onp = np 94 95 Th1 2. o p = p V O o p Th13. n((p V nq) A (q V np)) = np V nq Th14. o n p = n o n p T h l 5 . n o p = o n o p Th16. o p A nq o <>(p A nq) Th17. o n p A nq o o n ( n p A nq) Th l 8 . o n p A o n q o o n ( n p A nq) T h l 9 . n o ( p V q) o n o p V n o q Th20. n o p A nq o n o ( p A nq) Th21. n o p A o n q o n o ( p A nq) Th22. (p o q) U n t i l r o (p U n t i l r D q U n t i l r) Th23. p U n t i l q o (~q U n t i l r o p U n t i l r) Th24. p U n t i l (q A r) o (p U n t i l q) U n t i l r Th25. 0(p U n t i l q) o (Op) U n t i l (Oq) APPENDIX 6 SETL S p e c i f i c a t i o n of the Stop-Wait P r o t o c o l type data-type=...; seq-type=0...; id~type=(DATA,ACK) ; (* Channel d e f i n i t i o n s *) Channel U s e r T r a n s m i t t e r ( U s e r , P r o v i d e r ) ; By User: SENDreq(d:data-type); By P r o v i d e r : SENDack; Channel U s e r R e c e i v e r ( U s e r , P r o v i d e r ) ; By P r o v i d e r : R E C E I V E i n d i c ( d : d a t a - t y p e ) ; Channel EntityNetwork(User, P r o v i d e r ) ; By User: SEND(id:id-type, d:data-type, seq:seq-type); By P r o v i d e r : RECEIVE(id:id-type,d:data-type, seq:seq-type); Channel System T r a n s m i t t e r (User, P r o v i d e r ) ; By User: STARTTIMER; STOPTIMER; By P r o v i d e r : TIMEOUT; (* A b b r e v i a t i o n s used i n t h i s s p e c i f i c a t i o n * ) us(o) = P(a, SENDreq), us i = SENDreq(d ^ ), and us=any SENDreq. ua(a)=P(a,SENDack), ua=any SENDreq. ur ( a) =P( a, RECEIVEindic ) , ur^ =RECEIVEindic (b^^ ), ur=any u r i sd(a)=P(a,[SEND, where id=DATA]), 96 97 s d i = SEND(DATA,d^ , i ) and sd=any sd^ rd(a)=P(a,[RECEIVE,where id=DATA]), r d ^ =RECEIVE(DATA, , i ) and rd=any rd^ sa(o)=P(a,[SEND,where id=ACK]), sa i =SEND(ACK,-,i) and sa=any sa^ ra(a)=P(a,[RECEIVE, where i d = A C K ] ) , ra i =RECEIVE(ACK,-,i) and ra=any r a ^ in ESTAB = [a1=X] V t r a | u s ( a ! ) | _ 1 e < 7 1 3 ( s t a t e l ) i n ACK-WAIT = [a1*A] A [ r a | u s ( a 1 ) | - •] ] ( s t a t e 2 ) (* Module d e f i n i t i o n s *) Module T r a n s m i t t e r ( U s e r T r a n s m i t t e r ( P r o v i d e r ) ; EntityNetwork(User)) SES : a1=[us,ua,sd,ra,STARTTIMER,STOPTIMER,TIMEOUT] T r a n s i t i o n Semantics: • i n ESTAB A [ol=o0] A [ a t ( u s ) ] o ( t l ) 0 ( i n ACK-WAIT A [a1=a0<us, / r, \ i > |us(aO)I < S d | u s ( a O ) | ,STARTTIMER>] A [ s d | u s ( a O ) | ] A f STARTTIMER]) • i n ACK-WAIT A [o,=o0] A t a t < r a | u s ( a n ) | - 1 ^ 0 ( t 2 ) 0 ( i n ESTAB A [o1=a0<ra, , „ n , |us(aO)|- 1 ><STOPTIMER,ua>] A [STOPTIMER] A [ua]) • i n ACK-WAIT A [a^=oO] A [at(TIMEOUT)] D 0 ( i n ACK-WAIT A [0 1=aO<TIMEOUT> < S d | u s ( a O ) | - 1 'STARTIMER>] A [ 5 d | u s ( a 0 ) | - 1 ] A [STARTIMER]) Module Receiver (UserReceiver ( P r o v i d e r ) ; EntityNetwork (User)) SES : a2=[ur, r d , sa] T r a n s i t i o n Semantics: * [ a 2 = C T ° ] A [ a t ( r d | u r ( a O ) | ) ] 0 O ( [ a 2 = a 0 < r d ) u r ( a 0 ) | > < u r | u r U 0 ) | ' S a | u r ( a O ) | > ] A  [ u r | u r ( a O ) | ] A C s a | u r ( a O ) | ] ) • [02 = 0-0] A [ a t ( r d k where k*|ur(aO)|)] o O([02=oO<rd k > < s a | u r ( a 0 ) | _ 1 >] A [ s a | u r ( o 0 ) | - 1 ] ) ( * A d d i t i o n a l Modules*) Module Userl ( U s e r T r a n s m i t t e r ( U s e r ) ) P r o p e r t i e s : • n ( [ u s ] o [01=X] V [ua e s u f f ( 0 1 , u s ) ] ) • [a1=X] V [ u a e s u f f ( a 1 , u s ) ] o <>[us] Module U s e r 2 ( U s e r R e c e i v e r ( U s e r ) ) P r o p e r t i e s : none Module System ( S y s t e m T r a n s m i t t e r ( P r o v i d e r ) ) P r o p e r t i e s : • [ SETTIMER e S u f f U l , [ STOPTIMER, TIMEOUT ]) ] <>[TIMEOUT] Module Network ( E n t i t y N e t w o r k ( P r o v i d e r ) E n t i t y N e t w o r k ( P r o v i d e r ) ) P r o p e r t i e s : • n ( [ r d i ] V [ r d i eo2] o ([sd^^ eo, ] A [ d a t a ( r d i )=data(sd i ) ] ) ) • n ( [ r a i ] V [ r c ^ ea1 ] o [sa^ eo2]) • n o [ s d - ] o <>[rd. ] 1 1 • n o [ s a . ] o <>[ra^ ] • n o [ s d ] o <>[rd] • n o [ s a ] o <>[ra] APPENDIX 7 FDT S p e c i f i c a t i o n of the Stop-Wait P r o t o c o l type data-type=...; seq-type=0...; id-type=(DATA,ACK) ; (* Channel d e f i n i t i o n s *) Channel UserTransirtitter (User , P r o v i d e r ) ; By User: SENDreq(d:data-type); By P r o v i d e r : SENDack; Channel UserReceiver(User, P r o v i d e r ) ; By P r o v i d e r : RECEIVEindic(d:data-type); Channel EntityNetwork(User, P r o v i d e r ) ; By User: SEND(id:id-type, d:data-type, seq:seq-type); By P r o v i d e r : RECEIVE(id:id-type,d:data-type, seq:seq-type); Channel System T r a n s m i t t e r (User, P r o v i d e r ) ; By User: STARTTIMER; STOPTIMER; By P r o v i d e r : TIMEOUT; (* Module d e f i n i t i o n s *) Module T r a n s m i t t e r ( U : U s e r T r a n s m i t t e r ( P r o v i d e r ) ; N:Ent ityNetwork(User); S:SystemTransmitter(User)); Var data:data-type; send-seq:seq-type; S t a t e s e t [ESTAB,ACK-WAIT]; I n i t i a l i z e 1 00 Begin s t a t e . to ESTAB; send-seq:=0; end (* t r a n s i t i o n s *) t r a n s from ESTAB to ACK-WAIT when U.SENDreq(d) begin data:=d; out N.SEND(DATA,data,send-seq) ; out S.STARTTIMER; end; from ACK-WAIT to ESTAB when N.RECEIVE(ACK,-,seq) provided (send-seq=seq) begin send-seq:=send-seq+1; out U.SENDack; out STOPTIMER; end; from ACK-WAIT to SAME when S.TIMEOUT begin out N.SEND(DATA,data,send-seq); out S.STARTTIMER; end; end Module Module R e c e i v e r ( U : U s e r R e c e i v e r ( P r o v i d e r ) N:EntityNetwork(User)) Var recv-seq:seq-type; I n i t i a l i z e begin recv-seg:=0; end (* t r a n s i t i o n s *) tr a n s when N.RECEIVE(DATA,d,seq) provided(seq=recv-seq) begin out N.SEND (ACK,-,seq); 1 02 out U.RECEIVEind(d); recv-seq:=recv-seq+1 ; end; p r o v i d e d otherwise begin out N.SEND(ACK,-,recv-seq); end; end Module. APPENDIX 8 SETL s p e c i f i c a t i o n of the A l t e r n a t i n g B i t P r o t o c o l type data-type=. . .; seq-type=0..1; id-type=(DATA,ACK); (*Channel d e f i n i t i o n s * ) Channel E n t i t y U s e r ( U s e r , P r o v i d e r ) ; By User: SENDreq(d:data-type); RECVreq(); By P r o v i d e r : RECVrresp(d:data-type); Channel EntityNetwork(User, P r o v i d e r ) ; By User: SEND(id:id-type; d:data-type, seq:seq-type); By P r o v i d e r : RECV(id:id-type; d:data-type; seq:seq-type); Channel E n t i t y S y s t e m ( U s e r , P r o v i d e r ) By User: SETTIMER; STOPTIMER; BUFFERstore(d:data-type); BUFFERreq(); By P r o v i d e r : TIMEOUT() BUFFERresp(d:data-type);e (*Abbreviations used i n t h i s s p e c i f i c a t i o n * ) us( a)=P( a,SENDreq) , us^^ =SENDreq(d i ) uq(a)=P(a, RECVreq) ur(a)=P(a,RECVresp), u r i =RECVresp(a i ) sd(0)=P(0,[SEND where id=DATA]), s d i =SEND(DATA,di , i mod 2) rd(0)=P(0,[RECV where id=DATA]), r d i =RECV(DATA,b^ , i mod 2) sa(a)=P(0,[SEND where id=ACK]), sa. =SEND(ACK,-,i mod 2) ra(0)=P(0,[RECV where id=ACK]), r a i =RECV(ACK,-,i mod 2) 1 03 1 04 bs ( a ) = P U , BUFFERstore) , b s i =BUFFERstore ( ) br(a)=P(a,BUFFERresp), b r i =BUFFERresp(a^ ) bq(a)=P(o,BUFFERreq) in ESTAB = [a=X] V [ r a | u s ( a ) | _ 1 e s u f f ( a , u s ) ] i n ACK-WAIT = [a*\] A [ r a , / \ i , |us(a) |- 1 /suf f ( a , u s ) ] Buf-not-empty = [|bs(o)| - | b r ( a ) | >0] B u f - n o t - f u l l = [ | bs (cr) | - | br ( a) | <buf-capac i t y ] ( s t a t e l ) (state2) (bf 1 ) (bf2) (*Module D e f i n i t i o n s * ) Module ABPEntity ( E n t i t y U s e r ( P r o v i d e r ) ; E n t i t y N e t w o r k ( U s e r ) ; E n t i t y S y s t e m ( U s e r ) ; SES: a=[us,uq,ur,sd,rd,sa,ra,bs,br,bq,SETTIMER,STOPTIMER,TIMEOUT] T r a n s i t i o n Semantics: • i n ESTAB A [o=a0] A [ a t ( u s ) ] o ( t i ) 0 ( i n ACK-WAIT A t a = a 0 < u s | u s ( a u ) | >  < S d | u s ( a 0 ) | ' SETTIMER>] A [ s d | u s ( a 0 ) | ] A [SETTIMER]) • i n ACK-WAIT A [o-aO] A t a t * r a | u s ( a n ) | - 1 ^ 0 ( t 2 ) 0 ( i n ESTAB A lo=o0<ralus{o0)l_] ><STOPTIMER>] A [STOPTIMER]) 1 05 i n ACK-WAIT A [a=a0] A [at(TIMEOUT)] o (t3) 0 ( i n ACK-WAIT A [a=a0<TIMEOUT> < 5 d | u s ( a 0 ) | - 1 ' SETTIMER>] A [ s d | u s ( a 0 ) | - 1 ] A f SETTIMER>]) B u f - n o t - f u l l A [a=a0] A f a t ( r d | b s ( a 0 ) | '1 0 ( t 4 ) 0 ( [ a = a O < r d j b s U o ) | > < b S | b s ( a O ) | ' S a | b s ( a 0 ) | > ] A  t b S | b s ( a O ) | ] A [ s a | b s ( a 0 ) | ] ) [a=a0] A [ a t ( r d k where k*|bs(a0)|)] o (t5) O([a=a0<rd R > < s a j b s ( a 0 ) ( _ 1 >] A [ s a | b s ( a O ) | - 1 ] ) [o=a0] A [ a t ( u q ) ] o 0 ([ a=a0<rqxbq> ] A [bq]) (t6) [a=a0] A [ a t ( b r ) ] o (t7) 0 ( [ a = a O < b r j b r U o ) | > < u r | b r ( a Q ) | >] A [ u r | b r ( a 0 ) | ] ) ( * A d d i t i o n a l Modules*) Module U s e r ( E n t i t y U s e r ( U s e r ) ) P r o p e r t i e s : • n o u s (U1 ) • n o u q (U2) Module Sy s t e m ( E n t i t y S y s t e m ( P r o v i d e r ) ) P r o p e r t i e s : 1 06 • [SETTIMER e suff(a,[STOPTIMER, TIMEOUT])] (Timer) D <>[TIMEOUT] • [|br(a)|=n] o [|bs(a)|>n] A (Bl) [V i < n ( d a t a ( b r i )=data(bs i ) ) ] • Buf-not-empty A [bq] D <>[br] (B2) • Buf-not-empty o Buf-not-empty U n t i l - A f t e r (B3) [bq] • B u f - n o t - f u l l D B u f - n o t - f u l l U n t i l - A f t e r (B4) [bs] • [bq] o <>Buf-not-full (B5) • [bs] o <>Buf-not-empty (B6) Module Network(EntityNetwork(Provider) E n t i t y N e t w o r k ' ( P r o v i d e r ) ) Propert i e s : • [RECV'(m)] V [RECV(m)ea'] D [SEND(m)ea] (N1) • [RECV(m)] V [RECV(m)ea] o [SEND'(m)ea'] ( N T ) • [msg(P(a,SEND)) i =msg(P(a',RECV)) f c ] (N2), A [msg(P(a,SEND))_j =msg(P(a',RESV)) 1 ] (N2') A [ i < j ] D [k<l] • n o [ SEND ] o <>[RECV r] (N3), (N3') • n o [ SEND(m) ] o <>[RECV'(m)] (N4), (N4') 

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-0051887/manifest

Comment

Related Items