UBC Theses and Dissertations

UBC Theses Logo

UBC Theses and Dissertations

Total correctness of an ISO transport protocol subset Jürgensen, Wolfgang 1984

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

Item Metadata

Download

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

Full Text

TOTAL CORRECTNESS OF AN ISO TRANSPORT PROTOCOL SUBSET by WOLFGANG JURGENSEN D i p l . - I n f . , U n i v e r s i t y of Bonn, West Germany, 1982 A THESIS SUBMITTED IN PARTIAL FULFILLMENT OF THE REQUIREMENTS FOR THE DEGREE OF MASTER OF SCIENCE i n THE FACULTY OF GRADUATE STUDIES (Department of Computer Sci e n c e ) We accept t h i s t h e s i s as conforming t o the r e q u i r e d s t a n d a r d THE UNIVERSITY OF BRITISH COLUMBIA A p r i l 1984 © Wolfgang J i i r g e n s e n , 1984 In p r e s e n t i n g t h i s t h e s i s i n p a r t i a l f u l f i l m e n t of the requirements f o r an advanced degree a t the U n i v e r s i t y o f B r i t i s h Columbia, I agree t h a t the L i b r a r y s h a l l make i t f r e e l y a v a i l a b l e f o r r e f e r e n c e and study. I f u r t h e r agree t h a t p e r m i s s i o n f o r e x t e n s i v e copying 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 t h a t copying or p u b l i c a t i o n of t h i s t h e s i s f o r f i n a n c i a l g a i n s h a l l not be allowed without my w r i t t e n p e r m i s s i o n . Department of 6cv*y> ^ /g>- Sett*otC-f The U n i v e r s i t y of B r i t i s h Columbia 2075 Wesbrook P l a c e Vancouver, Canada V6T 1W5 Date 7cn i i ABSTRACT In t h i s t h e s i s , a new P e t r i net based model c a l l e d CSP nets i s proposed to s p e c i f y the c o n t r o l s t a t e aspects of a communication p r o t o c o l . T h i s model i s combined with a CSP programming language s p e c i f i c a t i o n to produce a formal model of a s i g n i f i c a n t subset of the ISO tran s p o r t p r o t o c o l . The two compatible models are v a l i d a t e d . The CSP programming language s p e c i f i c a t i o n i s checked for p a r t i a l c o r r e c t n e s s and system safety and l i v e n e s s using a s s e r t i o n proofs and temporal l o g i c . A s a t i s f a c t i o n proof i s provided, too. The CSP net s p e c i f i c a t i o n , checked by an automatic v a l i d a t i o n t o o l c a l l e d "cspnet" c o n t a i n s no deadlock and i s c y c l i c . The combined v a l i d a t i o n r e s u l t s show our ISO t r a n s p o r t p r o t o c o l s p e c i f i c a t i o n to be t o t a l l y c o r r e c t . T h i s t h e s i s argues that a communication p r o t o c o l should be s p e c i f i e d using a combined programming language and st a t e t r a n s i t i o n model to produce a rigorous and complete proof of i t s c o r r e c t n e s s . i i i TABLE OF CONTENTS ABSTRACT i i TABLE OF CONTENTS i i i LIST OF TABLES v LIST OF FIGURES - v i ACKNOWLEDGEMENT v i i CHAPTER 1: INTRODUCTION 1 1.1 Mo t i v a t i o n and Ob j e c t i v e 1 1.2 Thesis o u t l i n e 4 CHAPTER 2: THE ISO TRANSPORT LAYER 6 2.1 The tr a n s p o r t s e r v i c e (TS) 6 2.2 The tr a n s p o r t p r o t o c o l (TP) 8 CHAPTER 3: CSP NETS 1 3 3.1 Communicating Sequential Processes 14 3.2 CSP nets 16 3.3 T r a n s l a t i n g a CSP program i n t o a CSP net 18 CHAPTER 4: SPECIFICATION OF THE ISO TRANSPORT PROTOCOL 22 4.1 The ISO t r a n s p o r t . p r o t o c o l s p e c i f i c a t i o n using CSP 23 4.2 The ISO t r a n s p o r t ^ p r o t o c o l s p e c i f i c a t i o n i v using CSP nets 26 4.3 The ISO tra n s p o r t p r o t o c o l s p e c i f i c a t i o n s : explanations 27 CHAPTER 5: VERIFICATION OF THE ISO TRANSPORT PROTOCOL 32 5.1 Axiomatic semantics for CSP 32 5.2 A channel i n v a r i a n t 34 5.3 A tra n s p o r t s t a t i o n i n v a r i a n t 42 5.4 System s a f e t y „ 43 5.5 Liveness 45 5.6 D u p l i c a t i o n , d i s o r d e r i n g and l o s i n g of TPDUs 48 5.7 S a t i s f a c t i o n proofs 49 5.8 Freedom from deadlock 51 5.9 Summary: T o t a l c o r r e c t n e s s * 52 CHAPTER 6: CONCLUSION 54 REFERENCES 56 APPENDIX 1: Program "cspnet" and data • 59 APPENDIX 2: CSP net s p e c i f i c a t i o n of the ISO tran s p o r t p r o t o c o l 74 APPENDIX 3: "cspnet"-Documentation 76 LIST OF TABLES Table 1: TPDUs v i LIST OF FIGURES F i g . 1 : The t r a n s p o r t l a y e r 6 F i g . 2: A simple CSP net 1 8 F i g . 3: The 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 20 F i g . 4: ISO t r a n s p o r t p r o t o c o l process arrangement 22 F i g . 5: Transport s t a t i o n CSP s p e c i f i c a t i o n 24 F i g . 6: Channel CSP s p e c i f i c a t i o n 25 F i g . 7: Sink CSP s p e c i f i c a t i o n 25 F i g . 8: Transport p r o t o c o l CSP net s p e c i f i c a t i o n 26 F i g . 9: General b u f f e r s t a t e 30 v i i A c k n o w l e d g e m e n t Thanks t o D r . 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 t h a n k D r . S. T. Chanson f o r r e a d i n g t h e f i n a l d r a f t . 1 CHAPTER j j _ INTRODUCTION 1.1 M o t i v a t i o n and O b j e c t i v e Over the l a s t decade the amount of communication across the world has r i s e n d r a m a t i c a l l y . Not only are humans p l a c i n g i n t e r c o n t i n e n t a l c a l l s in minutes' or even seconds' time, but computers have been organized into l a r g e communication networks, too: ARPAnet [McQuillan 77], CSnet [Landw 82], CYCLADES [Pouzin 82], Datapac [Clipsham 76]. Software and hardware of these networks have to be r e l i a b l e in order to ensure r a p i d , u n i n t e r r u p t e d and e r r o r free communication. While it the hardware engineers have found procedures e i t h e r to make t h e i r communication t o o l s r e l i a b l e w i t h i n narrow s e c u r i t y l i m i t s or to deal with hardware f a i l u r e s in f a i r l y quick time, the software engineers have not yet been such s u c c e s s f u l . The working of a computer network i s l a r g e l y c o n t r o l l e d by sets of formal i n t e r a c t i o n procedures c a l l e d communication p r o t o c o l s . Their s p e c i f i c a t i o n has been standardized i n t e r n a t i o n a l l y in order to allow for easy i n t e r c o n n e c t i o n among s i n g l e computers and even d i f f e r e n t networks [IS01]. The I n t e r n a t i o n a l Standard O r g a n i s a t i o n (ISO) has decided on an a r c h i t e c t u r e of seven d i s t i n c t l a y e r s of p r o t o c o l s , where each la y e r accepts s e r v i c e s from i t s next lower l a y e r and provides s e r v i c e s to i t s next higher l a y e r . As of 1982 the four lower l a y e r s ( p h y s i c a l , l i n k , network and tr a n s p o r t ) had been s p e c i f i e d at l e a s t in. the form of d r a f t proposals [S t u d n i t z 2 83]. However, a l l the s p e c i f y i n g documents use E n g l i s h prose for e x p l a i n i n g the f u n c t i o n a l p r i n c i p l e s of the p r o t o c o l s . This may lead to a better understanding of the mechanisms and algorithms involved, but i t c o n t r i b u t e s l i t t l e to achieve rig o r o u s proof of t h e i r c o r r e c t n e s s . F i n d i n g the proof of c o r r e c t n e s s of an a l g o r i t h m i n v o l v e s two steps: F i r s t , the v e r b a l d e s c r i p t i o n of the a l g o r i t h m has to be s p e c i f i e d in a well d e f i n e d formal model. U s u a l l y t h i s formal s p e c i f i c a t i o n i s c o n s t r u c t e d by hand from the v e r b a l d e s c r i p t i o n . Second, the a l g o r i t h m now d e f i n e d by the formal model has to be v a l i d a t e d . Two main kinds of models have been used to s p e c i f y communication p r o t o c o l s : State t r a n s i t i o n models [Bochmann 77], [Bochmann 80], [Danthine 80], [Vuong 83], e s p e c i a l l y P e t r i net based models and i t s v a r i a n t s [Peterson 77], [Jensen 81], [Genrich 81], have proved very u s e f u l in d e s c r i b i n g the c o n t r o l aspects of s e l e c t e d p r o t o c o l components. Gl o b a l 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 such a model. A common setback, however, i s encountered, when the systems to be s p e c i f i e d and l a t e r v a l i d a t e d become large and r i c h of features which are d i f f i c u l t to c o n t r o l . Such systems e x h i b i t complicated behavior, which often r e s u l t s in a problem commonly known as s t a t e space e x p l o s i o n : The system can reach so many d i f f e r e n t s t a t e s that i t becomes u n t o l e r a b l y timeconsuming even for l a r g e computers to examine them a l l . 3 S p e c i f i c a t i o n approaches which are based on a high l e v e l programming language allow for a s s e r t i o n proof v e r i f i c a t i o n techniques [Hoare 69], [Owicki 76], [Kroger 80] provided the programming language has a well d e f i n e d axiomatic semantics. A number of programming languages capable of s p e c i f y i n g message exchange behavior have been developed [Hoare 78], [Vuong 84], 'but accompanying axiomatic semantics and a s s e r t i o n proof methods are s t i l l rare [Apt 80], [Sounda 83], and l i t t l e work has been done to automate a s s e r t i o n proof techniques [Wald 77]. A s s e r t i o n proofs are t h e r e f o r e u s u a l l y done by hand and i n v i t e a l l the error's humans commonly commit. E s p e c i a l l y , when the same person having s p e c i f i e d an alg o r i t h m subsequently v e r i f i e s i t by hand, (s)he i s l i k e l y to make the same e r r o r s in both phases. Although t h i s d i f f i c u l t y can be p a r t l y overcome by e n t r u s t i n g 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 to d i f f e r e n t i n d i v i d u a l s , human involvement nevertheless remains a major problem for a s s e r t i o n proof methods. An important advantage of a s s e r t i o n proofs i s , however, that i n d i v i d u a l s conducting the proof can f a i r l y f r e e l y decide, what they want to prove. State t r a n s i t i o n models, on the other hand, u s u a l l y j u s t allow proof of a few g l o b a l p r o p e r t i e s such as freedom from deadlock, properness and/or l i v e n e s s of the s p e c i f i e d systems. Although some progress has been made i n proving s t r u c t u r a l designer d e f i n e d p r o p e r t i e s by the use of i n v a r i a n t s i n P e t r i net r e l a t e d models [Lautenbach 74], [Jensen 81a], they do not allow the same freeness of choice and elegance of expression as a s s e r t i o n s do. 4 In the context of a s s e r t i o n proofs for d i s t r i b u t e d algorithms two p r o p e r t i e s are important [Hailpern 80]. Safety p r o p e r t i e s ensure "that bad things w i l l not happen", thus making up the p a r t i a l c o r r e c t n e s s of a system. Such p r o p e r t i e s have been i n v e s t i g a t e d in a number of research e f f o r t s [Hailpern 81]. Liveness p r o p e r t i e s ensure "that good things w i l l happen". They are much l e s s researched [Owicki 82], but are important for recor d i n g p e r i o d i c behavior of non terminating systems. Communication p r o t o c o l s can u s u a l l y be modeled by non terminating programs using i n f i n i t e loop c o n s t r u c t ions. It i s our f i r m b e l i e f that both main s p e c i f i c a t i o n approaches have t h e i r advantages. They should t h e r e f o r e be used simultaneously to produce a v a l i d a t i o n of a r e a l world , p r o t o c o l . For an ISO p r o t o c o l d e s c r i b e d in E n g l i s h t h i s means the c o n s t r u c t i o n of a programming language and a s t a t e t r a n s i t i o n model, which have to be compatible. Appropriate proof methods w i l l then be a p p l i e d to these two models. T h i s t h e s i s i s intended to be a f i r s t step in to the l a r g e l y unresearched t e r r a i n of i n t e g r a t e d proof methods i n v o l v i n g both programming language and state t r a n s i t i o n models. A dual model of the ISO tran s p o r t p r o t o c o l w i l l be developed and proof methods of the two de s c r i b e d kinds w i l l show i t s t o t a l c o r r e c t n e s s . 1.2 Thesis o u t l i n e In the remainder of t h i s t h e s i s , Chapter 2 b r i e f l y 5 d e s c r i b e s the features of the ISO transport p r o t o c o l which w i l l be modeled. Chapter 3, a f t e r i n t r o d u c i n g Communicating Sequential Processes (CSP) [Hoare 78], w i l l d e r i v e from them a corresponding, compatible P e t r i net based s p e c i f i c a t i o n , which we c a l l e d a CSP net. A b r i e f example w i l l c l a r i f y the s u i t a b i l i t y of CSP nets for modeling communication p r o t o c o l behavior. In Chapter 4, the important p a r t s of the ISO tr a n s p o r t p r o t o c o l are s p e c i f i e d both by using CSP and CSP nets. Chapter 5 introduces an axiomatic semantics for CSP [Sounda 83] and then proceeds to prove s e l e c t e d i n v a r i a n t s for the ISO t r a n s p o r t p r o t o c o l . Systems sa f e t y , l i v e n e s s p r o p e r t i e s and freedom from deadlock are considered as w e l l . Chapter 6 o f f e r s the c o n c l u s i o n s of t h i s t h e s i s , i n c l u d i n g some suggestions for future research. 6 CHAPTER 2_i THE ISO TRANSPORT LAYER The t r a n s p o r t l a y e r of the OSI Reference Model [IS01] ( F i g . 1) has p r e v a i l e d in the form of a d r a f t proposal in 1982 as a r e s u l t of many a c t i v i t i e s in p r o t o c o l s t a n d a r d i z a t i o n . It provides the transport s e r v i c e [ISO TS] to be used by the session l a y e r [ISO SP] and uses the network s e r v i c e [ISO NS ] . In t h i s s e c t i o n , we present an overview of the tran s p o r t l a y e r . I t s exact d e t a i l s can be found in [ISO TS], [ISO TP]. sess1 on l a y e r t r a n s p o r t 1 a y e r t r a n s p o r t t r a n s p o r t 1 a y e r c o n n e c t i o n ne twork t ayer F i g . 1: The tran s p o r t layer 2.1 The tr a n s p o r t s e r v i c e (TS) The t r a n s p o r t s e r v i c e d e f i n i t i o n d e f i n e s TS p r i m i t i v e s , which are implementation dependent elements of i n t e r a c t i o n between a s e r v i c e provider and a s e r v i c e user, here between a network 1 a y e r 7 t r a n s p o r t and a session e n t i t y . They are sent through t r a n s p o r t s e r v i c e access p o i n t s between those l a y e r s . P r i m i t i v e s are the only way for the s e r v i c e user to" be in contact with i t s supporting l a y e r s ; the i n t e r n a l working of the t r a n s p o r t s e r v i c e p r o v i d e r ( i . e. the t r a n s p o r t p r o t o c o l ) i s t h e r e f o r e i n v i s i b l e to the session l a y e r . The t r a n s p o r t s e r v i c e d e f i n i t i o n d e f i n e s the TS p r i m i t i v e s to be used by the session e n t i t i e s for three separate phases: The connect ion establishment phase serves to e s t a b i s h ' an end-to-end transport connection (TC) between two transport e n t i t i e s and i n v o l v e s four TS p r i m i t i v e s (T-connect request, i n d i c a t i o n , response and c o n f i r m a t i o n ) , which c a r r y parameters mainly for n e g o t i a t i n g the q u a l i t y of s e r v i c e (QOS) of the t r a n s p o r t connection. The QOS can be measured by throughput, t r a n s i t delay, e r r o r r a t e s , p r o t e c t i o n , maximal acceptable cost e t c . Since these parameters are o f t e n used to s p e c i f y b e t t e r s e r v i c e s than provided by the network l a y e r , the transport l a y e r i s a l s o c a l l e d q u a l i t y enhancement l a y e r . The data t r a n s f e r phase allows data to be exchanged across the TC. Therefore i t s TS p r i m i t i v e s (T-data request and i n d i c a t i o n , T-expedited-data request and i n d i c a t i o n ) c a r r y TS user data as the main parameter. The r e l e a s e phase terminates a TC; i t s TS p r i m i t i v e s (T-disconnect request and i n d i c a t i o n ) can c a r r y user data and/or the disconnect reason. 8 A TC can be imagined as a set of two queues for t r a n s p o r t s e r v i c e data u n i t s (TSDUs) connecting the two t r a n s p o r t e n t i t i e s in both d i r e c t i o n s as d e s c r i b e d in [ISO TS]. Each queue has a flow c o n t r o l mechanism a s s o c i a t e d with i t . As an option i t i s p o s s i b l e to t r a n s f e r expedited user data using the T-expedited-data request and i n d i c a t i o n p r i m i t i v e s and a separate flow c o n t r o l mechanism. Expedited data have preference over normal data in the queues. The d e t a i l e d working of the t r a n s p o r t l a y e r i s d e s c r i b e d in the t r a n s p o r t p r o t o c o l s p e c i f i c a t i o n . 2". 2 The t r a n s p o r t p r o t o c o l (TP) The task of the t r a n s p o r t p r o t o c o l i s to e s t a b l i s h , maintain and e v e n t u a l l y r e l e a s e a connection between two transport e n t i t i e s , thereby p r o v i d i n g the next upper layer with a q u a l i t y of s e r v i c e b e t t e r than d e l i v e r e d by the underlying network l a y e r . This i s achieved by a number of p r o t o c o l mechanisms [ISO TP] c a t e g o r i z e d as f i v e c l a s s e s of the ISO t r a n s p o r t p r o t o c o l . To communicate over a TC c o n t r o l and data t r a n s p o r t u n i t s ( i . e. the TPDUs in Table 1) are used. They c a r r y parameters and play an important r o l e in any s p e c i f i c a t i o n of the ISO t r a n s p o r t p r o t o c o l ; they are t h e r e f o r e d i s c u s s e d here. 9 CR TPDU CC TPDU DR TPDU DC TPDU DT TPDU AK TPDU ED TPDU EA TPDU RJ TPDU ERR TPDU Connection request TPDU Connection confirm TPDU Disconnect request TPDU Disconnect confirm TPDU Data TPDU Data acknowledge TPDU Expedited data TPDU Expedited acknowledge TPDU Reject TPDU Er r o r TPDU Table 1: TPDUs The connection request (CR) TPDU is- issued by an i n i t i a t i n g t r a n s p o r t s t a t i o n to request for the establishment of a tra n s p o r t connection, which w i l l be confirmed by the connection confirm (CC) TPDU. During the connection establishment the q u a l i t y of s e r v i c e to be provided to the s e s s i o n layer i s negotiated v i a the exchange of parameters, some which are o p t i o n a l : i n i t i a l c r e d i t s , references chosen by both s i d e s to i d e n t i f y the TC, the p r o t o c o l c l a s s , an optimal s i z e for the TPDUs to be sent, t a r g e t values of QOS requirements e t c . F u l f i l l m e n t of c e r t a i n QOS requirements i n v o l v e s d e c i s i o n s , whether expedited data t r a n s f e r i s employed, whether m u l t i p l e x i n g (mapping more than one TC onto one network connection) or s p l i t t i n g (mapping one TC onto more than one network connections) are needed, whether TSDUs can be segmented i n t o s e v e r a l TPDUs and reassembled a f t e r t r a n s f e r , whether 10 s e v e r a l TPDUs can be concatenated i n t o one Network Service Data Unit and separated a f t e r t r a n s f e r , how e r r o r d e t e c t i o n and recovery are performed e t c . A f t e r accomplishing the connection establishment phase through CR, CC (and in p r o t o c o l c l a s s 4 data acknowledge (AK)) TPDUs, the data t r a n s f e r phase works through data (DT) TPDUs, which are the main c a r r i e r for user data. AK TPDUs are used to acknowledge s u c c e s s f u l l y t r a n s f e r r e d data, a l s o for g i v i n g a d d i t i o n a l or withdrawing c r e d i t s from the communication partner thereby manipulating the current window s i z e . For expedited s e r v i c e the r o l e s of DT ' and AK TPDUs are taken over by the expedited data (ED) and expedited acknowledge (EA) TPDUs. They provide data t r a n s f e r under separate flow c o n t r o l ; an ED TPDU can only be sent, i f the previous one has been acknowledged by an EA TPDU. A tr a n s p o r t s t a t i o n with an outstanding ED TPDU suspends the sending of f u r t h e r DT TPDUs u n t i l i t re c e i v e s the acknowledging EA TPDU f o r the sent ED TPDU. The connection r e l e a s e phase i s performed through disconnect request (DR) and disconnect confirm (DC) TPDUs. A DR TPDU gives the reason for the re l e a s e request and p o s s i b l y a d d i t i o n a l information r e l a t e d to the termination of the connection. A DC TPDU j u s t serves to confirm a DR TPDU. To deal with p r o t o c o l e r r o r s the E r r o r (ERR) TPDU i s provided, c o n t a i n i n g the r e j e c t cause and a part of the r e j e c t e d TPDU. The r e a c t i o n of an e n t i t y r e c e i v i n g an ERR TPDU 11 i s i m p l e m e n t a t i o n d e p e n d e n t . A r e j e c t (RJ) TPDU, which c a u s e s r e t r a n s m i s s i o n of d a t a TPDUs, i s us e d i n the p r o t o c o l c l a s s e s 1 and 3 o n l y . The d i f f e r e n t TPDUs a r e d e s i g n e d t o e n a b l e t h e d i f f e r e n t t r a n s p o r t p r o t o c o l c l a s s e s t o enhance the QOS as r e q u e s t e d by the s e s s i o n l a y e r u s i n g the v a r i o u s p r o t o c o l mechanisms d e f i n e d i n [ISO T P ] . To cope w i t h d i f f e r e n t q u a l i t i e s of s e r v i c e p r o v i d e d by network l a y e r s and demanded by s e s s i o n l a y e r s the f i v e p r o t o c o l c l a s s e s of t h e t r a n s p o r t l a y e r a r e d e f i n e d as f o l l o w s : C l a s s 0 ( s i m p l e c l a s s ) p r o v i d e s a v e r y b a s i c t r a n s p o r t s e r v i c e w i t h c o n n e c t i o n e s t a b l i s h m e n t and d a t a t r a n s f e r . C l a s s 1 ( b a s i c e r r o r r e c o v e r y c l a s s ) has an e x p l i c i t r e l e a s e phase and i s a b l e t o r e c o v e r from network i n d i c a t e d e r r o r s by k e e p i n g c o p i e s of TPDUs, t i l l t h ey a r e acknowledged. As w e l l , e x p e d i t e d d a t a t r a n s f e r can be p r o v i d e d . C l a s s 2 ( m u l t i p l e x i n g c l a s s ) p r o v i d e s t h e p o s s i b i l i t y of m u l t i p l e x i n g s e v e r a l TC's o n t o one network c o n n e c t i o n . E x p l i c i t f l o w c o n t r o l u s i n g c r e d i t s i s p r o v i d e d i n t h i s c l a s s (as w e l l as i n c l a s s e s 3 and 4 ) . T h e r e f o r e a window can be d e f i n e d . C l a s s 3 ( e r r o r r e c o v e r y and m u l t i p l e x i n g c l a s s ) i n a d d i t i o n t o c l a s s 2 b u f f e r s t h e t r a n s p o r t s e r v i c e u s e r from network l a y e r s i g n a l l e d f a i l u r e s t h r o u g h a p p r o p r i a t e e r r o r r e c o v e r y p r o c e d u r e s . 1 2 C l a s s 4 ( e r r o r d e t e c t i o n and recovery c l a s s ) i s the most s o p h i s t i c a t e d , since i t can detect and recover from l o s t , d u p l i c a t e d and out of sequence TPDUs by using checksum mechanisms, sequence numbering, timeout mechanisms, resequencing, i n a c t i v i t y c o n t r o l e t c . The working of a major part of t h i s p r o t o c o l c l a s s i s s p e c i f i e d in a l a t e r chapter. 1 3 CHAPTER 3: CSP NETS The f i n a l goal of t h i s t h e s i s w i l l be to prove the t o t a l c o r r e c t n e s s of a major part of the ISO tr a n s p o r t p r o t o c o l in a rigorous way. Any e r r o r in the E n g l i s h prose s p e c i f i c a t i o n of the p r o t o c o l [ISO TP] should be detected. For t h i s purpose a s u i t a b l e model has to be s e l e c t e d . State t r a n s i t i o n r e p r e s e n t a t i o n s can e a s i l y model the c o n t r o l aspects of a p r o t o c o l . Moreover, they can be e a s i l y checked against o c c u r r i n g deadlock, properness, l i v e n e s s and/or boundedness in an automated way. A s s e r t i o n proof methods enable the p r o t o c o l designer to prove p a r t i a l c o r r e c t n e s s of a program by w r i t i n g down the system s p e c i f i c a t i o n s and then • conducting the c o r r e c t n e s s proof by hand. Both methods can be combined to achieve a proof of t o t a l c o r r e c t n e s s of a p r o t o c o l . For t h i s purpose CSP [Hoare 78] has been found to be a very powerful t o o l . CSP has three main advantages. F i r s t , CSP uses D i j k s t r a ' s guarded commands [ D i j k s t r a 75] to express n o n d e t e r m i n i s t i c program behavior. Second, CSP's input and output n o t a t i o n s can be e a s i l y expressed i n a state t r a n s i t i o n model based, on P e t r i nets by c o u p l i n g t r a n s i t i o n s . T h i s w i l l be expl a i n e d in d e t a i l s , when we d e f i n e CSP nets. F i n a l l y , there e x i s t at l e a s t two axiomatic semantics for CSP [Apt 80], [Sounda 83], which are s u i t a b l e f o r p a r t i a l c o r r e c t n e s s proofs of a p r o t o c o l s p e c i f i c a t i o n . Therefore CSP has been s e l e c t e d to serve as a t o o l for 1 4 s p e c i f y i n g the two communicating t r a n s p o r t e n t i t i e s . It can express the tra n s p o r t p r o t o c o l behavior in a programming language model, and, at the same time, can be e a s i l y t r a n s l a t e d i n t o a state t r a n s i t i o n model, developed in t h i s t h e s i s , based on P e t r i nets and c a l l e d CSP nets. 3.1 Communicating Sequent i a l Processes Communicating s e q u e n t i a l processes have been introduced by Hoare [Hoare 78] to allow the s p e c i f i c a t i o n of ' s e v e r a l processes communicating with each other through message exchange. CSP i s based on a number of p r i m i t i v e c o n s t r u c t s , which are p a r t i c u l a r l y well s u i t e d to model the behavior of communicating e n t i t i e s . The input and output commands ! and ? are used to s p e c i f y message sending and r e c e i v i n g . T h e i r form has been s l i g h t l y a l t e r e d for the purposes of t h i s t h e s i s . The statement P ? (k i n t o x) in a process s p e c i f i c a t i o n i n d i c a t e s that t h i s process r e c e i v e s a value k from another process P i n t o i t s v a r i a b l e x. Q ! (k from y) in a process s p e c i f i c a t i o n s t a t e s that a process sends value k from i t s v a r i a b l e y to another process Q. (The claus e s i n t o . . . and from... w i l l , whenever a p p r o p r i a t e and p o s s i b l e , often be omitted from the I/O commands in our l a t e r p r o t o c o l s p e c i f i c a t i o n s . ) Corresponding operations ?,! can only be executed simultaneously, otherwise input/output commands are s a i d to f a i l . T h i s s y n c h r o n i z a t i o n concept i s a c r u c i a l p r i n c i p l e of CSP. As well the message i s t r a n s f e r r e d i n s t a n t a n e o u s l y . Any b u f f e r i n g by queues between 1 5 communicating processes has therefore to be modeled by an extra process sending/receiving/storing messages. In these processes flow control mechanisms can be specified. Di j kstra's guarded command has the form G --> C. G is called a guard. C is a command l i s t and contains statements. A guard can contain boolean expressions or input or output commands. A guarded command can be executed, i f f i t s guard does not f a i l . (A boolean expression f a i l s , i f f i t s value is 'false''.) When a guarded command is executed, then f i r s t the guard G is executed by executing i t s constituent commands, then the command l i s t C. Note: In agreement with c r i t i c i s m s against CSP [Kieburtz 79] we have allowed output commands in guards. An alternative "command [ G1 —> CI n G2 --> C2 n Gn —> Cn] (n>1 ) is composed of a number of guarded commands. Execution of an alternative command means execution of an arbitrary one of i t s constituent guarded commands, whose guard does not f a i l . If a l l guards G1,...,Gn f a i l , then the alternative command f a i l s . Since alternative commands specify arbitrary and therefore nondeterministic choices, the behavior of message exchanging stations, which can be a r b i t r a r i l y sending or receiving messages of different types (according to different 1 6 c o n d i t i o n s ) , are very s u i t a b l y modeled. A r e p e t i t i v e command * < a l t e r n a t i v e command> s p e c i f i e s as many executions of i t s a l t e r n a t i v e command as p o s s i b l e , t i l l the a l t e r n a t i v e command f a i l s . The r e p e t i t i v e command models the behavior of a s t a t i o n , which sends sequences of messages to i t s communication p a r t n e r ( s ) , very w e l l . For other features of CSP we r e f e r to [Hoare 78]. 3.2 CSP nets CSP nets are advocated in t h i s t h e s i s as a s u i t a b l e means to f a c i l i t a t e automatic p r o t o c o l v a l i d a t i o n . They are p r e d i c a t e - t r a n s i t i o n nets based on P e t r i nets [ P e t r i 62]. Let Pr be a set of p r e d i c a t e s and Ac be a set of a c t i o n s . 2(S) s h a l l denote the power set of a set S. Let N be the set of integer numbers. Then a CSP net i s defi n e d as a 7-tuple (P,T,F,B,Tp,Ta,S), where: - P i s a nonempty set of p l a c e s , - T i s a nonempty set of t r a n s i t i o n s , - F : P x T -> N i s the "forward incidence f u n c t i o n " , - B : P x T -> N i s the "backward incidence f u n c t i o n " , - Tp : T -> 2(Pr) i s the "pr e d i c a t e f u n c t i o n " which a s s o c i a t e s a set of p r e d i c a t e s with every t r a n s i t i o n t e T , - Ta : T -> 2(Ac) i s the " a c t i o n f u n c t i o n " , which a s s o c i a t e s a set of a c t i o n s with every t r a n s i t i o n t e T, - S : T -> 2(T) i s the "s y n c h r o n i z a t i o n f u n c t i o n " , which a s s o c i a t e s with every t r a n s i t i o n t e T a set S(t) of 1 7 t r a n s i t i o n s , which always f i r e simultaneously with t. t i s a t r i v i a l member of S ( t ) . A marking of a CSP net i s a mapping M : P -> N. " F i r i n g " of a s y n c h r o n i z a t i o n S can take p l a c e , i f f every t r a n s i t i o n t e S i s enabled by a p p r o p r i a t e tokens in i t s predecessor places and a l l the p r e d i c a t e s in T p ( t ) , t e S are t r u e . F i r i n g of a s y n c h r o n i z a t i o n changes a CSP net's marking according to F and B. Furthermore, the a c t i o n s in Ta(t) w i l l be executed simultaneously for a l l t r a n s i t i o n s t belonging to S, p o s s i b l y changing the values of l o c a l v a r i a b l e s of CSP net s p e c i f i e d processes. F and B can be represented by forward and backward incidence matrices C(F) and C(B). An incidence matrix C can be d e f i n e d * f o r a s e l f loop free CSP net by C = C(F) - C(B). I t w i l l turn out, however, that the use of s e l f loops often helps the u n d e r s t a n d a b i l i t y of a CSP net. It i s e s s e n t i a l to recognize that F and B do not n e c e s s a r i l y define a f u l l y connected CSP net. This property w i l l be used l a t e r to s p e c i f y the ISO t r a n s p o r t p r o t o c o l by a system of 5 d i f f e r e n t processes, a l l of which w i l l be d e f i n e d by a CSP net p a r t . A simple example i s shown in F i g . 2. I 18 with: P = {p1,p2,p3,p4}, C(F) = Tp(t1 ) Tp(t3) Tp(t4) -Ta (11 ) Ta(t3) Ta(t4) Ta(t5) S ( t i ) • S(t4) : 0 0 1 0 0 0 1 0 1 0 1 0 0 0 0 0 0 0 0 1 T={t1 ,t2,t3,t4,t5}, C(B) = Tp(t2) = Tp(t5) {k=0}, U = 2}, n , Ta(t2) = (k {k := 2}, {k := k-2}, O, := k-1}, {ti} for i = 1, 2, 3, S(t5) = {t4,t5}. 1 0 0 1 0 0 0 1 0 0 0 1 0 0 0 0 0 0 0 1 F i g . 2: A simple CSP net where {t4,t5} i s a s y n c h r o n i z a t i o n and can f i r e , i f f p2 and p4 contain a token and k=2. The a c t i o n executed w i l l be k:= k-2. 3.3 T r a n s l a t ing a CSP program i n t o a CSP net Places of CSP nets are used s t r i c t l y to represent' c o n t r o l s t a t e s . CSP net t r a n s i t i o n s t h e r e f o r e 'represent s t a t e t r a n s i t i o n s and can be thought of being the implementation of an assignment operator for a l o c a l v a r i a b l e " s t a t e " of a given process. This operator w i l l appear often in the f o l l o w i n g 19 p r o t o c o l s p e c i f i c a t i o n s using CSP. The a l t e r n a t ing b i t p r o t o c o l , an example A s i m p l i f i e d 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 [Bart 69] i s s p e c i f i e d below. This p r o t o c o l i s used often to c l a r i f y p r o t o c o l s p e c i f i c a t i o n approaches [Merl i n 79], [Boch78], [Diaz 83]. The p r o t o c o l works as f o l l o w s . A sender S sends messages to r e c e i v e r R and r e c e i v e s acknowledgements from R. Each message in c l u d e s a c o n t r o l b i t , whose value a l t e r n a t e s between 0 and 1 f o r consecutive messages. As shown in F i g . 3, S sends a message by f i r i n g t r a n s i t i o n 1, and r e c e i v e s an ack by f i r i n g t r a n s i t i o n 2. R r e c e i v e s a message by f i r i n g t r a n s i t i o n 7, and sends an ack by f i r i n g t r a n s i t i o n 8. To model a transmission delay two channel processes have been included which transmit messages (Ch1) and acks (Ch2). As s p e c i f i e d , t r a n s i t i o n s 1 and 3 are synchronized: S sends a message at the same time Ch1 r e c e i v e s i t . Other s y n c h r o n i z a t i o n s can be i n t e r p r e t e d in an analogous manner. The CSP programming language expresses s y n c h r o n i z a t i o n s through the d e f i n i t i o n of i t s send/receive operations ! and ?. Every occurrence of the operator corresponds to a t r a n s i t i o n i n the CSP net. For c l a r i f i c a t i o n purposes some t r a n s i t i o n s are marked by "M" or "Ack" and an a p p r o p r i a t e arrow, i f they s p e c i f y sending or r e c e i v i n g of messages or acknowledgements. Th i s dual model of 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 20 su.it.able for automatic proofs of g l o b a l p r o p e r t i e s through i t s CSP net s p e c i f i c a t i o n and for a s s e r t i o n proofs through i t s CSP programming language s p e c i f i c a t i o n . : s t a t e :- A; bL := 0; *[ s t a t e = A, Chi ! Message[bL] n s t a t e = W, Ch2 ? Ack[bL] n s t a t e = E ] : s t a t e :- B; bR := 0; *[ state=B, Ch1 ? Message[bR] n state=C, Ch2 ! Ack[bR] n state=D ] Ch1:': s t a t e :- empty; i := 0; ] Ch2:: s t a t e :- empty; j := 0; *[ s t a t e = empty, R ? A c k [ j ] n s t a t e = f u l l , S ! Ack[j ] ] - > s t a t e :- W - > s t a t e :- E - > s t a t e :- A; bL := bL* - > s t a t e :- C - > s t a t e :- D - > s t a t e :- B, bR := bR + i ] — > s t a t e • — • f u l l i ] - - > s t a t e • — empty; i • = i + 1 - > s t a t e :- f u l l - > s t a t e :- empty; j := j * 1 • C tO-r- bR : =bR ' 1 5 ^tr- -zzhc 6 E ( ) \ / "T T \ / ( ) o Ack Ack C h 2 F i g . 3: The 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 21 The s y n c h r o n i z a t i o n s of the net are {1,3},{4,7}, {6,8}, and {2,5}. The i n i t i a l s t a t e of the system i s i n d i c a t e d by an i n i t i a l marking of the places and the i n i t i a l i z a t i o n s of the l o c a l v a r i a b l e s . Notice that there i s a l o c a l v a r i a b l e ' s t a t e ' for each of the four processes. The operation + denotes a d d i t i o n mod 2. J 22 CHAPTER 4j_ SPECIFICATION OF THE ISO TRANSPORT PROTOCOL In the f o l l o w i n g , a l l three phases of the ISO tra n s p o r t p r o t o c o l (connection establishment, data t r a n s f e r and release phases) are s p e c i f i e d using both CSP and CSP nets. Timeout handling has been excluded. The arrangement of the f i v e communicating processes i s the f o l l o w i n g : s i nk Fig.4: ISO transport p r o t o c o l process arrangement P[0] and P[ 1 ] model the two tra n s p o r t e n t i t i e s . P[0] sends TPDUs to P [ 1 ] v i a channel process P [ 0 - > 1 ] and r e c e i v e s TPDUs from P[1 ] v i a P[l->0]. A l l messages l o s t from channels (a DR TPDU can destroy TPDUs waiting in a channel) are accepted by a process c a l l e d s i nk. Because of the symmetry of the message . t r a n s f e r mechanisms P[0] and P[1] have the same s t r u c t u r e , as well as P[ 0 - > 1 ] and P[1->0]. Subsections 4 . 1 and 4.2 w i l l s p e c i f y the ISO transport p r o t o c o l using CSP and CSP nets. Explanations of both s p e c i f i c a t i o n s w i l l be given in subsection 4.3. 23 4.1 The I SO tr a n s p o r t p r o t o c o l spec i f i c a t ion using CSP ( i ) The t r a n s p o r t s t a t i o n s : ({PAs} denotes an i n v a r i a n t proved in a later' chapter.) P[ i ] ( i : 0..1) :: s t a t e : 1..14; hg,hbg : 0..15; hg := 0; hbg := 0; s t a t e :- 5+ i ; * {PAs} state= 1+i, hbg>0,P[i- >i* 1 ] ! DT --> hbg := hbg- 1 a state= 1+i, P[i*1->i] ? AK --> hbg := hbg+ 1 n state= 1+i, hg<size,P[ i - > i + 1 3 ! AK --> hg := hg+1 n state= 1+i , P [ i + 1 - > i ] ? DT, P[ i -> i •1] ! AK - -> n i l n state= 1+i , P [ i - > i * 1 ] ! ED --> n i l • state= 1+i , P [ i + 1-> i ] ? ED,P[i ->i* 1 ] ! EA --> n i l n state= 1+i , P [ i + 1->i ] ? EA - -> n i l n state= 1+i, P [ i - > i * 1 ] ! DR • --> s t a t e :- 1 1 + i • s t a t e s 1+i, P [ i + 1 - > i ] ? DR --> stat e :- 13 + i n state= 3 + i , P [ i - > i * 1 ] ! CR --> s t a t e :- 7 + i ; P [ i *1->i ] ? CR,P[i 1 ] hg:=hg+1 n state= 3 + i , ->i * ! CC --> stat e :- 9+i; hbg:=1;hg:=1 n state= 3 + i — -> s t a t e :- 5 + i n state= 5 + i --> s t a t e :- 3 + i n state= 5+i, P [ i * 1->i ] ? CR,P[i -> i * 1 ] ! DR — -> n i l n state= 7 + i , P [ i +1->i ] ? CR - -> stat e :- 3 + i P [ i * 1-> i ] hbg : = 0 n state= 7 + i , ? CC,P[i ->i + 1 ] ! AK --> s t a t e : - 1 + i ; P [ i + 1->i ] hbg : = 1 n state= 7 + i , ? DR --> stat e :- 3 + i ; hg : = 0 n state= 9 + i , P [ i • 1->i ] ? AK --> s t a t e :- 1 + i n state= 9+i, P [ i + 1 - > i ] ? DR --> stat e :- 13 + i n state= 1 1+i , hg=0, hbg =0, P [ i + 1 ->i ] ? DR --> stat e :- 3 + i n state= 1 1+i , hg=0, hbg =0, P [ i + 1 ->i ] ? DC --> s t a t e :- 3 + i • state= 1 1+i , hg>0, hbg>0 --> hg:=0; hbg:=0 n state= 1 1+i , (mes:CR.. EA)P[i + 1 ->i] 7 mes --> n i l n s t a t e = 1 3 + i , hg = 0, hbg = 0, P [ i - > i M ] ! DC --> s t a t e :- 3 + i n s t a t e = 1 3 + i , hg>0, hbg>0 --> hg:=0;hbg:=0 n s t a t e = 1 3 + i , (mes:CR..DC)P[i + 1->i ] ? mes --> n i l ] F i g . 5: T r a n s p o r t s t a t i o n CSP s p e c i f i c a t i o n ( i i ) The c h a n n e l s : ({ChAs} d e n o t e s an i n v a r i a n t p r o v e d i n a l a t e r c h a p t e r . ) P[s->r : 0->1 , 1->0 ] :: s i z e s t a t e i n , o u t , i n e x , o u t e x b u f ( 0 . . s i z e - 1 ) , b u f e x nmsg xmsg s t a t e :- s + 15; i n := out := i n e x * {ChAs} [(msg:CR,CC,DT,AK) n (msg: ED,EA) n (msg: DR,DC) = i n t e g e r - c o n s t ; 15..16; i n t e g e r ; T P DUholder; (CR,CC,DT,AK,DR,DC); (ED,EA); = o u t e x := 0; i n < s i z e + o u t , i n e x = o u t e x , P [ s ] ? (msg i n t o b u f ( i n mod s i z e ) ) --> i n : = i n + 1 i n < s i z e + o u t , i n e x = o u t e x , P [ s ] ? (msg i n t o b u f e x ) in e x := in e x + 1 P [ s ] ? (msg i n t o b u f ( i n mod s i z e ) ) — > ( i : o u t . . i n - 1 ) : ( s i n k ! (nmsg from b u f ( o u t mod s i z e ) out := out + 1); ( i : o u t e x . . i n e x - 1 ) : ( s i n k ! (xmsg from b u f e x ) ; ,outex := outex + 1); i n := i n + 1 n (msg:CR,CC,DT,AK,DR,DC): outex = i n e x , out < i n , P [ r ] ! (msg from b u f ( o u t mod s i z e ) ) --> o u t := out + 1 n (msg:ED,EA): outex < i n e x , P[r](msg from bufex) — > outex := outex +1 ] F i g . 6: Channel CSP s p e c i f i c a t i o n ( i i i ) The sink s i n k : : sta t e :- 17; state : i n t e g e r ; t : TPDUholder; *[ (r->s : 0->1,1->0), (message:CR,CC,DT,AK,EA,ED,DR,DC) P[r->s] ? (message i n t o t) --> ni ] F i g : 7: Sink CSP s p e c i f i c a t i o n 26 4.2 The I so t r a n s p o r t p r o t o c o l spec i £ i c a t ion usinq CSP nets "O •vj "0 'O m m > C n O > o * h n xs CJ J) Ol u w - o HO.-' ~J -J 'O "J -sJ -v) -J -O 8: Transport p r o t o c o l CSP net s p e c i f i c a t i o n 27 4.3 The I SO transport p r o t o c o l spec i f i c a t ions: explanat ions  ( i ) D e s c r i p t i o n of s t a t i o n P[0] Every place in the CSP net s p e c i f i c a t i o n represents a s t a t e . If place i holds a token then the process i s s a i d to be in s t a t e i . T h i s i s r e f e r r e d to in the CSP programming language s p e c i f i c a t i o n as "state = i " . P[0] contains 7 d i f f e r e n t s t a t e s : s t a t e 1: "connected", stat e 3: "disconnected, w i l l i n g to communicate", st a t e 5: "disconnected, not w i l l i n g to communicate", state 7: " a c t i v e connect request pending", stat e 9: "passive connect request pending", stat e 11: " a c t i v e disconnect request pending", s t a t e 13: "passive disconnect request pending". F i r i n g a t r a n s i t i o n (and t h e r e f o r e the s y n c h r o n i z a t i o n i t belongs to) connecting two d i f f e r e n t places r e s u l t s in s t a t e change, e. g. to s t a t e i . In the CSP programming language notation t h i s i s r e f e r r e d to by the con s t r u c t "state :- i " . T r a n s i t i o n s are l a b e l e d with the TPDUs, which P[0] sends/receives when the t r a n s i t i o n i s f i r i n g . Often, to improve l e g i b i l i t y , only one t r a n s i t i o n i s drawn, where s e v e r a l t r a n s i t i o n with the same predecessor and successor p l a c e s , but d i f f e r e n t incoming/outgoing messages are s p e c i f i e d . To enhance c l a r i t y f u r t h e r , place 3 i s included twice. E s p e c i a l l y in the net r e p r e s e n t a t i o n the p r o t o c o l phases are showing up c l e a r l y . The connection establishment phase s t a r t s in s t a t e 3 and reaches s t a t e 1 e i t h e r through s t a t e 7 by sending a CR, 28 r e c e i v i n g a CC .and sending an AK TPDU (3-way-handshake) or through stat e 5 by r e c e i v i n g a CR, sending a CC and r e c e i v i n g an AK TPDU. CR c o l l i s i o n , which in the tr a n s p o r t p r o t o c o l cannot happen [ISO TP], i s avoided by the s t a t i o n ' s switching back i n t o s t a t e 3 v i a t r a n s i t i o n 7. During the data t r a n s f e r phase the s t a t i o n remains in state 1 and f i r e s any of the. t r a n s i t i o n 10 - 16, e f f e c t i n g the i n d i c a t e d TPDU tr a n s m i s s i o n s . The disconnect phase s t a r t s in s t a t e 1 and reaches s t a t e 3 e i t h e r through s t a t e 11 by sending a DR and then r e c e i v i n g a DC (or . c o l l i d i n g DR) TPDU or through s t a t e 13 by r e c e i v i n g a DR and sending a DC TPDU. For both stat e 11 and 13 a number of t r a n s i t i o n s implement loops to reset l o c a l v a r i a b l e s (which are disc u s s e d below) and to empty the channels. A disconnected s t a t i o n can switch f r e e l y between s t a t e s 3 and 5. For c l a r i t y reasons p r e d i c a t e s and a c t i o n s of a l l t r a n s i t i o n s are omitted from the CSP net r e p r e s e n t a t i o n . They can be found in the CSP programming language s p e c i f i c a t i o n . The CSP programming language r e p r e s e n t a t i o n i n c l u d e s the p r e d i c a t e s as c o n s t i t u a n t s of i t s guards G and the a c t i o n s as c o n s t i t u a n t s of i t s command l i s t s C i n i t s guarded commands G-->C. Pred i c a t e s and a c t i o n s use the f o l l o w i n g l o c a l integer v a r i a b l e s f o r c r e d i t management: 29 hg c o n t a i n s the number of c r e d i t s P[0] has given to the other s t a t i o n at any moment ("having g i v e n " ) , hbg contains the number of c r e d i t s P[0] has been given by the other s t a t i o n at any moment ("having been g i v e n " ) . The terms n i l (CSP repre s e n t a t i o n ) and e (CSP net repr e s e n t a t i o n ) mean that no a c t i o n i s s p e c i f i e d for t h i s p a r t i c u l a r guarded command/transition. F i n a l l y , the s p e c i f i c a t i o n of P[0] incl u d e s output commands to channel P[0->1] and input commands from channel P[l->0] as guard c o n s t i t u a n t s . They s p e c i f y the TPDU t r a n s f e r s y n c h r o n i z a t i o n s using the s y n c h r o n i z a t i o n d e f i n i t i o n s of CSP. A tab l e of the synch r o n i z a t i o n s of the CSP net i s included in Appendix 2. ( i i ) D e s c r i p t i o n of s t a t i o n P[1] P[1] i s s t r u c t u r e d in a manner completely analogous to P[0]. ( i i i ) D e s c r i p t i o n of channel P[0->1 ] Channel P[0->1] r e c e i v e s TPDUs from P[0] and a f t e r an u n s p e c i f i e d delay sends them ( i n most cases) to P[1]. The c o n t r o l s t r u c t u r e of a channel i s t r i v i a l and c o n s i s t s of one s t a t e , in which the channel always remains. A s s o c i a t e d with the channel are the l o c a l b u f f e r s buf(0..size-1) f o r normal TPDUs and bufex for expedited TPDUs. The l o c a l counter "out" p o i n t s to the next normal TPDU i n buf to be sent to P[1], the l o c a l counter " i n " point s to the next b u f f e r place in buf that can 30 take an' incoming normal TPDU.' bufex, inex and outex act i n an analogous manner for expedited TPDUs. Since bufex contains at most one TPDU at any time, we can often r e f e r to bufex instead of bufex(inex) or bufex(outex) without ambiguity. An incoming DR or DC TPDU causes a l l TPDUs in a b u f f e r to be sent to si n k . A general s t a t e for buf i s : TP TP TP TP TP DU OU OU DU OU o u t i n F i g . 9: General b u f f e r s t a t e Boolean expressions c o n t a i n i n g out and in (outex and inex) are components of guards in the CSP programming language s p e c i f i c a t i o n of the tran s p o r t p r o t o c o l . They can s p e c i f y , for example, i f a b u f f e r i s f u l l . If a channel accepts or sends a TPDU, l o c a l v a r i a b l e s are changed a c c o r d i n g l y . Simple s p e c i f i c a t i o n s of bounded b u f f e r s in CSP can be found in [Hoare 78], [Sounda 83]. (i v ) D e s c r i p t i o n of channel P[0->1] P[l->0] i s s t r u c t u r e d in a manner completely analogous to P[0->1]. (v) D e s c r i p t i o n of sink Sink (only one c o n t r o l state) simply acts as a r e c i p i e n t , for TPDUs forced out of a buf f e r by an incoming DR or DC TPDU. In 31 f u t u r e extensions, i t can act to r e c e i v e l o s t frames as w e l l . The dual s p e c i f i c a t i o n of the ISO t r a n s p o r t p r o t o c o l i s completed and we proceed to v e r i f y i t using a s s e r t i o n proofs and an automatic v a l i d a t i o n system lo o k i n g for g l o b a l p r o p e r t i e s of a CSP net.' ) 32 CHAPTER 5: VERIFICATION OF THE ISO TRANSPORT PROTOCOL 5.1 Axiomat i c semant i c s for CSP Several attempts to c o n s t r u c t an axiomatic semantics for CSP have been made, i n c l u d i n g [Apt 80], [Sounda], [Sounda 83]. Because the l a t t e r does not use shared a u x i l i a r y v a r i a b l e s , t h e r e f o r e e l i m i n a t i n g any need for i n t e r f e r e n c e proofs [Levin 81], we use t h i s system for conducting a s s e r t i o n p r o o f s . An important r o l e in the proof system i s played by h i s t o r y  v a r i a b l e s h [ i ] f o r processes P [ i ] , where h [ i ] records the TPDU exchange sequence which a f f e c t e d P [ i ] in the past. The element ( i , j , n ) in h [ i ] corresponds to a TPDU with contents n sent from P [ i ] to P [ j ] , j * i , and element ( j , i , n ) in h [ i ] corresponds to a TPDU with contents n r e c e i v e d by P [ i ] from P [ j ] . The f o l l o w i n g axioms and r u l e s of inference are taken from [Sounda 83] with only minor m o d i f i c a t i o n s in the input and output axioms. The pre- and p o s t c o n d i t i o n s are p r e d i c a t e s over the s t a t e of a process and i t s h i s t o r y v a r i a b l e . Assignment: ^Pe^ x : = e Skip: (p) s k i p {p} Output: { P h [ i ] . ( i , j , k ) } P [ : i ] ! ( k f r o m y ) { p } • denotes concatenation of an element to the r i g h t of a h i s t o r y v a r i a b l e . 33 i n p u t : * P K ; n S i ] . ( j , i , k ) ^ P [ ^ ? ( k i n t 0 x ) { P } Guarded s e l e c t i o n : (p,B(gl)} C(gl) , SI {q}', 1=1 ,. . ,m {p} [n(l=1,...,m)gl-->Sl]{q} SI i s a command l i s t . Guards are denoted by g l , 1 = 1,....,m. B(gl) i s the boolean part of a guard g l , C(gl) i s i t s I/O p a r t . If no I/O part i s s p e c i f i e d , C(gl) i s " s k i p " . P a r a l l e l composition: {p(i),h[i]=e} P [ i ] { q ( i ) } , i=1,...,n {p(1),...,p(n)} P[1]| | . . . | | P[n] ( q ( i ) , C o m p a t ( h [ i ] ) , i = 1,...n} H i s t o r y v a r i a b l e s are empty in the beginning. Compat(h[1],...,h[n]) denotes c o m p a t i b i l i t y of the h i s t o r y v a r i a b l e s h [ 1 ] , . . . , h [ n ] , see [Sounda 83]. The r u l e for guarded r e p e t i t i o n w i l l not be needed here. Furthermore, the r u l e s of s e q u e n t i a l composition • and consequence [Hoare 69] are assumed. The important strength of the proof system for CSP in [Sounda 83] i s the absence of any shared v a r i a b l e s . This feature i s supported by the absence of shared v a r i a b l e s in CSP i t s e l f . T h i s makes the c o n j u n c t i o n of the p r e d i c a t e s q ( i ) in the r u l e of p a r a l l e l composition p o s s i b l e . 34 Therefore every process involved can be proved p a r t i a l l y c o r r e c t independently and p a r t i a l c o r r e c t n e s s of the whole process system follows by c o n j u n c t i o n . 5.2 A channel i n v a r i a n t In the f o l l o w i n g we w i l l use a number of n o t a t i o n s : - "nmsg" w i l l denote a normal TPDU, "xmsg" w i l l denote an expedited TPDU. - V a l ( h , i ) denotes the contents being communicated in the i t h element of h i s t o r y v a r i a b l e h. - h [ i / ( a , b , c ) ] i s a h i s t o r y v a r i a b l e d e r i v e d from h [ i ] by removing a l l elements except those with components a,b,c. A "." w i l l denote an u n s p e c i f i e d component value. - h seq {(a,b,c),(d,e,f)} means that h i s t o r y v a r i a b l e s h c o n s i s t s , i f not empty, of elements of the form (a,b,c) or ( d , e , f ) . The f o l l o w i n g i n v a r i a n t ChAs w i l l be proved tt> hold at the i n d i c a t e d p o i n t in the channel s p e c i f i c a t i o n : ChAs : in > 0 & out > 0 & out < in < out + s i z e (1) & inex > 0 & outex > 0 & outex < inex ^ outex+1 (1') & h[s->r] seq {(s , s - > r , . ) , ( s - > r , r , . ) , ( s - > r , s i n k , . ) } (2) & ||h[s->r/(s,s->r,.)]|| = in + inex (3) & | | h [ s - > r / ( s - > r , r , . ) ] | | + ||h[s->r/s->r,sink,.) ] | [ = out + outex (4) & V ( i : 0^i<out): Val(h[s->r/(s,s->r,nmsg)],i+1) = Val(h[s->r/(s->r,.,nmsg)],i+1) (5) 35 & V ( i : 0 < i < o u t e x ) : V a l ( h [ s->r/(s,s->r,xmsg)],i+1) = V a l ( h [ s - > r / ( s - > r , . , x m s g ) 3 , i + 1 ) & V( i : o u t < i < i n ) : V a l ( h [ s - > r / ( s , s - > r , n m s g ) 3 , i +1) (5' ) = buf ( i mod s i z e ) (6) & V ( i : outex<i<inex): Val(h[s->r/(s,s->r,xmsg)],i+1) = bufex (6* ) & in - out = | |h[s->r/(s,s->r,nmsg)3| | |h[s->r/(s->r i • i nmsg]|| (7) & inex - outex = | | h[.s->r/( s, s->r , xmsg) ] | | |h[s->r/(s->r i ' i xmsg3|| (7' ) Explanat ions The i n v a r i a n t ChAs expresses the f o l l o w i n g f a c t s : (1) The markers in and out are always nonnegative and the b u f f e r holds between 0 and s i z e TPDUs. (2) Channel P[s->r] r e c e i v e s TPDUs from P[s] only and sends TPDUs to P[r] and sink only. (3) A l l TPDUs, which P[s->r3 r e c e i v e s , are counted by in and inex. ( 4 ) A l l TPDUs, which P[s->r] sends, are counted by out and outex. (5) A l l normal TPDUs with number below out have been rec e i v e d and sent by P[s->r3 in t h e i r proper order. (6) A l l normal TPDUs s t i l l in the bu f f e r are in t h e i r proper order. (7) i n - out i s the number of normal TPDUs in the b u f f e r . ( 1 ' ) , ( 5 ' ) , (6'), (7') express the to (11,(5), (6), (7) 36 analogous a s s e r t i o n s about expedited TPDUs. The a s s e r t i o n ChAs expresses the flow c o n t r o l p r o p e r t i e s of the ISO t r a n s p o r t p r o t o c o l . Notice t h e i r s p e c i f i c a t i o n i s part of the channel processes and not of the s t a t i o n s . T h i s i s due to the f a c t that the h i s t o r y v a r i a b l e s are l o c a l and non-shared. A process t h e r e f o r e does not know about the h i s t o r y v a r i a b l e s of the other processes. The h i s t o r y v a r i a b l e s of a channel c o n t a i n messages r e c e i v e d from a s t a t i o n and d e l i v e r e d to the communications partner. This holds p o s s i b i l i t i e s for extensions of t h i s s p e c i f i c a t i o n to include l o s t , d u p l i c a t e d and/or erroneous TPDUs. Proof of the channel invar iant ChAs . The proof of ChAs i s d i v i d e d i n t o the subcases G 1 , . . . , G 5 corresponding to the f i v e guarded commands of the channel CSP s p e c i f i c a t i o n . ChAs i s true immediately a f t e r the i n i t i a l i z i n g statements. When the r i g h t hand side of a ! or ? operation i s obvious from the context, i t w i l l often be w r i t t e n as "...". "nmsg" w i l l denote a normal TPDU, "xmsg" an expedited TPDU. G1 Receiving DT TPDUs Assert i o n : {ChAs & in<out+size}P[s]?(DT i n t o buf ( i n mod s i z e ) ) { C h A s ^ + 1 } 37 We d e r i v e from th e i n p u t axiom: The e x a c t e f f e c t of r e c e i v i n g a DT TPDU i s t h e r e f o r e the r e p l a c e m e n t of t h e c o n t e n t s of b u f ( i n mod s i z e ) w i t h DT and t h e c o n c a t e n a t i o n of (s,s->r,DT) t o h [ s - > r ] . P r o o f : The p r o o f i s c a r r i e d out f o r a l l p a r t s of ChAs. (1) {ChAs & i n < o u t + s i z e } => { i n > 0} ( t r i v i a l ) { i n > 0} P f s ] ?... {in+1 > 0}, s i n c e e x e c u t i o n of P [ s ] ? . . does not change the v a l u e of i n . T h e r e f o r e {ChAs & i n < out +size} P f s ] ?... {in+1 > 0}. {ChAs' & i n < o u t + s i z e ] P f s ] ? . . . {out>0} i s p r o v e d s i m i l a r i l y . {ChAs & i n < o u t + s i z e } => {out < i n < o u t + s i z e } ( t r i v i a l ) {out < i n < out + size}- P f s ] ? . . . { o u t < in+1 < out + s i z e } T h e r e f o r e {ChAs & i n < o u t + s i z e } P f s ] ? . . . { o u t ^ i n + 1 < o u t + s i z e } . The i m p l i c a t i o n s marked as t r i v i a l w i l l be o m i t t e d i n f u r t h e r p r o o f s . (1') i s not a f f e c t e d by r e c e p t i o n of a DT TPDU. (2) P f s ] ? . . . adds an element of form ( s , s - > r , . ) t o h [ s - > r ] . (3) | | h [ s - > r / ( s , s - > r , . ) ] | | i n c r e a s e s by 1. (4) , ( 5 ) , (5') a r e not a f f e c t e d by r e c e p t i o n of a DT TPDU. (6) The incoming-DT TPDU i s s t o r e d i n b u f ( i n mod s i z e ) , t h e r e f o r e : V a l ( h f s - > r / ( s , s - > r , n m s g ) ] , i n + 1 ) = b u f ( i n mod s i z e ) a f t e r e x e c u t i o n of P f s ] ? . . . 38 (6') i s not a f f e c t e d by r e c e p t i o n of a DT TPDU. (7) | | h [ s - > r / ( s , s - > r , . ) ] i n c r e a s e s by 1. (7') i s not a f f e c t e d by r e c e p t i o n of a DT TPDU. The a s s i g n m e n t axiom d i r e c t l y y i e l d s : {ChAs• i n in+ 1 } i n := i n + 1 {ChAs}. T h e r e f o r e , r u l e of s e q u e n t i a l c o m p o s i t i o n : {ChAs & i n < s i z e + o u t } P [ s ] ? ( D T i n t o b u f ( i n mod s i z e ) ) ; in:=in+1 {ChAs}. The r e c e p t i o n of a DT TPDU does not a f f e c t the t r u t h of ChAs. The p r o o f f o r r e c e p t i o n of AK, CR or CC i s a n a l o g o u s . The f i r s t g u a r d e d command of the c h a n n e l s p e c i f i c a t i o n t h e r e f o r e does not a f f e c t the t r u t h of ChAs. G2 R e c e i v i n g ED, EA TPDUs * A s s e r t i on: {ChAs & in< = s i z e + o u t & i n e x = outex } P[ s ] ? (ED i n t o buf ex) { C h A s ^ ® * + 1 } P r o o f : The i n p u t axiom y i e l d s : {p-b u f e x , h [ s - > r ] 'ED,h[s->r] • (s,s->r,ED) } P [ s ] ? ( E D i n t o b u f e x ) { p } The e f f e c t of the r e c e p t i o n of an ED TPDU t h e r e f o r e i s the a s s i g n m e n t of ED t o t h e b u f f e r -for e x p e d i t e d TPDUs and the c o n c a t e n a t i o n of (s,s->r,ED) t o h [ s - > r ] . 39 The p r o o f i s l a r g e l y a n a l o g o u s t o the one v e r i f y i n g the r e c e p t i o n of a DT TPDU (G1 ) . ( D , ( 5 ' ) , ( 6 ' ) , (7') t a k e o v e r the r o l e s of ( 1 ) , ( 5 ) , ( 6 ) , (7) and v i c e v e r s a . The p r o o f f o r EA TPDUs i s t h e same as f o r ED TPDUs. G3 R e c e i v i n g DR, DC TPDUs The i n p u t and o u t p u t axioms y i e l d : r b u f ( i n mod s i z e ) , h[ s->r ] ,_ r • . , r / . , • \ \ f - •> { P D R , h [ s - > r ] . ( s , s - > r , D R ) ) P f s ] ? ( D R i n t o b u f d n mod s i z e ) ) { p ] { p h S l - > r ] . ( s - > r , s i n k , n m s g ) } s i n k ! ( n m s 5 f r o m b u f ( o u t mod s i z e ) ) { p } { p h [ s - > r ] } s i n k ! ( x m s g from b u fex){p} h [ s - > r ] ••(s->r,sink,xmsg) U s i n g t h e s e a s s e r t i o n s one can e a s i l y p r o v e : ( i ) {ChAs} P f s ] ? (DR i n t o buf ( i n mod s i z e ) ) {ChAsJ[J + 1} The p r o o f i s a n a l o g o u s t o t h e one i n G1. ( i i ) {ChAs|[J + 1} S {ChAs^JJ + 1} w i t h S = ( i : o u t . . i n - V ) : ( s i n k ! (nmsg from b u f ( i mod s i z e ) ) ; out := out + 1) One s t e p o n l y of S i n v o l v e s t h e s e n d i n g of a normal TPDU and t h e p r o o f p r o c e e d s as i n G4. T h i s p r o o f i s a p p l i e d i n - o u t t i m e s ( t h e number of i t e r a t i o n s ) u s i n g t h e r u l e of c o m p o s i t i o n . 40 ( i i i ) { C h A s J [ J + 1 ) T { C h A s J " + 1 } w i t h T = ( i : o u t e x . . i n e x - 1 ) : ( s i n k ! (xmsg from b u f e x ) ; outex := outex + 1) The p r o o f p r o c e e d s i n a manner s i m i l a r t o ( i i ) . ( i v ) F i n a l l y : { C h A s J " + 1 l i n := in+1 {ChAs} Re p e a t e d a p p l i c a t i o n of the r u l e o f • c o n s e q u e n c e y i e l d s t h a t r e c e p t i o n of a DR TPDU l e a v e s ChAs u n a l t e r e d . R e c e p t i o n by a DC TPDU i s h a n d l e d a n a l o g o u s l y . G4 S e n d i n g a normal TPDU The p r o o f i s c o n d u c t e d f o r t h e s e n d i n g of a CR TPDU. The p r o o f s f o r t h e o t h e r normal TPDUs a r e a n a l o g o u s . A s s e r t i o n : {ChAs & out<in} P [ r ] ! ( C R from b u f ( o u t mod s i z e ) ) i c h A s o u t + 1 ^ P r o o f : The o u t p u t axiom y i e l d s : { p h [ s - > r ] • ( s - > r , r CR) } p t r ] ! < C R f r o m b u f ( o u t mod s i z e ) ) { p } The e f f e c t of the e m i t t a n c e of a CR TPDU i s t h e r e f o r e t h e c o n c a t e n a t i o n of an element of f o r m (s->r,r,CR) t o h [ s - > r ] . The p r o o f has t o check a l l s u b c a s e s of ChAs: (1 ) { i n > 0} P [ r ] ! . . . { i n > 0} {out > 0} P[r]!...{out+1>0} { o u t < i n < o u t + s i z e } P [ r ] ! . . . { o u t + 1 < i n < o u t + s i z e } < 41 (1') not af fe c t e d (2) P [ r ] ! . . . adds an element of form (s->r,r,.) to h[s->r]. (3) not a f f e c t e d (4) | | h [ s - > r / ( s - > r , r , . ) ] | | i s incremented by 1. (4') not a f f e c t e d (5) From (6) in ChAs we d e r i v e : Val(h[s->r/(s,s->r,nmsg)],out+1) = buf(out mod s i z e ) . Since P[r] ! (CR from buf(out mod s i z e ) ) i s executed, we have: buf(out mod s i z e ) = CR and t h e r e f o r e : Val(h[s->r/(s,s->r,nmsg)],out+1) = CR. Since the CR TPDU i s sent from buf(out mod s i z e ) , we have: Val(h[s->r/(s->r,.,nmsg)],out+1) = CR and t h e r e f o r e : V ( i : 0<i<out+1): Val(h[s->r/(s,s->r,nmsg)],i+1) = Val(h[s->r/(s->r,.,nmsg)],i+1). (5'), (6) (6') not a f f e c t e d (7) ||h[s->r/(s->r,.,nmsg)]|| in c r e a s e s by 1. (7') not a f f e c t e d G5 Sending an expedited TPDU The proof i s analogous to the one i n G4. Summary (G1,...,G5) The r u l e of guarded s e l e c t i o n completes the proof by acc e p t i n g the proofs G1,...G5 and producing: {ChAs} [n(l=1,..,5)gGl-->SGl] {ChAs}. 42 T h i s c o m p l e t e s the p r o o f of ChAs. S e n d i n g or r e c e i v i n g o f a TPDU does not a f f e c t ChAs, which i s t h e r e f o r e an i n v a r i a n t of the c h a n n e l s p e c i f i c a t i o n . As l o n g as no d i s c o n n e c t TPDU i s communicated, a l l TPDUs s e n t a r e r e c e i v e d i n c o r r e c t o r d e r , e x a c t l y once on the o t h e r s i d e . A d i s c o n n e c t TPDU e m p t i e s t h e b u f f e r s . Then the c y c l i c s p e c i f i c a t i o n can s t a r t a n o t h e r t r a n s m i s s i o n s e s s i o n . 5.3 A t r a n s p o r t s t a t i o n i n v a r i a n t The f o l l o w i n g i n v a r i a n t PAs can be t r i v i a l l y p r o v e d t o h o l d a t the i n d i c a t e d p o i n t i n t h e s p e c i f i c a t i o n of t h e t r a n s p o r t s t a t i o n P [ i ] : The s t a t i o n i s i n one of t h e s t a t e s 1+i,3+i,...,13+i and O ^ h b g ^ s i z e and 0^hg<size. T h i s i n v a r i a n t w i l l be used i n s a t i s f a c t i o n p r o o f s i n s e c t i o n 43 5.4 System s a f e t y S a f e t y p r o p e r t i e s have the form "bad t h i n g s w i l l not happen". A s a f e t y p r o p e r t y i n a sys t e m of p a r a l l e l p r o c e s s e s i s e x p r e s s e d by an i n v a r i a n t o v e r t h e whole system of p r o c e s s e s ; i t i s t h e r e f o r e d e r i v e d by r e a s o n i n g o v e r a l l p r o c e s s s p e c i f i c a t i o n s i n v o l v e d . Because i t s c l e a r l y d e f i n e d s y n c h r o n i z a t i o n p r o p e r t i e s CSP i s w e l l s u i t e d t o p r o o f of system s a f e t y i n v a r i a n t s . C r u c i a l f o r the development of sys t e m i n v a r i a n t s a r e t h e l o c a l i n v a r i a n t s . T h i s i s e s p e c i a l l y t r u e i n our example, where t h e l o c a l c h a n n e l i n v a r i a n t ChAs i s needed t o p r o v e the f o l l o w i n g g l o b a l i n v a r i a n t : "A r e c e i v e r , a t any ti m e , has r e c e i v e d o n l y TPDUs s e n t by t h e s e n d e r " . P r o o f : Because of the t i g h t s y n c h r o n i z a t i o n of the I/O o p e r a t i o n s ! and ? i n CSP t h e f o l l o w i n g h o l d s (P [ 1 ] and P [ 2 ] , a r e com m u n i c a t i n g p r o c e s s e s ) : h [ 1 ] / ( 1 , 2 , . ) = h [ 2 ] / ( 1 , 2 , . ) . Both p r o c e s s e s have e x a c t l y the same r e c o r d of t h e i r m u t ual c o m m u n i c a t i o n h i s t o r y . T h i s p r o p e r t y i s i n d e p e n d e n t from any o t h e r p o t e n t i a l l y c o m municating p r o c e s s . T h e r e f o r e we c o n c l u d e f o r our ISO t r a n s p o r t p r o t o c o l s p e c i f i c a t i o n u s i n g CSP: h [ i / ( i , i - > i * 1 , . ) ] = h [ i - > i + ! / ( i , i - > i * 1,.)] and 44 h [ i - > i + l / ( i - > i + 1 , i + 1 , . ) ] = h [ i + l / ( i - > i * l , i + i , . ) ] , i e {0,1}. A sending process P [ i ] sends e x a c t l y what i t s outgoing channel P [ i - > i + 1] r e c e i v e s . A r e c e i v i n g process P [ i * 1] r e c e i v e s e x a c t l y what i t s incoming channel P [ i - > i + l ] sends to i t . Assume that a f t e r completed communication the channels are empty and sender and r e c e i v e r are in a s t a t e "disconnected". (We w i l l prove that these s t a t e s can be reached in a l a t e r subsection by proving that our CSP net s p e c i f i e d p r o t o c o l i s deadlock free and c y c l i c . ) Then, part (5) of the channel i n v a r i a n t ChAs d e l i v e r s : V( i : 0 ^ i < o u t ) : Val(h[s->r/s,s->r,nmsg)],i + 1) Val(h[s->r/(s->r,.,nmsg)],i+1), and, since in=out (empty channels), i t follows that the channel has t r a n s f e r r e d a l l received normal TPDUs in t h e i r c o r r e c t order, no l o s s e s and no d u p l i c a t i o n s have occurred. The same r e s u l t can be deduced from ChAs part (5') for expedited TPDUs. Furthermore, P [ i - > i + l ] r e c e i v e s from P [ i ] only and sends to P [ i * 1 ] and sink only. Therefore: h [ i - > i * l / ( i - > i * l , i * l , . ) ] c h [ i - > i * 1 / ( i , i - > i + 1 , . ) ] , where the "c" r e l a t i o n denotes i n c l u s i o n . h[1] c h[2] i s the case, i f f a l l elements of h[1] are contained in h[2] i n the same order. From the l a s t two proof steps i t can be concluded that h [ i + l / ( i - > i * 1 , i * 1,.)] c h [ i / ( i , i - > i * l , . ) ] . T h i s g l o b a l s a f e t y property expresses the f a c t that a r e c e i v e r 45 r e c e i v e s only TPDUs sent by the sender (no generation of TPDUs during t r a n s m i s s i o n s ) . 5.5 Liveness Liveness p r o p e r t i e s have been explored only very r e c e n t l y [ H a i l p e r n 80], [Owicki 82]. They have the form "good things w i l l happen". In a nonterminating process s p e c i f i c a t i o n l i k e our ISO t r a n s p o r t p r o t o c o l s p e c i f i c a t i o n they can describe c e r t a i n aspects of the system's c y c l i c behavior. For the tr a n s p o r t p r o t o c o l , we w i l l show that the r e c e i v e r h i s t o r y v a r i a b l e s grow forever provided the sender keeps sending. For proving l i v e n e s s p r o p e r t i e s of a p a r a l l e l process s p e c i f i c a t i o n , the most s u i t a b l e t o o l i s temporal l o g i c [Pnueli 77], [ P n u e l i 79], [H a i l p e r n 80], [Owicki 82]. The main advantage of temporal l o g i c i s that i t s formulas are able to' r e f e r to fut u r e s t a t e s of a system. The main operators of temporal l o g i c are: • ( e v e n t u a l l y ) and '• (he n c e f o r t h ) . Let P be a p r e d i c a t e . Then » P means: "P w i l l e v e n t u a l l y become true in the computation". "P means: "P w i l l henceforth be true for a l l s t a t e s of the computation". The two operators can be combined: ••P: " i n f i n i t l y often P", and: ••P: "P becomes true in the future and then w i l l be true f o r e v e r " . The d e s c r i p t i o n of two p r e d i c a t e s necessary for our f u r t h e r i n v e s t i g a t i o n s concludes the i n t r o d u c t i o n i n t o temporal l o g i c . 46 Let S be a statement. Then "at S" ("after S") i s true, i f f the c o n t r o l of the program c o n t a i n i n g S i s at the beginning (end) of S, r e s p e c t i v e l y . When freedom of deadlock i s proven for a p r o t o c o l s p e c i f i c a t i o n (see a subsequent s u b s e c t i o n ) , then i t s components can always make progress. For the a l t e r n a t i v e commands ALT implementing the tra n s p o r t s t a t i o n s , i t s connecting channels and sink i t can th e r e f o r e be assumed: at(ALT) => «after(ALT), af t e r ( A L T ) => •at(ALT). The s t a t i o n , channel and sink s p e c i f i c a t i o n s t h e r e f o r e keep looping f o r e v e r . In the f o l l o w i n g an important l i v e n e s s property of the ISO trans p o r t p r o t o c o l w i l l be proved. Let m be any TPDU, m e {CR,CC,DT,AK,ED,EA}, thus excluding the disconnect TPDUs. For our CSP (net) s p e c i f i c a t i o n t h i s would mean that the system reaches the data t r a n s f e r phase v i a the connection establishment phase and stays there f o r e v e r . Let us assume that one of the tran s p o r t s t a t i o n s P [ i ] sends forever TPDUs m, m e {CR,CC,DT,AK,ED,EA}. Then: | | h [ i / ( i , i - > i * 1 , m ) ] | | --> ». Because of the CSP d e f i n e d s y n c h r o n i z a t i o n p r o p e r t i e s of the I/O commands ? and ! and because P [ i ] sends to P [ i ~ > i + 1 ] only, we have: | | h [ i - > i M / ( i , i - > i + 1 ,m) ] | | — > », and t h e r e f o r e : 47 • • [ ( a f t e r ( i n : = in+1)) or ( a f t e r ( i n e x : = i n e x + 1 ) ) ] . At l e a s t one of inex and in i s incremented i n f i n i t e l y o f t e n . Since only one r e c e p t i o n can occur at every c y c l e of the r e p e t i t i v e command RC implementing a channel, the f o l l o w i n g h olds: •• at(RC) and •• a f t e r ( R C ) . The l o c a l channel i n v a r i a n t ChAs ensures: at(Rc) => out^in^out+size with 0<size<°°, at(RC) => outex<inex<outex+1. So in (inex) can be incremented only a f i n i t e number of times without incrementing out (outex) and v i c e v e r s a . Therefore: •• a f t e r ( i n : = i n + l ) <=> •• after(out:=out+1), and • • a f t e r ( i n e x : = inex+1) < = > •• after(outex:=outex+1). . It can t h e r e f o r e be concluded that | |h[i->i + 1 / ( i - > i * 1 , i + l,m)]| | --> «. Because of the s y n c h r o n i z a t i o n p r o p e r t i e s of the CSP I/O commands we have: | | h [ i + 1 / ( i - > i * 1 , i + 1 , m ) ] f | --> ». The f o l l o w i n g c o n c l u s i o n t h e r e f o r e holds: If a sender P [ i ] keeps sending f o r e v e r , then an u n l i m i t e d number of TPDUs are rec e i v e d at the r e c e i v e r P [ i + l ] , i e { 0 , 1 } , disconnect TPDUs excluded. C o r o l l a r y : The s p e c i f i c a t i o n of P [ i ] shows that any DT or ED TPDU r e c e i v e d t r i g g e r s an immediate acknowledgement. Therefore, i f the sender keeps sending f o r e v e r , i t w i l l r e c e i v e an u n l i m i t e d number of / 48 acknowledgements. 5.6 D u p l i c a t i o n , d i s o r d e r i n g and l o s i n g of TPDUs S i n c e t h e f o l l o w i n g 3 theorems a r e easy t o p r o v e u s i n g the same t e c h n i q u e s as i n the p r o o f of t h e l o c a l c h a n n e l i n v a r i a n t ChAs, o n l y t h e i r i n f o r m a l o u t l i n e s a r e g i v e n . Theorem 1: No TPDUs a r e l o s t , i f no DR, DC TPDUs a r e s e n t . P r o o f o u t l i n e : The e x c l u s i o n of DR, DC TPDUs i m p l i e s t h a t no TPDUs a r e se n t t o s i n k , making P [ i * 1] t h e o n l y r e c i p i e n t of P [ i - > i + l ] ' s TPDUs. I n c r e m e n t a t i o n of out ( o u t e x ) and s e n d i n g of a normal ( e x p e d i t e d ) TPDU happen- i n the same gu a r d e d command. T h e r e f o r e no i n c r e m e n t a t i o n of out ( o u t e x ) can o c c u r w i t h o u t s e n d i n g t h e TPDU i n buf o r b u f e x . T h e r e f o r e no TPDU i s l o s t . Theorem 2: No TPDU i s d u p l i c a t e d . P r o o f o u t l i n e : I n c r e m e n t a t i o n of out ( o u t e x ) and s e n d i n g of a normal ( e x p e d i t e d ) TPDU happen i n the same g u a r d e d command. T h e r e f o r e any s e n d i n g of a normal ( e x p e d i t e d ) TPDU from a_ c h a n n e l t r i g g e r s i n c r e m e n t a t i o n of out ( o u t e x ) . T h e r e f o r e no normal ( e x p e d i t e d ) TPDU i s s e n t w i t h the same v a l u e of out ( o u t e x ) . T h e r e f o r e no TPDU i s d u p l i c a t e d . Theorem 3: TPDUs do not become d i s o r d e r e d by a c h a n n e l . P r o o f o u t l i n e : 49 I n c r e m e n t a t i o n of out (o u t e x ) and s e n d i n g of a normal ( e x p e d i t e d ) TPDU happen i n the same gu a r d e d command. The o n l y o p e r a t i o n on out (o u t e x ) i n s i d e the l o o p i s i n c r e m e n t a t i o n by 1 . D i s o r d e r i n g of a TPDU would i n v o l v e i t s s e n d i n g , when out has a c e r t a i n v a l u e n a f t e r a n o t h e r TPDU has been sent w i t h out>n. T h i s i s not p o s s i b l e . T h e r e f o r e TPDUs do not become d i s o r d e r e d by a c h a n n e l . C o r o l l a r y : S i n c e no TPDUs become d u p l i c a t e d , d i s o r d e r e d or l o s t i n t h e d a t a t r a n s f e r phase, a sender w i l l r e c e i v e acknowledgments f o r a l l i t s TPDUs i n the c o r r e s p o n d i n g o r d e r , as l o n g as no d i s c o n n e c t TPDUs a r e s e n t . 5.7 S a t i s f a c t i o n p r o o f s P r o o f s of p a r t i a l c o r r e c t n e s s a r e not enough t o c a p t u r e t h e n o t i o n t h a t s y n c h r o n i z e d I/O commands i n CSP s p e c i f y d i s t r i b u t e d a s s i g n m e n t [ L e v i n 8 1 ] . C o n s i d e r the f o l l o w i n g c o m m u n i c a t i o n between two p r o c e s s e s S1 and S 2 : S1 ! k || S 2 ? (k i n t o x ) . S1 sends v a l u e k t o l o c a l v a r i a b l e x of S 2 . L e t us assume t h a t {P} S i l k {Q} and {R} S 2 ?.(k i n t o x) {S} have been p r o v e d . I f the communication i s c o n s i d e r e d as d i s t r i b u t e d a s s i g n m e n t , then -{ ( Q & S ) £ } S 1 ! k || S 2 ? ( k i n t o x) {Q&S} i s t r u e . To p r o v e t h e c o n n e c t i o n between t h e p r e c o n d i t i o n s P and R and 50 the p o s t c o n d i t i o n s Q and S i n t h e d i s t r i b u t e d e n v i r o n m e n t , we have t o p r o v e : {P&R} SI ! k || S2 ? (k i n t o x {Q&S} T h i s can be done by p r o v i n g (Q&S)* => (P&R) and a p p l y i n g the r u l e of c o n s e q u e n c e . C o n s i d e r the commun i c a t i o n of a normal TPDU between P [ i ] and P [ i - > i + U ] i n the ISO t r a n s p o r t s p e c i f i c a t i o n . L e t GC be the guarded command s e n d i n g a DT TPDU i n p r o c e s s P [ i ] and l e t GP be t h e g u a r d e d command r e c e i v i n g a DT TPDU i n p r o c e s s P [ i - > i + l ] . Then, t o show {ChAs & PAs} GC || GP {ChAs & PAs} we have t o p r o v e {ChAs & i n < s i z e + o u t & inex=outex & PAs & hbg>0 & s t a t e = l } => ( r , . b u f ( i n mod s i z e ) , i n , h [ i - > i * 1] ' h [ i ] , h b g , l t SDT, in+1 , h [ i - > i • 1 ] • ( i , i - > i * 1 ,DT) t' r s h [ i]«(i., i - > i * l , DT) ,hbg-1 ' P r o o f : The p r o o f c o n s i s t s of s i m p l e s u b s t i t u t i o n s i n ChAs and PAs. F o r e v e r y s y n c h r o n i z e d I/O p a i r of t h e ISO t r a n s p o r t p r o t o c o l s p e c i f i c a t i o n a s a t i s f a c t i o n p r o o f can be c o n d u c t e d . 51 5.8 Freedom from deadlock A number of automatic or h a l f automatic e v a l u a t i o n t o o l s f o r p r o t o c o l s p e c i f i c a t i o n s a l r e a d y e x i s t [Sunshine 8 2 ] , [Good 78], [Cheza 7 9 ] . The l a t t e r system i s an i n t e r a c t i v e v a l i d a t i o n system f o r P e t r i nets c a l l e d OGIVE. Among numerous o t h e r f e a t u r e s , OGIVE p r o v i d e s a way to v a l i d a t e g l o b a l p o r p e r t i e s of a P e t r i net l i k e freedom from d e a d l o c k , p r o p e r n e s s , boundedness and/or s a f e n e s s . For an a p p l i c a t i o n of OGIVE to r e s t r i c t e d t r a n s p o r t p r o t o c o l components, see [Jvirg 8 4 ] . G l o b a l p r o p e r t i e s of P e t r i n e t s are d e f i n e d i n [ D i a z 8 2 ] . The program "cspnet" (see Appendix 1) extends one of OGIVE's a n a l y s i n g methods (enumeration) by a p p l y i n g i t to CSP n e t s . W r i t t e n i n P a s c a l r a t h e r than i n F o r t r a n l i k e OGIVE, "cspnet" t a k e s a g l o b a l view a t a CSP net. I t d e f i n e s a s t a t e as c o n s i s t i n g of the c u r r e n t marking of the CSP net's u n d e r l y i n g P e t r i net and a c e r t a i n , u s e r - d e f i n e d c o m b i n a t i o n of l o c a l p r o c e s s v a r i a b l e s . B e g i n n i n g w i t h a user-chosen i n i t i a l s t a t e , the program enumerates a l l s t a t e s r e a c h a b l e by f i r i n g the CSP n e t ' s enabled s y n c h r o n i z a t i o n s . A r e a c h a b i l i t y graph of a l l the reached s t a t e s i s b u i l t and a t the same time the net i s checked f o r boundedness and s a f e n e s s . When a l l the r e a c h a b l e markings have been enumerated and t h e r e f o r e the whole r e a c h a b i l i t y graph i s b u i l t up, the r e a c h a b i l i t y graph i s examined t o determine, i f the net i s p r o p e r . I f the net i s proper and a l l s y n c h r o n i z a t i o n s have been f i r e d then the net i s l i v e as w e l l . A good summary of the P e t r i net based models and t h e i r use f o r p r o t o c o l s p e c i f i c a t i o n can be found i n [Diaz 8 2 ] . 52 The CSP net s p e c i f i c a t i o n of the ISO tra n s p o r t p r o t o c o l has been examined by the program "cspnet". The net has been found to be deadlockfree, proper and safe. Since the net has been found to be not l i v e , but proper, some s y n c h r o n i z a t i o n s have never been f i r e d during e v a l u a t i o n . A l l of them are syn c h r o n i z a t i o n s , which are used to empty channels before a disconnect phase becomes completed. They w i l l be necessary for future extensions of the model, when d u p l i c a t e frames w i l l be permitted in the channel. Those w i l l be e i t h e r d i s c a r d e d or cause an ERR or REJ TPDU to be sent. Further documentation about "cspnet", e x p l a i n i n g i t s algorithms in some d e t a i l , can be found in Appendix 3. 5.9 Summary: T o t a l c o r r e c t n e s s A proof of t o t a l c o r r e c t n e s s of a p a r a l l e l process s p e c i f i c a t i o n in CSP c o n s i s t s of (compare with Levin [81]): ( i ) a p a r t i a l c o r r e c t n e s s proof for every relevant component process ( a s s e r t i o n proofs of ChAs and PAs), ( i i ) a p a r t i a l c o r r e c t n e s s proof for the whole p a r a l l e l system (system s a f e t y ) , ( i i i ) a l i v e n e s s proof for the whole system ("something i s accomplished by the p a r a l l e l system"), ( i v ) a s a t i s f a c t i o n proof, (v) a noninterference proof (not necessary here, since the axiomatics used does not allow shared a u x i l i a r y v a r i a b l e s ) , and 53 ( v i ) p r o o f of a b s e n c e of d e a d l o c k . A l l t h e s e p a r t s have been a c c o m p l i s h e d h e r e . The f o r m a l ISO t r a n s p o r t p r o t o c o l s p e c i f i c a t i o n p r o p o s e d i n t h i s t h e s i s ( w h i c h c o v e r s a s i g n i f i c a n t s u b s e t o f t h e E n g l i s h p r o s e s p e c i f i c a t i o n ) i s t h e r e f o r e t o t a l l y c o r r e c t . 54 CHAPTER 6j_ CONCLUSION In t h i s t h e s i s , a s i g n i f i c a n t ISO tr a n s p o r t p r o t o c o l subset has been formally s p e c i f i e d and r i g o r o u s l y v e r i f i e d . To accomplish t h i s goal, a combined approach has been used. F i r s t , we have used Hoare's communicating s e q u e n t i a l processes for a programming language s p e c i f i c a t i o n of the p r o t o c o l . CSP's embedded command types, e s p e c i a l l y D i j k s t r a ' s guarded command and the synchronizing input and output commands have proved to be very s u i t a b l e to s p e c i f y a communication p r o t o c o l f o r m a l l y . Second, a P e t r i net based p r e d i c a t e / t r a n s i t i o n net, c a l l e d a CSP net, has been developed to s p e c i f y the c o n t r o l s t r u c t u r e of a p r o t o c o l . .CSP nets r e l y h e a v i l y on coupled t r a n s i t i o n s of. d i f f e r e n t processes ( s y n c h r o n i z a t i o n s ) to simulate the behavior, of CSP's input and output commands. The two s p e c i f i c a t i o n methods have been used to produce - a compatible, dual s p e c i f i c a t i o n of a major subset of the ISO tran s p o r t p r o t o c o l . Subsequently the dual model has been v e r i f i e d . An axiomatic semantics for CSP was used to de r i v e i n v a r i a n t s for both the tr a n s p o r t s t a t i o n and the channel s p e c i f i c a t i o n s . System s a f e t y and l i v e n e s s p r o p e r t i e s , reasoning over the whole process system, have a l s o been checked f o r . A d d i t i o n a l l y , the CSP net s p e c i f i a t i o n of the ISO transport p r o t o c o l has been v a l i d a t e d f o r g l o b a l p r o p e r t i e s such as absence of deadlock and properness. The combined r e s u l t s i n d i c a t e t o t a l c o r r e c t n e s s of our ISO t r a n s p o r t p r o t o c o l s p e c i f i c a t i o n . 55 A n a t u r a l extension of t h i s thesis,^, the v e r i f i c a t i o n of the complete ISO t r a n s p o r t p r o t o c o l , can be c a r r i e d out by i n c l u d i n g d u p l i c a t e d , l o s t or d i s o r d e r e d TPDUs and recovery from the r e s u l t i n g erroneous s i t u a t i o n s . T h i s can be accomplished by i n t r o d u c i n g processes l i k e "source" f o r producing TPDUs "out of the blue" and "sink" for erroneously e x t r a c t i n g TPDUs from a channel. Another p o s s i b l e research path could explore the p o s s i b i l i t y of guarded commands being parts of the command l i s t C of a guarded command G-->C down to a r b i t r a r y depths. Some problems have to be overcome here, since a process system could deadlock at a r e l a t i v e l y deep l e v e l of guarded commands. Look-ahead procedures to recognize such a "deep" deadlock are important to develop algorithms which t r y to avoid them. A s s e r t i o n proof methods have the disadvantage that they are done by hand i n t r o d u c i n g ' a l l the kinds of e r r o r s humans commonly commit. Automating these methods would increase t h e i r speed and r e l i a b i l i t y s i g n i f i c a n t l y . T h i s complex problem i s s t i l l an open research area. The l a s t , but not the l e a s t purpose of t h i s t h e s i s l i e s in proposing a methodical approach: State t r a n s i t i o n and programming language models should be combined to a compatible, dual model to explore and allow for the v e r i f i c a t i o n of every p o s s i b l e aspect of behavior of a communication p r o t o c o l . Only in t h i s way can we be reasonably sure that the p r o t o c o l algorithms-we design and implement w i l l work c o r r e c t l y . 56 REFERENCES• [Apt 80] K. R. Apt, N. Francez, W. P. de Roever: A proof system for CSP, ACM Trans, on Prog. Lang and Systems, V o l . 2, No. 3, J u l y 80, pp. 359-385 [Bart 69] K. A. B a r t l e t t , R. A. Scantlebury, P. T. Wilkinson: A note on f u l l - d u p l e x t r ansmission over h a l f - d u p l e x l i n k s , CACM 12 (1969), pp. 260-261 [Bochmann 78] G. v. Bochmann: F i n i t e s t a t e d e s c r i p t i o n of communication p r o t o c o l s , Computer Networks 2, Oct 78, pp. 361-372 j [Bochmann 80] G. v. Bochmann: A general t r a n s i t i o n model for p r o t o c o l s and communication s e r v i c e s , IEEE Trans, on Comm., Vol COM-28, A p r i l 1980, pp. 624-631 [Cheza 79] B. C h e z a v i e l - P r a d i n : Un O u t i l graphique i n t e r a c t i f pour l a v a l i d a t i o n des systemes a e v o l u t i o n p a r a l l e l e d e c r i t s par reseaux de P e t r i (OGIVE), These de Docteur-Ingenieur, U n i v e r s i t e Paul S a b a t i e r , Toulouse, December 1 979 [Clipsham 76] W. W. Clipsham, M. L. Narraway: Datapac Network Overview, T h i r d I n t e r n a t i o n a l Conference on Computer Communicatins, Toronto, Canada, August 1976 [Diaz 82] M. Diaz: Modeling and a n a l y s i s of communication and cooperation p r o t o c o l s using P e t r i net based models, Computer Networks 6(1982), pp. 419-441 [ D i j k s t r a 75] E. W. D i j k s t r a : Guarded commands, nondeterminacy and formal d e r i v a t i o n of programs, CACM 18(1975), pp. 453 -457 [Genrich 81] H. J . Genrich, K. Lautenbach: System modelling with h i g h - l e v e l P e t r i nets, T h e o r e t i c a l Comp. S c i 13(1981), pp. 1 0 9 - 1 3 6 • [Good 78] D. I. Good, R. M. Cohen: V e r i f i a b l e communications p r o c e s s i n g in Gypsy, Compcom 78, pp. 28-35 [Hai l p e r n 80] 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 29, 1980, pp. 18-28 [Hail p e r n 81] 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 Research Report RC 8726, 1981 [Hoare 78] C. A. R. Hoare: Communicating Sequential Processes, CACM, Aug. 78, Vol 21, No. 8, pp. 666-677 57 [Jensen 81] K. Jensen: Coloured P e t r i nets and the i n v a r i a n t method, T h e o r e t i c a l Comp. S c i . 14(1981), p. 317-337 [Jensen 8 1 a ] K. Jensen: How to f i n d i n v a r i a n t s for coloured P e t r i nets, LNCS 118, Springer V e r l a g 1981, pp. 327 [Jiirg 84] W. Jiirgensen, S. T. Vuong: Formal s p e c i f i c a t i o n and v a l i d a t i o n of ISO t r a n s p o r t p r o t o c o l components, using P e t r i nets, ACM SIGCOMM'84 Symposium, Montreal, June 1984 [Kieburtz 79] R. B. K i e b u r t z , A. S i l b e r s c h a t z : Comments on CSP, ACM Trans, on Prog. Lang. 1(1979), pp. 218-225 [Kroger 80] F. Kroger: I n f i n i t e proof r u l e s for loops, Acta Informatica 14 (1980), pp. 371-389 [Landw 82] L. Landweber, M. Solomon: The use of m u l t i p l e networks in CSNET, Proceedings of Compcon Spring 1982 (Feb. 1982) [Lautenbach- 74] K. Lautenbach, H. Schmid: Use of P e t r i nets for proving c o r r e c t n e s s of concurrent process systems, Proc. IFIP Congres 74, North-Holland Publ., Amsterdam 1974, pp. 187-191 [Levin 81] G. M. L e v i n , D. G r i e s : A proof technique for communicating s e q u e n t i a l processes., Acta Informatica 15(1981), pp. 281-302 [McQuillan 77] J . M. McQuillan, D. C. Walden: The ARPA network design d e c i s i o n s , Computer Networks 1(1977), pp. 243-289 [Me r l i n 79] P. M. M e r l i n : S p e c i f i c a t i o n and v a l i d a t i o n of p r o t o c o l s , IEEE Trans, on Communications, V o l . COM-27, No. 11, Nov. 1979, pp. 1671-1680 [Owicki 82] 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) pp. 455-495 [Peterson 77] J . L. Peterson: P e t r i nets, Computing Surveys 9(1977), pp. 223-252 [ P e t r i 62] C. A. P e t r i : Kommunikation mit Automaten, S c h r i f t e n des Rheinisch-Westfalischen I n s t i t u t e s fur Instrumentelle Mathematik an der U n i v e r s i t a t Bonn, 1962 [Pnueli 77] A. P n u e l i : The temporal l o g i c of programs. The 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode I s l a n d , IEEE 1977, pp. 46-57 [Pnue l i 79] 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, Evian-, J u l y 1979 58 [Pouzin 82] L. Pouzin (ed): 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 for computer communications, V o l . 2, North-Holland, 1982 [Sounda] N. Soundararajan: Axiomatic semantics for communicating s e q u e n t i a l processes, Research Report, I n s t i t u t e of Informatics, U n i v e r s i t y of Oslo [Sounda 83] N. Soundararajan: Correctness proofs of CSP programs, T h e o r e t i c a l Comp. S c i . , 24(1983), pp. 131-142 [St u d n i t z 83] P. V. S t u d n i t z : Transport p r o t o c o l s : Their performance and status in i n t e r n a t i o n a l s t a n d a r d i z a t i o n (July 1982), Computer Networks 7(1983) pp. 27-35 [Sunshine 82] C. A. Sunshine, D. H. Thompson, R. W. E r i c k s o n , S. L. 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 in 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., Vol SE-8, No. 5, Sept. 1982, pp. 460-489 [Vuong 83] S. T. Vuong, D. 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, Journal of Telecommunication Networks, Summer Issue, 1983 [Vuong 84] S. T. Vuong, D. D. Cowan: UNISPEX: A u n i f i e d model for 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 , INFOCOM Conference, San F r a n c i s c o , A p r i l 1984 [Wald 77] R. Waldinger:-Achieving s e v e r a l goal simultaneously, Machine I n t e l l i g e n c e 8, pp. 94-136, E. Elcock and D. M i t c h i e (eds.), E l l i s Horwood, 1977 [IS01] DIS 7499, Data Processing Systems - Open Systems Interconnection - Basic Reference Model, Computer Networks 5(1981), pp. 8 1 - 1 1 8 [ISO NS] ISO/TC97/SC16 N2610 (Oct. 82). Dat Processing Systems - Open Systems Interconnection - Network S e r v i c e D e f i n i t i o n [ISO TP] DP 8073, ISO/TC97/SC16 N1169 (June 82). Data Processing Systems - Open Systems Interconnection Transport P r o t o c o l S p e c i f i c a t i o n [ISO -TS] DP 8072, ISO/TC97/SC16 N1162 (June 82). Data Processing Systems - Open Systems Interco n n e c t i o n Transport Service D e f i n i t i o n [ISO SP] DP 8327, ISO/TC97/SC16 N1167 (5/9/83) Data Processing Systems - Open System Interconnection - Basic Connection Oriented Session P r o t o c o l S p e c i f i c a t i o n 59 APPENDIX 1: Program "cspnet" and data program cspnet (input, output); {The program examines a CSP net by enumeration of i t s states, A s t a t e of a CSP net i s made up by the marking of i t s underlying P e t r i net and a combination of the values of l o c a l process v a r i a b l e s . Comments about a procedure w i l l o f ten appear at the s t a r t of the procedure body.} const maxpl=20; maxpfollow = 17; maxdesc=l5; maxtr = 117; maxtfollow = 2 ; maxanc = 15; maxsync= 93; maxproc = 6; maxmark = 1000; s i z e = 1; size_1 = 0; type message = (CR,CC,DT,AK,ED,EA,DR,DC,undef); le a = (no,block); p l a r r a y = array (.1..maxpl.) of i n t e g e r ; t r a r r a y = array (.1..maxtr.) of boolean; synarray= array (.1..maxsync.) of boolean; markarray = array(.1..maxmark.) of boolean; {A node in the r e a c h a b i l i t y graph i s a record of type ma. It c o n t a i n s p o i n t e r s to a l l i t s ancestors and successors (desc, anc) and an array ( b y f i r e ) to store the s y n c h r o n i z a t i o n s used to expand the node to a p a r t i c u l a r successor s t a t e . Copies of a l l l o c a l v a r i a b l e s of the process system and the P e t r i net marking of the s t a t e are part of the node. Some boolean a u x i l i a r y v a r i a b l e s are used when the r e a c h a b i l i t y graph i s examined l a t e r . } maptr = Ma; ma = record numb,nanc,ndesc : in t e g e r ; desc: array (.1..maxdesc.) of Ma; anc : array (.1..maxanc.) of Ma; marking : p l a r r a y ; b y f i r e : array (.1..maxdesc.) of i n t e g e r ; stop : l e a ; hg1,hbg1,hg2,hbg2,inLR,outLR,inexLR,outexLR, inRL,outRL,inexRL,outexRL : i n t e g e r ; bufexLR,bufexRL : message; bufLR,bufRL : a r r a y ( . 0 . . s i z e _ 1 . ) of message; prop,propcheck, l i v , l i v e c h e c k : boolean end; {Declaration of v a r i a b l e s to take the CSP net input and of g l o b a l a u x i l i a r y v a r i a b l e s . } var n p l , n t r , n s y n c , n p f o l l o w , n t f o l l o w , n p r o c , l a s t m a r : i n t e g e r ; safe,bounded,proper,live,blocked : boolean; p l f o l l o w : a r r a y (.1..maxpl,1..maxpfollow.) of i n t e g e r ; t r f o l l o w : a r r a y ( . 1 . . m a x t r , 1 . . m a x t f o l l o w . ) of i n t e g e r ; s y n c : a r r a y (.1..maxsync,1..maxproc.) of i n t e g e r ; mark : p l a r r a y ; s y n c f i r e d : s y n a r r a y ; m a r k r o o t : maptr; x h g l , x h b g 1 , x h g 2 , x h b g 2 , x i n L R , x o u t L R , x i n R L , x o u t R L , x i n e x L R , x o u t e x L R , x i n e x R L , x o u t e x R L : i n t e g e r ; x b u f e x L R , x b u f e x R L : message; x b u f L R , x b u f R L : a r r a y ( . 0 . . s i z e _ 1 . ) of message; { P r o c e d u r e a l l o c i s used t o c r e a t e a new node d u r i n g the r e a c h a b i l i t y g r a ph b u i l t - u p . The new node's v a r i a b l e s a r e g i v e n v a l u e s computed d u r i n g the e x p a n s i o n of i t s p a r e n t node.} a l l o c ( v a r i n t e g e r ; do := l a s t m a r ; = n i l t h e n 0;. p r o c e d u r e v a r i : b e g i n new(p); w i t h p@ b e g i n numb i f c p ndesc anc ( . f o r i f o r i f o r i f o r i f o r i:= npl+1 s t o p := no; hg1 := xhg1; h b g l := xhbgl hg2 := xhg2; p:maptr; cp : maptr; v a r m a r : p l a r r a y ) ; nanc ;= 0 e l s e nanc 1 . ) :=2 : = 1 : = 1 := 1 t o t o t o t o cp; maxanc do anc( . i . ) maxdesc do d e s c ( . i maxdesc do b y f i r e ( n p l do m a r k i n g ( . i : = n i l ; ) := n i l ; i . ) := 0; ) : = ma r ( to maxpl do m a r k i n g ! . i . ) hbg2 i n L R outLR: inexLR : outexLR inR L := outRL:= i n e x R L : outexRL bufexLR bufexRL f o r i := f o r i : = xhbg2; x i n L R ; xoutLR; = x i n e x L R ; := xoutexLR; x i n R L ; xoutRL; = x i n e x R L ; := xoutexRL; := xbufexLR; := xbufexRL; 0 t o s i z e _ 1 0 t o s i z e 1 do b u f R L ( . i . ) := xbufRL( do b u f L R ( . i . ) := xbufLR( p r o p := f a l s e ; p r o p c h e c k := f a l s e ; l i v := f a l s e ; l i v e c h e c k := f a l s e end 61 end; { P r o c e d u r e i n i t r e a d s th e CSP net i n , i n i t i a l i z e s the g l o b a l a u x i l i a r y v a r i a b l e s and a l l o c a t e s the i n i t i a l r o o t node.} p r o c e d u r e i n i t ; v a r i , j : i n t e g e r ; b e g i n r e a d l n ( n p l , n t r , n s y n c , n p f o l l o w , n t f o l l o w , n p r o c ) ; l a s t m a r := 1; s a f e := t r u e ; bounded := t r u e ; p r o p e r := t r u e ; l i v e := t r u e ; b l o c k e d := f a l s e ; f o r i : = l t o maxpl do f o r J:=1 t o m a x p f o l l o w do p l f o l l o w ( . i , j . ) : = 0 ; f o r i:=1 t o n p l do f o r j:=1 t o n p f o l l o w do' r e a d ( p l f o l l o w ( . i , j . ) ) ; r e a d l n ; f o r i:=1 t o maxtr do f o r j:=1 t o m a x t f o l l o w do t r f o l l o w ( . i , j . ) : = 0 f o r i : = 1 t o n t r do f o r j : = 1 t o n t f o l l o w - d o r e a d ( t r f o l l o w ( . i , j . ) ) r e a d l n ; f o r i:=1 t o maxsync do f o r j:=1 t o maxproc do s y n c ( . i , j . ) : = 0 ; f o r i:=1 t o nsync do f o r j:=1 t o n proc do r e a d ( s y n c ( . i , j . ) ) ; r e a d l n ; f o r i:= 1 t o n p l do r e a d ( m a r k ( . i . ) ) ; r e a d l n ; . f o r i:=npl+1 t o maxpl do m a r M . i . ) := - 1 ; -f o r i:=1 t o maxsync do s y n c f i r e d ( . i . ) := f a l s e ; xhgl := 0; xhbg1 := 0; xhg2 := 0; xhbg2 := 0; x i n L R := 0; xoutLR := 0; x i n R L := 0; xoutRL := 0; x i n e x L R := 0; x outexLR := 0; < J x i n e x R L := 0; i xoutexRL := 0; ) ' x b u f e x L R := undef; x b u f e x R L := undef; f o r i := 0 t o s i z e _ 1 do x b u f L R ( . i mod s i z e . ) := undef; f o r i := 0 t o s i z e _ 1 do x b u f R L ( . i mod s i z e . ) := undef; a l l o c ( m a r k r o o t , n i l , m a r k ) end; 62 {Procedure b u i l d l e a v e s b u i l d s the r e a c h a b i l i t y graph. D e t a i l e d d e s c r i p t i o n at the s t a r t of i t s procedure body.} procedure b u i l d l e a v e s (cp:maptr; var l a s t m a r : i n t e g e r ) ; var found : boolean; p, pfound: maptr; i,j,s,numleav : i n t e g e r ; ts : t r a r r a y ; cs : synarray; nextmar : p l a r r a y ; checkarray : markarray; {Procedure t r a n s i b determines the enabled t r a n s i t i o n s of a current s t a t e and stores them in the array t s . I t determines f o r every t r a n s i t i o n , i f i t s input places hold a s u f f i c i e n t number of tokens and i f i t s enabling p r e d i c a t e s are true (using the f u n c t i o n locpred).} procedure t r a n s i b (var m:plarray; var c. : maptr; var t s : t r a r r a y ) ; var i , j : i n t e g e r ; funct ion var b : begin with c@ begin case i of 1 , 2, 16, 17, 31, 32, 50, 51 , 65, 66, lo c p r e d ( i boolean; do i n t e g e r ; var c : maptr) : boolean; 3, 18, 33 52, 67 34: 36, 1 0 1 2 25 35 47 : 49 : 62, 71: 72, 73, 75, 76, 79, 80 : 83 : 37 74: 77 4, 19 38 53 68 107,108,109,110 78 5, 20, 39, 54, 69, 111, b b b b b b b b b b b : = b : = 6, 7, 8, 9, 11, 13, 14, 15, 21 , 22, 23 ,.24, 26, 27 , 28 , 29, 40, 41, 42, 43, 44, 45, 46, 48 55, 56, 57, 58, 59, 60, 61, 63 70, 81, 82, 97, 98,115,116: b := true; 112,113,114: = f a l s e ; = (hbg1 > 0 ) ; = (hg1 < s i z e ) ; = ( (hg1 > 0). or (hbgl > 0) ) ; = ((hg1 = 0) and (hbgl = 0 ) ) ; = (hbg2 > 0); = (hg2 < s i z e ) ; = ((hg2 > 0) or (hbg2 > 0 ) ) ; = ((hg2 = 0) and (hbg2 = 0 ) ) ; = ((inLR < outLR + s i z e ) and (inexLR = outexLR)); ((inLR <= outLR +size) and (inexLR = outexLR)); ((outLR < inLR) 30, 64 63 84 : 85 : 86 : 87 88 89 90 91, 92, 95, 96: 99 : 100 : 101 : 102 : 103 : 104 : 105 : 106 : end; l o c p r e d end end; and and 93, 94: and b b ( b u f L R ( . b ( b u f L R ( , b and and and (outexLR = inexLR) and ( b u f L R ( . o u t L R mod s i z e . ) = CR)) := ( ( o u t L R < inLR) and (outexLR = i n e x L R ) and (bufLR( .outLR mod s i z e . ) = C O ) := ( ( o u t L R < inLR) and (outexLR = i n e x L R ) and ( b u f L R ( . o u t L R mod s i z e . ) = DT)) : = ( ( o u t L R < inLR) and (outexLR = i n e x L R ) ( b u f L R ( . o u t L R mod s i z e . ) = AK)) := ( ( o u t e x L R < inexLR) and (bufexLR = ED)) = ( ( o u t e x L R < inexLR) and (bufexLR = EA)) = ( ( o u t L R < inLR) outLR mod s i z e . ) = DR)) = ( ( o u t L R < inLR) outLR mod s i z e . ) = DC)) = ( ( i n R L < outRL + s i z e ) and ( i n e x R L = o u t e x R L ) ) = ( ( i n R L <= outRL + s i z e ) and ( i n e x R L = o u t e x R L ) ) := ( ( o u t R L < inRL) and (outexRL = i n e x R L ) and ( b u f R L ( . o u t R L mod s i z e . ) = CR) ) := ( ( o u t R L < inRL) and (outexRL = i n e x R L ) and (buf RL (. outRL mod s i z e . ) = C O ) := ( ( o u t R L < inRL) and (outexRL = i n e x R L ) and ( b u f R L ( . o u t R L mod s i z e . ) = DT) ) := ( ( o u t R L < inRL) and (outexRL = i n e x R L ) and ( b u f R L ( . o u t R L mod s i z e . ) = AK)) = ( ( o u t e x R L < inexRL) and (bufexRL = ED)) = ( ( o u t e x R L < inexRL) and (bufexRL = EA)) b := ( ( o u t R L < inRL) ( b u f R L ( . o u t R L mod s i z e . ) = DR)) b := ( ( o u t R L < inRL) ( b u f R L ( . o u t R L mod s i z e . ) = DC)) b e g i n f o r i : = 1 t o maxtr do ts("". i._. ) := t r u e ; f o r i:=1 t o n p l do f o r j:=1 t o n p f o l l o w do 64 b e g i n i f p l f o l l o w ( . i , j . ) <> 0 then i f ( m ( . i . ) < 1 ) or (. l o c p r e d ( p l f o l l o w ( . i , j . ) , c ) ) t h e n t s ( . p i f o l l o w ( . i , j . ) . ) := f a l s e end end; { P r o c e d u r e s y n c s i b , u s i n g the i n f o r m a t i o n , which t r a n s i t i o n s a r e e n a b l e d , d e t e r m i n e s , which s y n c h r o n i z a t i o n s a r e e n a b l e d . A s y n c h r o n i z a t i o n i s e n a b l e d , i f f it.s t r a n s i t i o n s a r e enabled.} p r o c e d u r e s y n c s i b ( v a r t s r t r a r r a y ; v a r c s : s y n a r r a y ) ; v a r i , j : i n t e g e r ; b e g i n f o r i : = l t o nsync do c s ( . i . ) := t r u e ; f o r i : = 1 t o nsync do f o r J : = 1 t o nproc do b e g i n i f c s ( . i . ) and ( s y n c ( . i , j . ) <> 0) then c s ( . i . ) := c s ( . i . ) and t s ( . s y n c ( . i , j . ) . ) end end;-"' { P r o c e d u r e s u c p l d e t e r m i n e s the m a r k i n g of the o u t p u t p l a c e s of a f i r e d t r a n s i t i o n . } p r o c e d u r e s u c p l ( t : i n t e g e r ; v a r m a r : p l a r r a y ) ; v a r i : i n t e g e r ; b e g i n i : = 1 ; w h i l e ( t r f o l l o w ( . t , i . ) <> 0) and ( i <= n t f o l l o w ) do b e g i n ma r-(. t r f o l l o w (. t , i . ) . ) := m a r ( . t r f o l l o w ( . t , i . ) . ) + 1 ; i := i + 1 end end; { P r o c e d u r e p r e d p l d e t e r m i n e s th e m a r k i n g of the i n p u t p l a c e s of a f i r e d t r a n s i t i o n . } p r o c e d u r e p r e d p l ( t : i n t e g e r ; v a r m a r : p l a r r a y ) ; v a r i , j : i n t e g e r ; b e g i n f o r i : = 1 t o n p l do b e g i n j := 1 ; w h i l e ( p l f o l l o w ( . i , j . ) <> 0) and ( j <= n p f o l l o w ) do b e g i n i f p l f o l l o w ( . i , j . ) = t 65 then mar(.i.) := mar(.i.) -1; j := j + 1 end end end; {Procedure l o c a c t i o n executes the a c t i o n s of a f i r i n g t r a n s i t i o n t.} procedure l o c a c t i o n ( t : i n t e g e r ) ; var i : i n t e g e r ; procedure drop; begin end; begin case t of 1, 2, 3, 9, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 26, 27, 28, 29, 30, 31, 32, 33, 35, 36, 37, 38, 39, 40, 46, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 63, 64, 65, 66, 67, 68, 69, 70, 72, 73, 74,107, 108,109,110,111,112,113,114,115,116: • begin end; 4: xhg1 := xhg1 + . 1; • 5,7:' xhg-1 := 0; 6: begin xhbgl := 1; xhgl := 1 end; 8: xhbg 1 : =• 1 ; . 1 0 : xhbgl :=' xhbgl - M ; 11: xhbgl := xhbgl + 1; 1 2 : xhgl :=.xhgl + 1; 25,34: begin xhgl := 0; xhbgl := 0 end; 41: xhg2 := xhg2 + 1; 42,44: xhg2 := 0; 43: begin xhbg2 := 1; xhg2 := 1 end; 45: xhbg2 := 1; 47: xhbg2 := xhbg2 - 1; 48: xhbg2 := xhbg2 + 1; 49 : xhg2 := xhg2 + 1; 62,71: begin xhg2 := 0; xhbg2 := 0 end; 75: begin xbufLR(xinLR mod s i z e ) := CR; xinLR := xinLR + 1 end; 76: begin xbufLR(xinLR mod s i z e ) :=CC; xinLR := xinLR +-1 end; 77: begin xbufLR(xinLR mod s i z e ) := DT; xinLR := xinLR + 1 end; 78: begin xbufLR(xinLR mod s i z e ) := AK; xinLR := xinLR + 1 end; 79: begin xbufexLR := ED; xinexLR := xinexLR + 1 end; 80: begin xbufexLR := EA; xinexLR := xinexLR + 1 end; 81: begin for i := xoutLR to xinLR - 1 do beg i n 66 d r o p ; xoutLR := xoutLR + 1 end; f o r i := xoutexLR t o x i n e x L R - 1 do b e g i n d r o p ; xoutexLR := xoutexLR + 1 end; x b u f L R ( x i n L R mod s i z e ) := DR; x i n L R := x i n L R + 1 end; 82: b e g i n f o r i := xoutLR t o x i n L R - 1 do b e g i n d r o p ; xoutLR := xoutLR + 1 end; f o r i := xoutexLR t o x i n e x L R - 1 do b e g i n d r o p ; xoutexLR := xoutexLR + 1 end; x b u f L R ( x i n L R mod s i z e ) := DC; x i n L R •:..= x i n L R + 1 end; • - • 83,84,85,86,89,90: xoutLR := xoutLR + -1 ; 87,88: •xoutexLR := xoutexLR + 1; • 91 : b e g i n x b u f R L ( x i n R L mod s i z e ) - : = CR; x i n R L :=• x i n R L + 1 end; 92: b e g i n x b u f R L ( x i n R L mod s i z e ) • : = • CC; x i n R L := x i n R L + 1 end; 93: b e g i n xbu.fRL(xinRL .mod s i z e ) := DT; , , x i n R L := x i n R L + •1 end; 94: b e g i n x b u f R L ( x i n R L mod s i z e ) := AK; x i n R L : = x i n R L + 1 end; 95: b e g i n xbufexRL := ED; x i n e x R L := = x i n e x R L + 1 end; 96: b e g i n xbufexRL := EA; x i n e x R L := = x i n e x R L + 1 end; 97: b e g i n f o r i := xoutRL t o x i n R L - 1 do b e g i n d r o p ; xoutRL := xoutRL + 1 end; f o r i := xoutexRL t o x i n e x R L - 1 do b e g i n d r o p ; xoutexRL := xoutexRL + 1 end; x b u f R L ( x i n R L mod s i z e ) := DR; x i n R L •:= x i n R L + 1 end; 98: b e g i n f o r i := xoutRL t o x i n R L - 1 do b e g i n d r o p ; xoutRL := xoutRL + 1 end; f o r i := xoutexRL t o x i n e x R L - 1 do b e g i n d r o p ; xoutexRL := xoutexRL + 1 end; x b u f R L ( x i n R L mod s i z e ) := DC; x i n R L := x i n R L + 1 end; 99,100,101,102,105,106: xoutRL := xoutRL + 1; 103,104: xoutexRL := xoutexRL + 1; end end; {The p r o c e d u r e check has s e v e r a l t a s k s implemented by i t s l o c a l f u n c t i o n s . F i r s t f u n c t i o n c o v m a r k i n g d e t e r m i n e s , i f a newly a l l o c a t e d node c o n t a i n s a m a r k i n g c o v e r i n g the m a r k i n g of a node g e n e r a t e d • e a r 1 i e r . I f t h i s i s the c a s e , the u n d e r l y i n g P e t r i net i s and the CSP net may be unbounded. A d e s i g n e r r o r i s v e r y p r o b a b l e . F u n c t i o n eqmarking s i m p l y d e t e r m i n e s , i f a newly g e n e r a t e d m a r k i n g has a l r e a d y been e n c o u n t e r e d e a r l i e r d u r i n g the b u i l d i n g of the CSP n e t ' s r e a c h a b i l i t y g r a p h . F u n c t i o n eqvar d e t e r m i n e s , i f a c e r t a i n c o m b i n a t i o n of l o c a l p r o c e s s v a r i a b l e s has been o b s e r v e d i n a node g e n e r a t e d e a r l i e r . The p r o c e d u r e body of check f i r s t c a l l s c o v m a r k i n g and t h e n , i f i t f i n d s the newly g e n e r a t e d s t a t e i n the r e a c h a b i l i t y g r a p h a l r e a d y b u i l t up, s e t s a p o i n t e r ( p f o u n d ) t o i t or c o n t i n u e s s e a r c h i n g t h r o u g h t h e graph.} p r o c e d u r e c h e c k ( n e x t m a r : p l a r r a y ; v a r f o u n d : b o o l e a n ;var p found:maptr; q :maptr); va r i : i n t e g e r ; f u n c t i o n c o v m a r k i n g ( v a r a,b: p l a r r a y ; n p l : i n t e g e r ) : b o o l e a n ; v a r i , j : i n t e g e r ; c : boolean;-b e g i n c := t r u e ; i : = 1 ; j := 0; w h i l e (c and ( i <=npl)) do b e g i n i f a ( . i . ) > b ( . i . ) t h e n j := j + 1; c := c and ( a ( . i . ) >= b ( . i . ) ) ; i := i + 1 68 end; c o v m a r k i n g := c and (j>0) end; f u n c t i o n eqmarking ( v a r a,b: p l a r r a y ; n p l : i n t e g e r ) : b o o l e a n ; v a r i : i n t e g e r ; e : b o o l e a n ; b e g i n e := t r u e ; i := 1_; w h i l e (e and ( i < = n p l ) ) do b e g i n e := e and ( a ( . i . ) = b ( . i . ) ) ; i : = i + 1 ; end; eqmarking := e end; f u n c t i o n e q v a r ( v a r q : maptr) : b o o l e a n ; v a r f : b o o l e a n ; i : i n t e g e r ; b e g i n f := ((xhg 1=q@.hgl)and(xhbgl=q@.hbg 1 ) and(xhg2=q@.hg2)and(xhbg2=q@.hbg2) and ( ( x i n L R - x o u t L R ) = ( q @ . i n L R - q @ . o u t L R ) ) and ((x i n R L - x o u t R L ) = (q@.inRL-q@.outRL)) and ( ( x i n e x L R - x o u t e x L R ) = ( q @ . i n e x L R - q @ . o u t e x L R ) ) and ( ( x i n e x R L - x o u t e x R L ) =(q@.inexRL-q@.outexRL))); i f f t h e n f o r i := xoutLR t o x i n L R - 1 do f := f and x b u f L R ( . i mod s i z e . ) =q@.bufLR(.i mod s i z e . ) ; i f f t h e n f o r i := xoutRL t o x i n R L - 1 do f := f and x b u f R L ( . i mod s i z e . ) =q@.bufRL(.i mod s i z e . ) ; i f f t h e n f o r i := xoutexLR t o x i n e x L R - 1 do f := f and xbufexLR=q@.bufexLR; i f f t h e n f o r i := xoutexRL t o x i n e x R L - 1 do f := f and xbufexRL=q@.bufexRL; eqvar := f end; b e g i n i f c o v m a r k i n g ( n e x t m a r , q @ . m a r k i n g , n p l ) the n bounded := f a l s e ; f o u n d := f a l s e ; checkarray(.q@.numb.) := t r u e ; i f e q m a r k i n g ( n e x t m a r , q @ . m a r k i n g , n p l ) and e q v a r ( q ) then beg in found := true; pfound := q end e l s e begin i := 1 ; while (qd.desc(.i.)<>nil) and found and (i<=q@.ndesc) do begin.. i f che'c kar ray ( ,q@ . desc (. i . ) d.numb.) then check(nextmar,found,pfound,q@.desc(.i.)); i := i+1 end end end; {Procedure nextvar i s used s o l e l y to t r a n s f e r l o c a l v a r i a b l e values to a u x i l i a r y v a r i a b l e s for computations, implementing the f i r i n g of a t r a n s i t i o n . } procedure nextvar; var i : integer; begin xhg1 := cp@.hg1; xhbgl := cpd.hbgl; xhg2 := cp@.hg2; xhbg2 := cp§.hbg2; xioLR := cp@.inLR; xoutLR := cp@.outLR; xinexLR := cp@.inexLR; xoutexLR := cp@.outexLR; xinRL := cpd.inRL; xoutRL := cp@.outRL; xinexRL := cp@.inexRL; xoutexRL := cp@.outexRL; xbufexLR := cp@.bufexLR; xbufexRL := cp(? . buf exRL; for i := xoutLR to xinLR - 1 do xbufLR(.i mod s i z e . ) := cp@.bufLR(.i mod s i z e . ) for i := xoutRL to xinRL - 1 do xbufRL(.i mod s i z e . ) := cp@.bufRL(.i mod s i z e . ) end; {The body of procedure b u i l d l e a v e s s t a r t s here. For a cur r e n t s t a t e embedded in a current node, the enabled sy n c h r o n i z a t i o n s are determined. These are then f i r e d (using s u c p l , predpl, l o c a c t i o n ) and checked (using check) 70 D e p e n d i n g on the outcome of check ( t h e newly g e n e r a t e d node i s f o u n d or not found i n the a l r e a d y b u i l t up graph) e i t h e r a new node i s a l l o c a t e d and r e c u r s i v e l y expanded by b u i l d l e a v e s or s i m p l y a l i n k from the expanded node t o i t s a l r e a d y e x i s t a n t s u c c e s s o r node i s c r e a t e d ( u s i n g the a r r a y s anc and d e s c ) . I f a node c a n n o t be expanded, the f l a g ' b l o c k e d ' i s set.} b e g i n t r a n s i b ( c p @ . m a r k i n g , c p , t s ) ; s y n c s i b ( t s , c s ) ; numleav:= 0; f o r ' i : = 1 t o n p l do n e x t m a r ( . i . ) := c p @ . m a r k i n g ( . i , ) ; n e x t v a r ; f o r i:=1 t o nsync do b e g i n i f c s ( . i . ) t h e n b e g i n numleav := numleav + 1; f o r j:=1 t o n p l do n e x t m a r ( . j . ) := c p @ . m a r k i n g ( . j . ) ; n e x t v a r ; ' f o r j:=1 t o nproc do b e g i n i f sync ( . i , j .) •<> 0 t h e n b e g i n s : = s y n c ( . i , j . ) ; s u c p l ( s , n e x t m a r ) ; p r e d p l ( s , n e x t m a r ) ; l o c a c t i o n ( s ) ; s y n c f i r e d ( . i . ) := t r u e ; w r i t e ( ' s y n c f i r e d : ' , i : 4,' t r f i r e d : ' , sync ( . i , j . ) : 4 , ' ; ' ) end end; w r i t e l n ; v w r i t e ( ' > ' ) ; f o r j:= 1 t o n p l do b e g i n i f n e x t m a r ( . j . ) > 1 t h e n s a f e := f a l s e ; wr i t e ( n e x t m a r ( . j . ) : 2 ) end; w r i t e ( ' vvv ',xhg1:2,xhbg1:2,xhg2:2,xhbg2:2, x i n L R : 2 , x o u t L R : 2 , x i n e x L R : 2 , x o u t e x L R : 2 , x i n R L : 2 , x o u t R L : 2 , x i n e x R L : 2 , x o u t e x R L : 2 ) ; w r i t e l n ; f o r j := xoutexLR t o x i n e x L R - 1 do w r i t e ( x b u f e x L R : 4 ) ; w r i t e ('<-exLR exRL->'); f o r j := xoutexRL t o x i n e x R L - 1 do w r i t e (xbufexRL : 4 ) ; w r i t e (' ; ' ); f o r j := xoutLR t o x i n L R - 1 do . 7 1 w r i t e ( x b u f L R ( . j mod s i z e . ) : 4 ) ; w r i t e ('<-LR RL->'); f o r j := xoutRL t o x i n R L - 1 do w r i t e ( x b u f R L ( . j mod s i z e . ) : 4 ) ; wr i t e l n ; f o r j := 1 t o l a s t m a r do c h e c k a r r a y ( . j . ) := f a l s e ; w r i t e ( ' * * * check begun f o r m a r k i n g a f t e r : ',cp@.numb:5); c h e c k ( n e x t m a r , f o u n d , p f o u n d , m a r k r o o t ) ; w r i t e l n ('*** i t i s an o l d m a r k i n g : ' , found : 6 ) ; cp@.ndesc := cp@.ndesc + .1 ; i f cp@.ndesc > maxdesc then w r i t e l n ( ' N o d e ',cp@.numb:4, ' g e t s too many d e s c e n d a n t s . ' ) ; i f f o und then ' b e g i n l a s t m a r := l a s t m a r + 1; a l l o c ( c p @ . d e s c ( . c p @ . n d e s c . ) , c p , n e x t m a r ) ; w r i t e l n ('new node no',cp@.desc(.cp@.ndesc.) @.numb:8, ', p a r e n t is',cp@.numb); w r i t e l n end e l s e b e g i n c p @ . d e s c ( . c p § . n d e s c . ) := p f o u n d ; pfound@.nanc•:= pfound®.nanc + 1 ; i f p foundd.nanc > maxanc then w r i t e l n ('Node ',pfound@.numb:4, , ' g e t s t o o many a n c e s t o r s . ' ) ; p f o u n d@.anc(.pfoundd.nanc.) := cp; w r i t e l n (cpd.numb,' g e t s o l d d e s c e n d a n t ' , p f o u n d d . n u m b ) ; w r i t e l n end; c p @ . b y f i r e ( . c p @ . n d e s c . ) := i ; i f f o und then b u i l d l e a v e s ( c p @ . d e s c ( . c p @ . n d e s c . ) , l a s t m a r ) end end; i f numleav = 0 t h e n b e g i n cp@.stop := b l o c k ; b l o c k e d := t r u e ; w r i t e l n ('Net becomes b l o c k e d a t m a r k i n g : ', cp@.numb) end end; { P r o c e d u r e e x a m i n e t r e e d e t e r m i n e s p r o p e r n e s s and p o s s i b l y l i v e n e s s of t h e CSP n e t . D e t a i l e d d e s c r i p t i o n a t t h e s t a r t of the p r o c e d u r e body.} 72 p r o c e d u r e e x a m i n e t r e e ( c p : m a p t r ) ; v a r i : i n t e g e r ; p r o p a r r a y : a r r a y (-. 1 . .maxmark. ) of b o o l e a n ; { P r o c e d u r e c y c l i c d e t e r m i n e s , i f t h e CSP net i s p r o p e r by s e a r c h i n g r e c u r s i v e l y backwards t h r o u g h t h e r e a c h a b i l i t y g r aph, s t a r t i n g a t t h e i n i t i a l r o o t node and r e c o r d i n g the e n c o u n t e r e d nodes i n p r o p a r r a y . I f f a l l g e n e r a t e d nodes a r e e n c o u n t e r e d d u r i n g t h i s s e a r c h , the n et i s pr o p e r . } p r o c e d u r e c y c l i c ( c p : maptr; v a r p r o p a r r a y : m a r k a r r a y ) ; v a r i : i n t e g e r ; b : b o o l e a n ; p r o c e d u r e a n c p r o p ( p : m a p t r ; v a r p r o p a r r a y : m a r k a r r a y ) ; v a r i : i n t e g e r ; b e g i n f o r i : = l t o pd.nanc do i f p @ . a n c ( . i . ) d . p r o p then b e g i n p d . a n c ( . i . ) @.prop := t r u e ; • w r i t e l n ( ' m a r k i n g ' , p@ .anc ('. i . ) d.numb : 5, ' i s p r o p e r by a n c p r o p ' ) ; p r o p a r r a y ( . p @ . a n c ( . i . ) d.numb.) := t r u e ; i f p @ . a n c ( . i . ) d.numb <> 1 then a n c p r o p ( p d . a n c ( . i . ) , p r o p a r r a y ) end end; b e g i n w r i t e l n ( ' C y c l i c e n t e r e d f o r m a r k i n g : ', cpd.numb); f o r i := 1 t o c p d . n d e s c do b e g i n i f ( c p d . d e s c ( . i . ) d.numb = 1) then b e g i n cp@.prop := t r u e ; w r i t e l n ( ' m a r k i n g ', cpd.numb : 5, ' i s p r o p e r by c y c l i c ' ) ; p r o p a r r a y ( . c p d . n u m b . ) := t r u e ; i f cpd.nanc > 0 then a n c p r o p ( c p , p r o p a r r a y ) ; end e l s e i f c p d . d e s c ( . i . ) d . propcheck and c p d . d e s c ( . i . ) d.numb > cpd.numb then c y c l i c ( c p d . d e s c ( . i . ) , p r o p a r r a y ) end; c p d . p r o p c h e c k := t r u e ; w r i t e l n ( ' M a r k i n g ', cpd.numb,' has been p r o p c h e c k e d ' ) 73 end; {If a s t a t e c o u l d not be expanded d u r i n g t h e b u i l d i n g of r e a c h a b i l i t y g r a p h , the net has become b l o c k e d and t h i s r e s u l t i s p r i n t e d . O t h e r w i s e the net i s c h e c k e d f o r p r o p e r n e s s ( u s i n g c y c l i c ) and t h e n , i f t h e net i s p r o p e r , p r o c e d u r e e x a m i n e t r e e c h e c k s , i f a l l s y n c h r o n i z a t i o n s have been f i r e d d u r i n g t h e b u i l d i n g of t h e t r e e . In t h i s c a s e the net i s l i v e . } b e g i n i f b l o c k e d then b e g i n wr i t e l n ('The net i s b l o c k e d so n e i t h e r p r o p e r nor l i v e ' ) ; p r o p e r := f a l s e ; l i v e := f a l s e end e l s e b e g i n f o r i := 1 t o maxmark do p r o p a r r a y ( . i . ) := f a l s e ; c y c l i c ( m a r k r o o t , p r o p a r r a y ) ; i • • = 1 • w h i l e p r o p e r and ( i ,<= l'astmar) do b e g i n p r o p e r := p r o p e r and p r o p a r r a y ( . i . ) ; i := i+1 end; .. . w r i t e l n ('The net i s p r o p e r : ', p r o p e r : 5 ) ; f o r i : = 1 t o nsync do l i v e := l i v e and s y n c f i r e d ( . i . ) ; w r i t e l n ( ' a l l s y n c s have been f i r e d : ', l i v e : 5 ) ; end end; {The main program t r i g g e r s " i n i t i a l i z a t i o n of v a r i a b l e s , b u i l d i n g and e x a m i n i n g of t h e r e a c h a b i l i t y g r a p h of the CSP net i n p u t . } b e g i n i n i t ; w r i t e l n ( ' i n i t d o n e , r o o t i s m a r k i n g no', markrootd.numb); b u i l d l e a v e s ( m a r k r o o t , l a s t m a r ) ; w r i t e l n ( ' t r e e b u i I t , ' , l a s t m a r : 5 , ' m a r k i n g s ' ) ; w r i t e l n ( ' s a f e ' , s a f e , ' bounded',bounded,' 2 p r o p e r t i e s ' ) ; e x a m i n e t r e e ( m a r k r o o t ) ; w r i t e l n ( ' t r e e i s e x a m i n e d ' , s a f e , b o u n d e d , p r o p e r , 1 i v e ) , end. \ APPENDIX 2: CSP net s p e c i f i c a t i o n 1 7 1 16 92 1 6 1 3 10 1 1 1 2 1 3 1 4 1 5 1 6 1 7 47 48 49 50 51 52 53 54 3 4 6 0 0 0 0 0 40 41 43 0 0 0 0 0 1 2 0 0 0 0 0 0 38 39 0 0 0 0 0 0 5 7 8 0 0 0 0 0 42 44 45 0 0 0 0 0 9 1 1 5 0 0 0 0 0 0 46 1 1 6 0 0 0 0 0 0 1 9 20 21 22 23 24 25 35 56 57 58 59 60 61 62 72 26 27 28 29 30 31 32 33 63 64 65 66 67 68 69 70 75 76 77 78 79 80 81 82 91 92 93 94 95 96 97 98 1 07 1 08 1 09 1 1 0 1 1 1 1 1 2 1 1 3 1 1 4 5 3 5 7 3 9 3 1 1 1 1 1 1 1 1 1 1 3 1 1 1 1 1 1 1 1 1 1 1 3 1 3 1 3 1 3 1 3 1 3 1 3 3 3 3 6 8 4 1 0 4 2 2 2 2 2 2 2 1 2 1 4 1 2 1 2 1 2 1 2 1 2 1 4 1 4 1 4 1 4 1 4 1 4 1 4 4 4 4 1 5 1 5 1 5 1 5 1 5 1 5 1 5 1 5 1 5 1 5 1 5 1 5 1 6 16 1 6 1 6 1 6 1 6 1 6 1 6 1 6 1 6 1 6 1 6 1 6 1 6 1 7 1 7 1 7 1 7 1 7 1 7 1 3 1 4 1 81 99 2 0 0 3 0 6 76 99 7 99 0 8 78 1 1 1 02 0 1 2 78 0 13 78 1 6 1 04 0 1 7 81, 0 18 105 21 101 0 22 1 02 0 23 1 03 26 99 0 27 1 00 0 28 101 31 1 04 0 32 1 05 0 33 1 06 36 1 06 0 37 82 0 38 83 41 91 0 42 89 0 43 83 46 86 0 47 93 0 48 86 51 95 0 52 87 96 53 88 56 83 0 57 84 0 58 85 61 88 0 62 0 0 63 83 66 86 0 67 87 0 68 88 71 0 0 72 89 0 73 90 84 108 0 85 1 09 0 86 1 1 0 89 1 13 0 90 114 0 99 1 07 1 02 1 10 0 1 03 1 1 1 0 1 04 1 1 2 of t h e I SO t r a n s p o r t p r o t o c o l 18 0 0 0 0 0 0 0 55 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 36 0 0 0 0 0 0 0 73 0 0 0 0 0 0 0 34 37 0 0 0 0 0 0 7 1 74 0 0 0 0 0 0 83 84 85 86 87 88 89 90 99 1 00 101 1 02 1 03 104 1 05 1 06 0 0 0 0 0 0 0 0 1 1 11 11 13 13 4 6 2 2 12 12 14 14 15 15 15 15 16 16 17 17 0 4 75 0 5 1 05 0 1 00 9 1 02 0 1 0 77 0 101 1 4 79 0 1 5 80 1 03 0 1 9 99 0 20 1 00 0 0 24 1 04 0 25 0 0 0 29 1 02 0 30 1 03 0 0 34 0 0 35 1 05 0 97 39 0 0 40 0 0 92 44 83 0 45 84 94 0 49 94 0 50 85 94 0 54 97 0 55 89 0 0 59 86 0 60 87 0 0 64 84 0 65 85 0 0 69 89 0 70 90 0 0 74 98 0 83 1 07 0 0 87 1 1 1 0 88 1 1 2 0 0 100 108 0 101 109 0 0 1 05 1 13 0 1 06 1 1 4 0 75 115 105 0 1 1 6 89 0 0 0 1 The CSP net format f o r i n p u t The f i r s t l i n e (a 1,a2,a3,a4,a5,a6) of 6 i n t e g e r s d e t e r m i n e s the s i z e of t h e i n p u t n e t . I t w i l l c o n t a i n a1 p l a c e s , which can have up t o a4 s u c c e s s o r t r a n s i t i o n s . For i n s t a n c e , p l a c e 3 has t h e s u c c e s s o r t r a n s i t i o n s 3,4 and 6; compare w i t h the CSP net s p e c i f i c a t i o n i n C h a p t e r 4. F u r t h e r m o r e , th e net c o n t a i n s a2 t r a n s i t i o n s w i t h up t o a5 s u c c e s s o r places'. S i n c e t r a n s i t i o n s i n CSP n e t s a r e n o r m a l l y used t o s p e c i f y s t a t e ' t r a n s i t i o n s , a5 has u s u a l l y the v a l u e 1. The net c o n t a i n s a3 s y n c h r o n i z a t i o n s of up t o a6 members. Four b l o c k s o f i n t e g e r s f o l l o w t h e f i r s t l i n e . The f i r s t s p e c i f i e s the s u c c e s s o r t r a n s i t i o n s of t h e CSP net p l a c e s , the s econd the s u c c e s s o r p l a c e s of t h e CSP net t r a n s i t i o n s , the t h i r d the s y n c h r o n i z a t i o n s (maximal s i z e 3) of the CSP net s p e c i f i c a t i o n of t h e ISO t r a n s p o r t p r o t o c o l . F i n a l l y , the i n i t i a l m a r k i n g of the u n d e r l y i n g P e t r i net i s g i v e n . 76 APPENDIX 3: "c s p n e f ' - D o c u m e n t a t i o n " c s p n e t " i s c o m p i l e d u s i n g a P a s c a l - C o m p i l e r on MTS ( * p a s c a l ) . I t t a k e s as o n l y d a t a the d e s c r i p t i o n of a CSP net as o u t l i n e d i n Appendix 2. " c s p n e t " i s used t o examine a CSP net f o r ab s e n c e of d e a d l o c k , and f o r boundedness, s a f e n e s s and p r o p e r n e s s . I f the net i s p r o p e r , i t i s examined f o r l i v e n e s s as w e l l . G e n e r a l o r g a n i z a t i o n and d a t a s t r u c t u r e s : The program t a k e s a CSP net w i t h an i n i t i a l m a r k i n g as i n p u t and c o n s t r u c t s an i n i t i a l r o o t node (of type ma) c o n t a i n i n g the i n i t i a l m a r k i n g and i n i t i a l v a l u e s of a l l l o c a l v a r i a b l e s i n p r o c e d u r e i n i t . The i n i t i a l node i s expanded by r e c u r s i v e l y e x p a n d i n g a l l i t s s u c c e s s o r nodes ( a l l e n a b l e d s y n c h r o n i z a t i o n s a r e f i r e d ) i n the p r o c e d u r e b u i l d l e a v e s i n d e p t h f i r s t f a s h i o n . The e x p a n d i n g p r o c e s s i s s t o p p e d when an a l r e a d y expanded node i s r e a c h e d . U l t i m a t e l y a l l p o s s i b l e s t a t e s of t h e CSP net w i l l be enumerated and a r e a c h a b i l i t y g r a p h of net s t a t e s i s then b u i l t up. W h i l e b u i l d i n g up the g r a p h i t i s easy t o c h e c k , i f t h e net i s bounded and/or s a f e . I f , a t any s t a t e , the net b l o c k s , b e c a u s e no s y n c h r o n i z a t i o n can f i r e , the CSP net s p e c i f i e d p r o c e s s s y s t e m i s not d e a d l o c k f r e e . At l a s t the r e a c h a b i l i t y g r a p h - i s examined i n t h e p r o c e d u r e e x a m i n e t r e e t o d e t e r m i n e , i f the CSP net i s p r o p e r 77 ( t h e r e b y e s t a b l i s h i n g t h a t t h e examined p r o t o c o l s p e c i f i c a t i o n i s c y c l i c ) . I f the net i s p r o p e r and a l l s y n c h r o n i z a t i o n s have been f i r e d d u r i n g the b u i l d i n g of t h e r e a c h a b i l i t y g r a p h , t h e net i s p r o v e d t o be l i v e as w e l l . D e t a i l e d p r o c e d u r e d e s c r i p t i o n s may be f o u n d i n comments i n the program i n Appendix 1. 

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:
http://iiif.library.ubc.ca/presentation/dsp.831.1-0051864/manifest

Comment

Related Items