UBC Theses and Dissertations

UBC Theses Logo

UBC Theses and Dissertations

Protocol specification techniques and specification of the ISO session layer protocol Lee, Roselyn Kam Yiu 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 L43.pdf [ 5.58MB ]
Metadata
JSON: 831-1.0051868.json
JSON-LD: 831-1.0051868-ld.json
RDF/XML (Pretty): 831-1.0051868-rdf.xml
RDF/JSON: 831-1.0051868-rdf.json
Turtle: 831-1.0051868-turtle.txt
N-Triples: 831-1.0051868-rdf-ntriples.txt
Original Record: 831-1.0051868-source.json
Full Text
831-1.0051868-fulltext.txt
Citation
831-1.0051868.ris

Full Text

P R O T O C O L SPECIFICATION TECHNIQUES AND S P E C I F I C A T I O N O F T H E ISO SESSION L A Y E R P R O T O C O L By Roselyn K a m Yiu^Lee B . S c , The University of British C o l u m b i a , 1982  A THESIS S U B M I T T E D IN P A R T I A L F U L F I L L M E N T O F THE REQUIREMENTS F O R THE D E G R E E OF MASTER OF SCIENCE in THE F A C U L T Y OF G R A D U A T E  STUDIES  Department of Computer Science  We accept this thesis as conforming to the required standard  T H E U N I V E R S I T Y O F BRITISH C O L U M B I A May 1984 © R o s e l y n K a m Y i u L e e , 1984  In p r e s e n t i n g  t h i s thesis i n p a r t i a l f u l f i l m e n t o f 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 t h e 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 reference  and study.  I further  agree t h a t p e r m i s s i o n f o r e x t e n s i v e copying o f t h i s t h e s i s f o r s c h o l a r l y purposes may be granted by t h e head o f my department o r by h i s o r her r e p r e s e n t a t i v e s .  It i s  understood t h a t copying o r p u b l i c a t i o n o f t h i s t h e s i s f o r f i n a n c i a l gain  s h a l l n o t be allowed w i t h o u t my w r i t t e n  permission.  Department o f  COMPUTER SCIENCE  The U n i v e r s i t y o f B r i t i s h 1956 Main Mall Vancouver, Canada V6T 1Y3 Date  DE-6  (3/81)  MAY  30, 1984  Columbia  ABSTRACT  C o m m u n i c a t i o n between computers on a network is coordinated by sets of rules known as communication protocols. It is the f o r m a l i z a t i o n of the definitions of such protocols which is the focus of this thesis. Formal  specifications  play  a  key  role  in  the  design,  implementation  and  v e r i f i c a t i o n of protocols. As we shall see, informal descriptions are inadequate due to the  complexity  of  most  protocols.  The  emergence  of  standard  protocols  to  be  implemented by a wide community of users further emphasize the importance of clear and concise s p e c i f i c a t i o n s . There have been extensive research in the area of f o r m a l definition of protocols. The techniques introduced generally f a l l into categories of transition models, program models and hybrid (transition and program combined) models. In this thesis, we review various  methods  alternating  bit  in  these  protocol.  classes To  and  illustrate  demonstrate  the  them  with  applicability  specifications of  these  of  the  specification  techniques, we also specify the ISO session layer protocol using one of the (hybrid) methods described.  ii  TABLE OF  CONTENTS  ABSTRACT TABLE  OF  ii FIGURES  v  ACKNOWLEDGEMENTS  vi  I.  1  II. III.  Introduction Specification of Protocols Transition  3  Models  6  A . F i n i t e State Automaton Models State Transition Diagrams State Decision Tables F o r m a l Grammars Extended State Machine  7 8 9 10 11  B. Petri Net Models Coloured P e t r i Nets Predicate-Transition P e t r i Nets N u m e r i c a l P e t r i Nets Timed P e t r i Net  12 14 14 15 15  1  IV.  Program Models A. B. C. D.  17  Programming Languages Flowcharts Buffer Histories Sequence Expressions  18 20 21 24  V. Hybrid Models A. B. C. D. E.  FAPL Specification Technique F D T and P D I L AFFIRM UNISPEX  26 for Protocols  iii  28 31 34 37 40  T A B L E O F C O N T E N T S (cont.)  VI.  VII.  F o r m a l "Specification of the ISO  Session Protocol  44  A . Overview of the Session Protocol Connection Establishment Phase D a t a Transfer Phase Connection Release Phase P r o t o c o l Subsets  45 45 45 47 47  B. F o r m a l Specification Technique  48  C.  51  Specification of the Session Protocol Conclusions  55  BIBLIOGRAPHY  58  APPENDIX  -  Specification of the ISO  Session Protocol  iv  62  TABLE OF  FIGURES  Figure  1. General View of the Layered P r o t o c o l Structure  3  Figure  2. State Diagram for the A l t e r n a t i n g Bit Protocol  9  Figure  3. State Decision Table for the A B P  10  Figure  4. F o r m a l Grammar for the A B P  11  Figure  5. Pseudo program for the A l t e r n a t i n g Bit P r o t o c o l •  19  Figure  6. Protocol Sequence Graph for the A B P  21  Figure  7. Sequential Processes of the A B P v.- "-  23  Figure  8. Sequence Expressions  .Figure  9. F A P b . FSM's for the Alternating Bit Protocol  30  Figure  10. A B P State Transitions  33  Figure  11. F D T  Figure  12. A F F I R M  Figure  13. Events  for the A B P  -  -  Blumer and Tenney Method  transitions of the A B P  25  36  Axioms of the A B P (from [STEG82])  -  and Topology of the A B P U N I S P E X i f i c a t i o n  v  40 43  ACKNOWLEDGEMENTS  I would like to acknowledge D r . Son Vuong whose strong interest in protocol specification and validation led me to the subject of this work. D r . Vuong provided valuable references and advices throughout the preparation of my thesis.  In  addition,  I  am  grateful  to  Dr.  Sam Chanson  for  his  guidance  and  encouragement.  Furthermore, many thanks are due to M r . Pat Boyle who kept the TI alive during critical  moments,  to M r . Steve  Deering  whose  Virtual  Wire  was (and is) most  definitely an inspiration, and to other graduate students in the department who made graduate studies just a bit more pleasant. Last but not least, I would like to express  my appreciation for the f i n a n c i a l  support of the N a t u r a l Sciences and Engineering Research C o u n c i l of C a n a d a .  vi  Chapter I  Introduction  The fundamental concept of distributed systems is based on means for entities to communicate over a network. A t the logical l e v e l , this "means" is the protocol, i . e . the  procedures  which  communicating  entities  must  follow  in order  to  exchange  i n f o r m a t i o n . Many communication protocols, either in-house or standard, exist to serve various  functions.  attempt  Most  of these  are extremely  to be general purpose or merely  problems  complicated due to either  their inherent c o m p l e x i t y .  their  As a result,  arise in managing a l l aspects of a protocol during the design phase, in  presenting  a  protocol  to  an implementor  unambiguously  and in  verifying  the  correctness of a protocol. The basis for overcoming these d i f f i c u l t i e s is to have a formalism for defining protocols clearly and concisely.  Natural language descriptions  is a popular  are undoubtedly  approach to describing protocols. Although such  useful  for conveying  a general  understanding  of a  protocol, they tend to be not only lengthy but also open to c o n f l i c t i n g interpretations. Furthermore, when one is concerned with v e r i f i c a t i o n or automatic implementation, prose descriptions are certainly unsuitable. Over the past several years, there have been numerous techniques developed to define  protocols.  Many  have  been  borrowed  from  specification  and analysis  of  programming algorithms. The approaches basically f a l l into three categories: transition models, program models and hybrid models combining the first two methodologies. Transition models are based on state transitions of finite machines. They are ideal for  -1-  capturing the control features of protocols. Methods in this category include finite state automata(FSA),  petri nets and grammars. A t the other end of the s p e c t r u m ,  program  able to  models are  depict  the  data flow  and algorithmic nature  of  the  protocols. Flowcharts and high level or pseudo programming languages belong to this class of approach. Specification techniques, however,  do not f a l l s t r i c t l y into these  two classifications. In f a c t , there are a wide range of techniques lying between the two e x t r e m i t i e s . Of these, we can distinguish a group known as event models which are concerned with the sequence of interaction events and could be considered closer to  (or  belonging  sequence  to)  expressions  transition  and  the program and buffer  program  models,  model approach. Examples histories. Due the  most  of event models are  to the inherent  practical  methods  limitations of  the  combine  two  the  philosophies to obtain advantages of both - the hybrid models. O f t e n hybrid models consist  of  a  high  level  programming  functionalities. One such hybrid  language  technique, by  augmented  with  state  transition  Blumer and Tenney, is examined in  detail and applied to the ISO session layer protocol.  In  the following chapter, we discuss what  Chapters  is meant by protocol s p e c i f i c a t i o n .  3, 4 and 5 survey various transition, program (including event) and hybrid  modelling techniques, respectively. Descriptions of the alternating bit protocol [STEG82,Boch78] using these methods are given as examples. Chapter  (ABP)  6 contains a  description of the hybrid s p e c i f i c a t i o n technique by Blumer and Tenney as well as discussions of experiences in applying it to the ISO session layer p r o t o c o l . The actual s p e c i f i c a t i o n is included in the appendix.  -2-  Chapter II  Specification of Protocols  In our discussions, we view hierarchy  of protocol  layers  a communication system as being composed of a  as described  in the ISO Open  System  Architecture  Reference Model [IS082]. A layer N protocol provides a set of services to its (layer N+l) users by making use of services available f r o m the N - 1 lower layers. It is useful for a user to consider a l l layers beneath it c o l l e c t i v e l y as a "black box". Thus at any given layer, one is concerned locally with the interfaces to the layers immediately above  and below  as well as to the system environment, and globally with logical  synchronization with the peer communicating entity, (see Figure 1). LAYER  n+l USERS  <:::::::::::::::::service A  i  I I  nterface:::::::::::::::::> A  I I  V +  I LAYER n I PROTOCOL. I ENTITY  +  V +  I | |<  \  +  +  +  +  > I LAYER n | PROTOCOL I ENTITY  A  A  V  V  I  +  +  I C O M P O S I T E OF L A Y E R S  I I I  I  n - 1 AND BELOW  +  I  Figure 1. General View of the Layered Protocol Structure  The  description of services provided by a layer to its user(s) is termed service  s p e c i f i c a t i o n . It contains abstract descriptions of the allowable sequences of service primitives,  their  effects,  as  well  as  parameters  and  results.  Here  one  is  only  concerned with the behaviour of the protocol as evident from the user's point of view and not with its internal structure. The emphasis is on  what  is available rather than  h o w it is achieved.  The s p e c i f i c a t i o n of the internal mechanisms of the protocol and "how the various protocol entities interact with each other in order to provide the services prescribed in  the  service  specification  of  the  protocol" [Sidh81] is known  as the  (internal)  protocol s p e c i f i c a t i o n . It describes appropriate actions by a protocol in response to all interactions with the user (commands), lower layer entity (incoming messages from the peer entity) and l o c a l system environment  (timeouts).  Although a great  deal more  details must be outlined (than in the service specifications), a high level of abstraction is nevertheless  desirable. Ideally, a s p e c i f i c a t i o n should "define each entity  to the  degree necessary to ensure c o m p a t i b i l i t y with other entities, but no further" ,[BoSu80]. In other words, there should be no ambiguities which may consequently a f f e c t the interaction of communicating entities. Y e t , the amount of details should not r e s t r i c t or bias implementation choices needlessly. It is this description of protocols to which f o r m a l s p e c i f i c a t i o n techniques generally are applied.  There have been discussions in the literature concerning exactly what constitutes a complete protocol (service and internal) s p e c i f i c a t i o n [BoSu80,SiKa82]. G e n e r a l l y , a s p e c i f i c a t i o n is introduced by an overview of the protocol in natural language. This is followed  by  descriptions  of the services  provided by the layer  to the upper  layer  (users), the services expected of the lower layer, and their respective interfaces, The main portion of the s p e c i f i c a t i o n is that of the protocol entity: its overall operation, the types and formats of messages exchanged, and rules governing its actions. Other nonessential requirements  sections and  may  be  included  implementation  to  strategies  • -4-  elaborate or  on  efficiency  execution issues.  environment Obviously,  a  specification  cannot  be  presented  entirely  in english or  entirely  in some f o r m a l  notation but must be a combination of both. Generally, f o r m a l techniques are applied in defining the service interfaces and operation of the protocol entity, although most concentrate on the l a t t e r . It is s u f f i c i e n t for the remainder of the s p e c i f i c a t i o n to be given in prose. [SiKa82] outlines the requirements for the various components of a complete protocol s p e c i f i c a t i o n .  Let us now turn our attention to the various techniques for describing protocols.  -5-  Chapter  III  Transition Models  Protocols are characterized by a large number of events (commands or inputs) requiring usually simple processing reactions (or outputs) which are governed by the sequence  of messages exchanged  thus f a r . State transition  models are natural for  depicting such systems.  There are two main types of state transition s p e c i f i c a t i o n techniques: those based on finite state automata (FSA) and those based on petri nets. F S A have the advantage of being more easily understood but lack the expressibility of petri nets in modelling concurrent general  processes.  properties  of  B o t h , however, protocols  provide  (liveness,  concrete safety,  models on which proofs of etc)  may  be  based.  Proof  methodologies founded on transition models including reachability analysis and analysis by invariants have been successfully automated [ R W Z a 7 8 , A C D i 8 2 ] .  While the control  flow  of a protocol can be clearly displayed using transition  models, its semantic details are not so apparent. Moreover, the readability of F S A state diagrams and petri nets is not always preserved as the more complex protocols have unmanageable numbers of states and transitions. In particular, basic transition models are susceptible to what is known as the state explosion problem when they are used to model protocols employing sequence numbers, message texts and/or timers. Since  at any given state, a l l information pertaining to the current  status of the  protocol machine must be encoded in a single state variable (the state), the state space must be at least as large as the sequence number (and/or message type and/or  -6-  timer  value) space -  possibly i n f i n i t e . Extensions  to the basic F S A and petri net  models for r e c t i f y i n g some of these shortcomings have been proposed. It should be noted that the further a model strays from a pure transition m o d e l , the less applicable are the properties  of a transition model to the augmented model. And hence, the  v e r i f i c a t i o n process becomes more complex. In- this chapter, we discuss the various F S A , petri net and extended models used to define protocols.  A. Finite State Automaton Models  The  basic  transition  modelling technique  is the finite  state  automaton (FSA)  [Dant80,Boch78]. A F S A consists of the 5-tuple, <S, I, O, X,. A> where, S  is a finite set of states  I  is a finite set of inputs  •  is a finite set of outputs  X  is a set of state transition functions (X: IxS r-> S)  A  is a set of action/output functions (A: Sxl -> •)  ,  The i n i t i a l state is usually defined as w e l l . A t a given s t a t e , the next input, applicable state transition and output functions uniquely determine the next state (and output) of the machine. The correspondence of incoming messages (from the user, lower  layer  and system) to input states and outgoing messages and actions to output states make F S A a natural choice of representation for communication protocols. For asymmetric protocols,  separate  F S A may be used  to describe  modules.  -7-  the transmittor  and receiver  F S A have the virtue of being readily represented as state transition diagrams, as decision tables and as f o r m a l grammars. Since these are merely representations of F S A , they inherit the limitations associated w i t h F S A . Thus there is a need to extend the  basic F S A m o d e l . We w i l l look at some such attempts after  we discuss the  representation techniques.  State Transition Diagrams A F S A is most commonly represented graphically by a state transition diagram - a directed graph whose nodes indicate states and whose arcs denote transitions. There are various notations for labelling the arcs in a state diagram. One convention is to associate an arc with either the transmission or reception of a message, e . g . + D A T A denotes reception of a D A T A message, and - A C K denotes the transmission of an A C K message. Another approach is to label each arc with its input and output message (command). Either the input or output may be omitted but not both, e . g . Open  request  CONNECT  denotes  reception  subsequent  of  an o p e n  transmission  of  request  and  a CONNECT m e s s a g e  State transition diagrams are useful for pictorially displaying the control structure and basic  mechanisms  protocols.  However,  transmission  of simple it  protocols  is awkward  or subsets  to include  (or  phases)  features  of messages in the diagrams. Moreover,  other  once  of  more  complex  than reception and  the number  of states  reaches a c e r t a i n threshold, the diagrams become cluttered and d i f f i c u l t to f o l l o w . A t this point the other two representation schemes are more appropriate.  -8-  Sender  Receiver +E,+D1,[T]  +E,+D0,[T] Figure 2. State Diagram for the Alternating Bit Protocol  State Decision Tables A F S A may be represented as a state transition matrix or often referred to as a decision table. States are listed as column headings and the possible events (messages or  commands)  as row headings  (or  vice  versa).  A  cell,  corresponding  to the  intersection of a state and an event, contains the resultant state (and action) f o r the occurrence of the event at the former s t a t e . A n empty c e l l may be used to signify that an event occuring at a certain state is invalid or requires response which is implementation dependent. A large protocol may be described using several tables f o r its  various modules (phases). Decision tables, although infeasible to carry  a large  amount of details, are handy as quick reference guides or summaries. For instance, the document of the ISO session layer protocol definition has decision tables included as annexes [!S083p].  -9-  Sender  EVENTS  sO  |  wO  Recei ver  STATES | si  s e n d |SendDO reques tI I wO  I  ISendDl 1 1 wl  wl  I EVENTS|  rO  STATES I rl  i i i  R e c v D O I c o n s ume 1SendAO 1SendAO 1 rl 1 rl  1 1 1  1SendDl 1 1 wl  RecvDl1SendAl 1 I rO  ISendDO 1 wO  1 1  1 1  RecvERlSendAl I rO  RecvERl  1SendDO 1 wO  1 1  1SendDl 1 wl  T imeou t I  1SendDO 1 wO  !  ISendDl 1 wl  I  + — — — — . _  RecvAO| 1 RecvAl|  si  sO  Timeout  F i g u r e 3. S t a t e D e c i s i o n T a b l e f o r t h e  1SendAl 1 rO  I c o n s ume I SendAl 1 rO —  1SendAO 1 rl 1SendAO 1 rl  ABP  Formal Grammars  There  is a direct  grammar.  translation  Transitions  are  from  mapped  a FSA to  description  production  correspond to nonterminal symbols and input/output  rules  of a protocol of  the  to a f o r m a l  grammar.  States  events to terminal symbols. The  i n i t i a l state, of course, is represented by the starting symbol of the grammar.  The  sentences of the f o r m a l language generated by such a grammar are the possible input and output sequences of the protocol machine. One of the drawbacks of defining a protocol  as a grammar  is that  there  is  no distinction between  symbols (except in the mnemonics assigned to them).  -10-  input  and  output  Sender SO DO WO  Rece i ver RO  = < g e t m e s s a g e ) DO = S e n d D a t a O WO = R e c v A c k O SI I R e c v A c k l DO I R e c v E r r DO j T i m e o u t DO = <get m e s s a g e ) D I = SendDatal Wl = R e c v A c k l SO I RecvAckO DI I R e c v E r r DI I Timeout DI  SI DI Wl  AO  AO  ::= RecvDataO (consume) I RecvDatal Al I RecvErr A l I Timeout A l : : = SendAckO RI  RI  ::=  Al  Al  RecvDatal (consume) I R e c v D a t a O AO I R e c v E r r AO j T i m e o u t AO : : = S e n d A c k l RO  Figure 4. Formal Grammar for the A B P  Extended State Machine A natural extension to the basic F S A model to solve the state explosion problem is to augment it with context variables. Thus each "state variable" is now actually a vector  of variables.. Sunshine in [Suns81] refers  to this extended F S A as being an  abstract machine. Although state transition and output functions are more complex, state diagrams and state tables as well as grammars with appropriate modifications, are adequate in representing the control structure of the protocols. S t r i c t l y speaking, augmenting an F S A with context variables results in a hybrid model.  The extended state machine in [SiKa82] contains several more features to organize the states and "improve a n a l i z a b i l i t y " . States and events are grouped into classes to increase readability and compactness of the descriptions. This c l a s s i f i c a t i o n technique enables more complex protocols to be handled. I n - f a c t , specifications of the A R P A TCP  and IP protocols  have been prepared according to the guidelines described in  [SiKa82]. The "hierarchy overall  state  machine  of state machine" concept is also introduced; that i s , the is  divided  into  logical  submachines  such  as  connection  establishment phase, data transfer phase or connection release phase modules. These  -11-  subordinate machines may be "invoked" from the top l e v e l state machine analogous to the invocation of subroutines in programming environments. Further- extensions to F S A are discussed in the chapter on hybrid models.  B. Petri Net Models  Petri Since  nets were  i n i t i a l l y introduced to model activities of concurrent  communication  protocols  fall  into  this  classification,  various  systems. protocol  specification techniques have been developed based on petri nets and their extensions [Diaz82,Bill82,JuVu84]. A petri net can be described f o r m a l l y by a 4-tuple, <P, T, I, 0 > where, P  is a set of places  T  is a set of transitions  I  is the input or forward incidence function (I: P x T -> N ; where N is the set of integers)  Q  is the output or backward incidence function (O: PxT -> N)  G r a p h i c a l l y , petri nets are represented as directed graphs w i t h arcs interconnecting places (circles) and transitions (bars). A n input arc connects a place to a transition whereas an output arc links a transition to a place. A place may be either an input place (input arc origin) or an output place (output arc incident) or both, relative to some transition(s). A transition may have many input places as well as many output places.  A place may contain zero,  one or more tokens. Tokens  -12-  may be used to  represent incoming/outgoing  messages, commands, conditions or other quantities. An  assignment of tokens to places is known as the marking of a petri net- A marking is analogous  to  incomplete  a FSA without  state.  In  the  specification  f o r m a l sense,  of  its  initial  a definition marking.  of  a petri  Markings  are  net  is  modified  according to the incidence functions. The operation of a protocol machine may be traced by the sequence of markings of its corresponding petri net. A r c s may have weights associated with them (the default weight is 1). (When all weights are 1, the petri net is said to be "safe"). For an input a r c , its weight is the number of tokens its associated place must contain before the a r c is "enabled". When all input arcs to a transition is enabled, the t r a n s i t i o n is said to be enabled. A n enabled transition may " f i r e " . Firing a transition involves removing the appropriate number of tokens from each of its input place and assigning tokens to its output place(s) according to the weights  labelling the corresponding  input  and output  arcs. During  the f i r i n g of a  transition, the number of tokens need not be preserved. New tokens may be created and " o l d " ones destroyed. This f a c i l i t a t e s the modelling of parallel processing such as execution of two child processes spawned f r o m a parent process during a transition. Although petri nets are able to model e x p l i c i t l y the interaction between separate modules  of  a  communication  system,  petri  nets  are  no  more  powerful  than  communicating F S A in specifying semantic details of a protocol. Hence, there have o  been several extensions devised to deal with some of the constrains of the "pure" petri nets: tokens may be uniquely identified - coloured petri nets; relationships may be imposed on tokens - predicate transition nets; predicated actions may label transitions - numerical petri nets; and f i r i n g t i m e intervals may be associated with transitions timed petri  nets. Many  of  these extensions  have  equivalent  counterparts  in  FSA  models. While some of these s i m p l i f y the modelling process, they do not increase the power of the basic petri nets. The numerical petri nets are the exceptions because they are actually hybrid models. The paper by D i a z [Diaz82] contains a comprehensive  -13-  description of petri nets and their variants, which are summarized in the following, as w e l l as a petri net description of the alternating bit protocol.  Coloured Petri Nets In basic petri nets, tokens do not have identities. This is quite adequate for modelling boolean or quantitative entities. When tokens are homogeneous, however, the only way to distinguish between them is to put them in separate places. As a result, even quite t r i v i a l systems can have corresponding large petri nets. The obvious solution is to allow places to have names or colours. More than one token may share the same colour; thus, tokens are not truly named but rather typed or c l a s s i f i e d . The concepts of enabling and f i r i n g have to be extended as w e l l . Arcs are labelled w i t h  "weight  functions" involving the coloured places instead of constants. These functions define "bags". A bag is similar to a set except that there may be more than one instance of an element in a bag. A transition may fire only if the bags on its input arcs are "covered" by the tokens contained in the respective  input places. The bags on the  output arcs of a transition specifies the tokens to be assigned to the output places upon  firing.  The introduction  of coloured  tokens  greatly  simplifies the petri net  representation of systems which contain inherently distinct classes of objects such as message types.  Predicate-Transition Petri Nets In even more complex systems, merely classifying the tokens is not s u f f i c i e n t ; one needs to be able to define relationships on the tokens to f a c i l i t a t e modelling of such systems.  In predicate-transition  expressions transition  nets, the tokens  of the input  places must  satisfy  specified in corresponding input arcs to a transition, in order for that to f i r e .  Predicates  tokens added to the output  on the output  relationships  between  places. P r e d i c a t e - t r a n s i t i o n nets are no more  powerful  -14-  arcs  determine  than coloured nets although predicate-transition nets enable more compact models to be defined.  Numerical Petri Nets A numerical petri net consists of a (possibly predicate-transition) petri net augmented with program variables and "predicate;action" constructs. A transition may  fire when  it is enabled and its associated predicate holds. Upon firing of a transition, its labelled action is executed and tokens reassigned accordingly. Since numerical petri nets model not only the control but also data aspects of a system, it is actually a hybrid model. The increased power and expressibility facilitate the specification of more complex communication  protocols. Control and  data  flow  aspects of the  models defined,  however, must be verified separately: the former using reachability analysis and the latter using program verification techniques. In [BU182], the CCITT transport service is specified using numerical petri nets.  Timed Petri  Net  In basic petri nets and its above mentioned extensions, events are modelled without time considerations. For communication protocols, however, the concept of time is fundamental. One may  needs to be able to specify, for instance, systems in which messages  get lost - recoverable systems. Petri nets augmented with time constrains are  known as timed petri nets. Each transition of such a net has associated with it an interval of time (tMIN, tMAX) in which it must fire. An enabled transition must wait tMIN amount of time before firing but cannot wait longer than tMAX. For a transition to fire during the specified interval, it must remain enabled. An enabled transition must fire at tMAX if it has not done so during that interval. (The basic petri net  may  be viewed as a special case of timed petri nets with tMIN equal to 0 and tMAX equal to  infinity).  This timing extension is ideal for capturing timeout  -15-  features in a  communication protocol.  Chapter IV Program Models  Another view of communication protocols is as sets of procedures. As such, it seems  appropriate  programming including  to specify  algorithms.  conventional  protocols  There  are  a  using the same techniques used to variety  of  program  approaches such as flowcharts  languages, and event-based schemes which concentrate  description  and high level  define  techniques  programming  on the sequence history  of  operations of interacting entities. The l a t t e r include sequence expressions and buffer histories.  With program models, the state explosion problem is no longer a threat. A l l the features of a protocol, no matter how complex, may be expressed concisely. However, it  is  often  supposed  to  difficult do  from  to  "separate the  the  particular  essential features way  chosen  to  of  what  the  accomplish those  program  is  functions"  [Suns79]. Not only are implementation decisions biased but the s p e c i f i c a t i o n may be cluttered up with unnecessary details. A higher level of abstraction is often sought. Furthermore,  a program description often hides the control flow structure  of  the  protocol making it very cumbersome to follow the logic of the protocol. It becomes d i f f i c u l t to analyze the protocols as well as verify or validate t h e m . Assertion and other methods used in verifying correctness of programs can be generalized to apply to protocols. Hbwever, program v e r i f i c a t i o n is itself a nontrivial task, and so, the situation is worst for protocol v e r i f i c a t i o n .  -17-  A. Programming Languages  The most straightforward of the program model approaches is to specify protocols using high level programming languages such as C , Pascal or A D A , or using pseudo code.  This  is the same concept  languages. One simply recognizes  as describing  programs  or algorithms  using such  the f a c t that a protocol is just another type of  algorithm.. Complex protocols can be handled relatively easily since variables can be used to store as much status information as required. The s p e c i f i c a t i o n also serves as a natural implementation model (depending s p e c i f i c a t i o n languages  are, of course).  on what the target implementation and  As mentioned, however,  a higher l e v e l of  abstraction is often preferred.  One way of achieving a higher level of abstraction is to specify as l i t t l e of the protocol specify  as possible using programming the "legal protocol  operation"  languages. and English  In [Wats82],  Pascal is used to  for "environment  details" of a  transport protocol. The approach, given the name "abstract behavioural s p e c i f i c a t i o n " , is  aimed  at  expressing  operations  on objects  in a nonprocedural  manner.  User  interfaces, operating environment, addressing, flow c o n t r o l , buffer management, e t c . , are described in English (about half of the entire description) while details pertaining to correct protocol operation, such as transmission/reception of data and timer events, are  written  in P a s c a l .  Although  there  is a higher  level of abstraction  gained in  specifying some aspects of the protocol in natural language, the authors admit that there is s t i l l an undesirable amount of restriction imposed on implementation choices.  -18-  procedure Sender i := 0; repeat getdata( D(i) ); repeat send( D(i) ); starttimer( X ) ; wait( event ); if( event=Receive( A(j) ) and i=j ) then break;  }  i := i +.1;  procedure  Receiver  { j := 0;  repeat starttimerC T ); wait( event );  if( event=Receive( D(i) ) and i=j )  then  {  consumedata( D(j) );  j  j *•= j + ! ;  send( A(j) );  Figure 5 . Pseudo program for the Alternating Bit Protocol  -19-  B. Flowcharts  Just as flowcharts are used to pictorially represent algorithms, they are used to model protocols as w e l l . Conventional flowcharting methods (including block diagrams) are  feasible.  However,  certain  aspects  of  a  protocol  not  common  to  other  programming algorithms may be more appropriately modelled using special symbols.  Gouda in [GoMa78] devised a scheme to describe protocols (or rather machines)  using  flowcharts._ Such  describes the actions of one  a flowchart,  called a protocol sequence  protocol graph,  communicating e n t i t y ; that is, it gives a l o c a l rather  than a global s p e c i f i c a t i o n . There are four types of nodes used corresponding to the write,  read,  assignment  and  conditional  statements  in  high  level  languages,  respectively: send  node - denotes transmission of a specified message to a designated destination. It is represented by a square with one output arc (or edge).  receive node - denotes reception of a message f r o m a set of expected messages f r o m a designated source. It is represented by a c i r c l e with as many output arcs as expected messages plus a " t i m e o u t " a r c . The timeout arc is taken if none of the expected messages arrive by a specified period of time. assignment node - denotes specified operations and assignments performed. It is represented by a bar with one output a r c .  to  be  decision node - denotes transfer of control based on values of certain variables. It is represented by a triangle with two or more output edges. In [GoMa78], the IBM B i n a r y Synchronous C o m m u n i c a t i o n (BiSync) Protocol is defined using protocol sequence graphs. , Since techniques  each  flowchart  has  a  have the same power  corresponding  equivalent  program,  flowcharting  as the programming language methods discussed  above.  -20-  Sender  Rece iver  V  i  I NV  +  I  m E  <-  j  0  <-  0  V \JS +  I  +  +  I D(i)  I  [T]  D(i)  E  I  J-<-  A(j)  +  i  <-  j+-l  +  A(j )  i+1  F i g u r e 6. P r o t o c o l S e q u e n c e G r a p h f o r t h e A B P  C. B u f f e r Histories  Buffer histories refer to records of messages sent and received between processes communicating via message passing. States are not modelled e x p l i c i t l y but may be embedded in data structures.  The  focus, rather, is on the input/output  behaviour  (relations between items in the buffers) of the processes. A major drawback of buffer  -21-  histories stems from the division of a system's interaction history into separate buffer histories. One cannot easily relate orders of items in different buffers. Timestamps on items have been proposed as a possible remedy.  The integrated specification/programming language, Gypsy, is based on concurrent processes  and  buffer histories. Gypsy  communication  protocols but  for  was  not  concurrent  designed systems  specifically in  for defining  general. However, its  concurrency capabilities make it suitable for protocols. Many features of this language was  adopted from Pascal and Concurrent Pascal. In addition, constructs are available  to specify relations between data items in buffers and other data objects referenced by  the processes. (One  verification  of the  goals of the language is to facilitate  of properties of the systems  defined). References  automatic  [Good77, GoCo78]  contain more details on the Gypsy language. A method for formal specification (and verification) of protocols based on Gypsy is presented by DiVito in [Divi82]. Modules of a protocol are represented as sequential (simple) processes  and  further  grouped  into  concurrent  (coorperating) processes.  Processes communicate via message buffers. Each sequential process is described by a state vector and events list. The state vector is actually just a list of the process' local variables. The events list consists of guarded statements; that is, a statement is not executed until its guard (or precondition) is true. Events which occur while the guard is false are queued at the appropriate statement. Event handlers ("routines" for processing events) are specified "non-procedurally" using decision tables which detail transitions and actions to be performed. when  an  event  occurs, reflecting  a  A process' (local) state vector is updated modification of  the  internal  environment.  Communication with the external environment (other processes) is via input and output buffers. Assertions on the items in these buffers constitute the service specification of  the protocol. Service specifications are stated as external invariants or, more  precisely, "a conjunction of relations  between -22-  histories  or  expressions  involving  histories".  This  technique  is  geared  towards  mechanical  verifications  of  system  operations. It is, however, quite l i m i t e d in modelling the control aspects of a protocol due to separate  histories  being kept for incoming and outgoing data. In f a c t , the  authors point out that with the existing s p e c i f i c a t i o n technique, it is not possible to describe the connecting phase of a protocol. The following is a process description of the A B P ; it does not include the decision table definitions of the event handlers.  process A B P (input source: message; output sink: message) = begin buffers( sndr_pkt, r c v r _ p k t : packet; sndr_ack, r c v r _ a c k : n a t u r a l ; cobegin sender( source, sndr_ack, sndr_pkt ); receiver( r c v r _ p k t , sink, rcvr_ack ); medium( sndr_pkt, rcvr_pkt ); medium( r c v r _ a c k , sndr_ack ); end end; process m e d i u m (input in_buf: T; output out_buf: T) = pending; process s e n d e r (inputs source: message; a c k _ i n : natural; output pkt_out: packet) = begin state vector( seq: n a t u r a l ; in_transit: boolean; t o _ t i m e : natural); initiallyC 0, false, 0 ); events true => on receipt of ack from ack_in handle by ack_hdlr; in_transit => after t o _ t i m e handle by stimeout_hdlr; not in_transit => on receipt of mess f r o m source handle by source_hdlr; end end; process r e c e i v e r (input p k t _ i n : packet; outputs sink: message; ack_out: natural) = begin state vector( next: natural; in_transit: boolean; t o _ t i m e : natural ); initially( 0, false, 0 ); events true => on receipt of pkt from pkt_in handle by pkt_hdlr; in_transit => after t o _ t i m e handle by rtimeout_hdlr; end end;  F i g u r e 7. S e g u e n t i a l P r o c e s s e s of t h e  -23-  ABP  D. Sequence Expressions  Sequence  expressions  operation of the protocol  is  an "algebraic"  approach  to  specifying  protocols.  The  is defined by a sequence of regular expressions. In the  f o r m a l sense, sequence regular expressions are neither true program nor transition models. Expressions correspond to F S A and (type 3) f o r m a l grammars; however, they contain  neither  explicit  states  nor  implicit  distinction between  input  and  output  symbols. As in program models, status of a protocol machine is given by its current location while symbol names may imply their input/output natures.  Basic regular expressions are constructed using the following operators: *  arbitrary repetition (Kleene closure),  ->  followed by, and  spaces-within-brackets alternatives. Schindler [Schi80] has suggested additional features sequence  expressions  more  suitable  for  expression may be labelled with "rejection current  modelling  to the basic scheme to protocols.. Terms  make  within  an  predicates" composed of parameters of  and previous operations and of the number of operations of a certain type  previously becomes  executed. An operation which contains a term whose predicate is false invalid.  An  expression  may  be  divided  into  "blocks",  each  of  which  corresponds to a nonterminal symbol in f o r m a l grammars or, f r o m another point of view, to a program procedure or f u n c t i o n . Blocks may have multiple exit blocks in order  for  exceptions  to  be easily handled. The  paper by_ Schindler contains  details on s p e c i f i c a t i o n of protocols using sequence expressions.  -24-  more  S E N D E R := { D A T A O -> D A T A 1 }* ; D A T AO := J s.DO -> R E C V O } ; R E C V O := { (r.AO -> D A T A 1 ) ( r . A l -> DATAO) }, X I := D A T A O ; D A T A 1 := { s . D l -> R E C V 1 } ; R E C V 1 := { ( r . A l -> D A T A O ) (r.AO -> D A T A 1 ) }, X I := D A T A 1 ; R E C E I V E R := { DATO -> D A T 1 }* ; DATO := { (r.DO -> XI SENDO := { s.AO -> D A T 1 := { ( r . D l -> XI SEND1 := { s . A l ->  SENDO) ( r . D l . -> SEND1) }, := S E N D 1 ; D A T 1 }; SEND1) (r.DO -> SENDO) }, := SENDO; DATO };  (Note: r . X X and s . X X denotes reception and transmission of messages of type X X , respectively) Figure 8. Sequence Expressions for the A B P  -25-  Chapter V Hybrid Models  As we have seen, transition techniques are suited to displaying the control flow of protocols  whereas  program  models  are ideal for handling  their  semantic  details  (variables and parameters). Methods in either category a r e , however, quite l i m i t e d by themselves  when  "real"  protocols  are to be defined. Many  approaches,  therefore,  sought to reap the advantages of both by combining the two philosophies. Such efforts form the class of hybrid models. A hybrid model consists of a simple state model augmented with context variables and routines to operate on t h e m . The "state portion" summarizes the overall control structure state  of a p r o t o c o l . The "program portion" specifies the actions, accompanying  changes,  according  to  values  of the context  variables  and input  message  parameters (eg. sequence numbers). A t y p i c a l hybrid technique employs a high level programming  language  "spiced-up"  with  special  constructs  for  realizing  state  transitions. Many hybrid models have been developed. Of these, there are two main schools of thought: one aimed at automatic implementation [ B l T e 8 2 , S R W G 8 0 , A C N R 8 3 , I S O 8 1 ] ; the other  at  verification  and  validation  [STEG82,DaBr78,Sehw81, JuVu84].  A  unified  implementation and v e r i f i c a t i o n oriented model has also been proposed, [VuCo82]. Implementing a complex communication protocol is a nontrivial and tedious task, to say to least. If we have a w e l l - d e f i n e d language for specifying protocols, we must also have a "syntax-checker"  available to verify that protocols are specified in the -26-  correct syntax. take this one  The  basic idea behind automatic implementation of protocols is to  step further: provide a compiler which not only checks the syntax  specifications but also translates them  into  of  some high level programming language. Of  course, only code for the implementation independent portions may be automatically generated.  Hence,  we  actually  have  only s e m i - a u t o m a t i c implementation schemes.  . Specification languages in this category include F A P L , the ."Specification Technique for  Protocols",  F D T and. P D I L .  If constructs are available, in a s p e c i f i c a t i o n language, for stating invariants about various aspects of a protocol, one could conceivably verify properties of the specified protocol based on the actions and transitions defined. Systems have been developed to automate v e r i f i c a t i o n of protocols described using hybrid techniques. V e r i f i c a t i o n of hybrid models is considerably less complex than that of pure program models since the "transition portions" of the models may be used in the proofs.  An example of a  specification language concerned with v e r i f i c a t i o n is A F F I R M . Most of the (semi) automatic implementation oriented s p e c i f i c a t i o n techniques are general enough that some features  for  definition  design,  scheme  verification  which,  capabilities  is  at  its  UNISPEX,  verification  a  may be included as w e l l . One  incorporates "unified  both  approach  implementation to  specification  and and  verification".  In this chapter, we discuss the various hybrid model s p e c i f i c a t i o n languages named above.  The  focus  is on  the general approach taken by each rather  details. Where appropriate, the methods are compared.  -27-  than s p e c i f i c  A. F A P L  The Format and Protocol Language ( F A ^ L ) evolved f r o m an e f f o r t to define IBM's Systems  Network  capabilities statements:  for  Architecture  (SNA)  representing state  ASSIGN,  CALL,  I F - T H E N - E L S E , and S E L E C T  formally  models. The  DECLARE,  DO,  [SRWG80], subset END,  of  It  augments  P L / 1 with  P L / 1 used includes PROCEDURE,  the  RETURN,.  groups. In addition to the standard P L / 1 data types, the  basic data-element construct in F A P L is the "entity". Entities (and their data fields) are defined using E N T I T Y statements. Subsequently, entities may be C R E A T E d  and  D I S C A R D e d dynamically. T y p i c a l use of an entity is to represent message units in a protocol. Lists of entities are manipulated using special F A P L list handling constructs such as N E W L I S T , D E S T R O Y ,  I N S E R T and R E M O V E . A particular type of l i s t , a data  queue, may contain only one entity type. I N S E R T i n g ( R E M O V E i n g ) an entity to (from) a data queue corresponds to queuing (dequeuing) an item with a specified priority.  The  overall  protocol (SNA)  state automata (referred  structure  to in F A P L  is successively refined into "basic" finite  as FSMs). A n F S M is defined using a state  transition m a t r i x . Each state name has a corresponding state number. Columns of the matrix are identified by state name and number pairs. Input conditions  (abbreviated)  are contained in the row headings. Input (and output) codes referenced within the matrix are defined outside the m a t r i x . . A c e l l in the m a t r i x contains a "next-state indicator" and possibly an output code. The next-state indicator may be one of: n  the number of the next state same state (no state change)  >  error condition (violation of protocol rules)  /  error condition (design error)  The output code (if any) denotes an output function to be executed.  A n F S M described using such a matrix may be referenced by -28-  C A L L FSM_fsmhame[(fsm_input)]; or  IF S E N D _ O R _ R E C E I V E _ C H E C K ( THEN...  FSM_fsmname[(fsm_input)] )  The latter " c h e c k i n g " F S M reference does not cause a state transition or output action to be executed except when the selected next state indicator is ">"- It is used f o r screening  out error  conditions  before  c o m m i t t i n g to a state  change.  Typically,  checking references of " a l l applicable" FSM's always precede " n o r m a l " type references. FSM's may also be referred to by generic names.  F A P L specifications are translated by a preprocessor into P L / 1 programs. Each F S M matrix becomes a . P L / 1 procedure. A l s o , there is a validation system developed which is applied to the data flow control layer of S N A defined i n F A P L . F SM_ I N P U T D E F I N I T I O N : /* s y m b o l s u s e d i n t h e " i n p u t s " t r a n s i t i o n m a t r i x */  column of  the state  MESS FSMINPUT='USER SEND'; ACK = 0 ; AO Al ACK = 1 ; SEQO SEQ = 0 ; SEQ1 . SEQ = 1 ; ERR BAD P A C K E T ; TIMEOUT' FSMINPUT='TIMEOUT' ; END F S M _ I N P U T _ D E F I N I T I O N ; 1  F SM_ S ENDER: F S M D E F I N I T I O N CONTEXT (ABP) ;  INPUTS  S T A T E N A M E S - - - > | S E N D O I WAITO | SEND1I W A I T l S T A T E NUMBERS ->1 0 1 1 02 | 0 3 I 0 4  MESS  12(SO ) 1  -  |4(S1) 1  AO  1  -  1  3  I -  Al  1  -  1  ERR  1  -  1 -(SO)|  -  l-(Sl)  'TIMEOUT'  1  -  1 -(SO) |  -  l-(Sl)  -29-  -Cso) | -  -  l-(Sl) 1  1  OUTPUT CODE\  FUNCTION  SO  I CALL  S E N 3 _ D A T A ( 0 ) ; / *s e nd d a t a O * /  . SI  CALL  SEND_DATA(1);/*s end d a t a l * /  END F S M _ S E N D E R ; FSM_RECEIVER:  F S M - D E F I N I T I O N CONTEXT(ABP) ; STATE NAMES--->IDATAOIDATA1 STATE NUMBERS->| 0 1 | 02  INPUTS SEQO  |2(C0)|-(R0)  SEQ1  l-(Rl)IKCl)  ERR  |-(R1)|-(R0)  'TIMEOUT'  |-(R1)|-(R0)  OUTPUT  CODE  FUNCTION  RO  1 CALL SEND_ACK(0);/*retransmit  ackO*/  RI  I  ackl*/  CO  1 C A L L CONSLME_DATA;  CALL  SEND_ACK(0);  CI  1 C A L L CONSUME_DATA;  CALL  SEND_ACK(1);  CALL SEND_ACK(1);/*retransmit  END F S M _ R E C E I V E R ; F i g u r e 9. F A P L FSM's f o r the A l t e r n a t i n g B i t P r o t o c o l  -30-  B. S p e c i f i c a t i o n T e c h n i q u e f o r P r o t o c o l s  The "specification technique for protocols" is a f o r m a l i s m introduced by Blumer and Tenney [BlBu82,BlTe82,TeB181]., The s p e c i f i c a t i o n technique is a transition model augmented  with . P a s c a l .  Pascal  CONST  addition, (user, lower  layer  declaration  Implementation  section.  and T Y P E  declarations  and system) interface events dependent  functions  are  available.  In  are included in the data may  be  declared  as  "primitive"s to denote that they w i l l only be described functionally and not defined e x p l i c i t l y within the s p e c i f i c a t i o n .  The bulk of the s p e c i f i c a t i o n is the state transitions. Each transition is modelled e x p l i c i t l y and independently (of other transitions). A state transition is characterized by  a current  state,  a resultant  s t a t e , an enabling condition  (event  and  possibly  predicates), program segment and transition priority: < dest > <-(p) < origin > [ begin trans i t i on_act i on_rout i ne; end; As  evident  here,  a  transition  production rule. Interpretation  from  statement  I:EVENT.type  resembles  ]  a regular  (  (type  of such a rule is straightforward:  pred  3)  )  grammar  the F S M at state  <origin> (either a single state or a state abbreviation), upon occurrence of an event at interface  I,  if  the  enabling  predicate  (pred)  holds,  will  execute  the  transition_action_routine and proceed to the state <dest> (either a single state or the pseudo state "same_state"). The priority p denotes the order which applicable rules are to be used. A rule without  a priority  has the lowest p r i o r i t y .  Note that enabling  predicates are not to have side effects on the machine variables for obvious reasons. Throughout the s p e c i f i c a t i o n , square brackets ([]) enclose interactions with the various i n t e r f a c e s . Each interface is identified by a single c a p i t a l l e t t e r (eg. U for User, S for System  and T  for  Transport  service). E V E N T  denotes  a service  primitve such as  T _ C O N N E C T and T _ D A T A . 'The type of an event may be one of request, i n d i c a t i o n , -31-  response or c o n f i r m . Thus, [to  I : E V E N T . t ype(  argl  :=  vail,  arg2  :=  val2  )]  i n i t i a t e s an event of the specified type at the interface I; while [from I:EVENT.type] signals  the  occurrence  of  an  event  of  the  specified  type  at  the  interface  I.  Arguments passed by the i n i t i a t o r may be accessed by the acceptor. eg.  ca 11ed_address  P r o g r a m segments  :=  may contain any  pascal assignments, repetition  [ f r o m U:  Ca11ed_address];  of the " b r a c k e f e d constructs intermixed  statements, conditionals and procedure  and  with  function  calls.  Since the transitions are defined separately, the s p e c i f i c a t i o n serves as a useful document for quick look-ups s i m i l a r to state decision tables. Blumer and Tenney have developed a compiler which takes the above language as input and generates C code. The ISO  (Class  2 and 4), as w e l l as the N B S (basic and extended)  transport  layer  protocols have been specified using this scheme [NBS83a,NBS83b,NBS81a,NBS81b]. (The authors c l a i m that approximately automatically produced.)  40 percent of the entire implementation may be  This s p e c i f i c a t i o n technique and its application to a session  protocol is discussed further in the following chapter.  {Transitions - module acts as both sender and receiver} <ACK_WAIT> <-- <ESTAB> [from U:SEND.request] begin p.msgdata : - [from U : U D a t a ] ; p.msgseq := send_seq; store(send_buffer,p); [to N : D A T A . r e q u e s t ( N D a t a : = n e t _ d a t a ( D A T A , p.msgseq, p.msgdata)]; [to S:TIMER.request(Name := retran_data, - T i m e := retran_time)]; end; <same_state>'<~  <ACK_WAIT> [from SrTIMER.indication] ([from S:Name] = retran_data)  begin p := retrieve(send_buffer); [to N:DATA.request(NData^ := n e t _ d a t a ( D A T A , p.msgseq, p.msgdata)]; [to S:TIMER.request(Name := retran_data, -32-  Time := retran_time)]; end; <ESTAB> <-- <ACK_WAIT> [from N : D A T A . i n d i c a t i o n ] ([from N : N D a t a . i d ] = A C K and [from N : N D a t a . s e q = send_seq ) begin [to S:TIMER.cancel(Name := retran_data)]; remove(send_buffer, [from N:NData.seq]); incr_send_seq; end; <same_state> <— <either> [from N r D A T A . i n d i c a t i o n ] ([from N : N D a t a . i d ] = D A T A ) begin {always A C K data; store if expected sequence number} q.msgdata := [from N : N D a t a . d a t a ] ; q.msgseq := [from N:NData.seq]; [to N : D A T A . r e q u e s t ( N D a t a := n e t _ d a t a ( A C K , q.msgseq, null)]; [to S:TIMER.request(Name : = retran_ack, Time := retran_time)]; if [from N:NData.seq] = recv_seq then begin store(re.cv_buff er,q); incr_recv_seq; end; end; <same state> <— (either> [from SrTIMER.indication] ([from SrName] = retran_ack) begin q := retrieve(recv_buffer); [to N : D A T A . r e q u e s t ( N D a t a := net_data(AC.K> q.msgseq, null)]; [to S:TIMER.request(Name := retran_ack, _ T i m e := retran_time)]; end; <same_state> <— <either> [from U : R E C E I V E . r e q u e s t ] (not buffer_empty(recv_buffer)) begin q := retrieve(recv_buffer); [to U : R E C E I V E . i n d i c a t i o n ( U D a t a := q.msgdata)]; remove(rec.v_buffer, q.msgseq); end;  Figure 10. ABP State Transitions - Blumer and Tenney Method  -33-  C. F D T and PDIL  The F o r m a l Description Technique  (FDT)  is an extended state transition model  first suggested by Bochnfann and later adopted by subgroup B of the ISO ad hoc group on formal description techniques. It is a combination of F S A and P a s c a l , in some aspects s i m i l a r to the method proposed by Blumer and Tenney. However, F D T appears to produce a more integrated program-like s p e c i f i c a t i o n .  In F D T , there is a concept of "channels" signifying interactions between modules within an environment.  A s p e c i f i c a t i o n of a module's channel lists all the feasible  interaction primitives which may occur over the channel. P r i m i t i v e s are classified according to their initiator(s).  For example, a channel between a service  providing  module and its users, referred to as a service access point in ISO terminology, may be defined by enumerating the primitives a user may issue followed by possible primitives initiated  by  "interface"  the  provider.  declarations  specifications  in  FDT  The  in are  the  channel  definitions  method  defined  using  by  Blumer  these  in  FDT and  channel  or  is  analogous  Tenney access  above. point  to  the  Service primitive  enumerations. The (internal) protocol s p e c i f i c a t i o n contains further channel definitions for interactions with the lower layer as well as with the system environment. The  actions  taken by an entity  module is according to transitions of an F S A .  Transitions are specified by transition types which have the following f o r m : FROM < o r i g i n > WHEN < e v e n t > PROVIDED < p r e c o n d TO < d e s t > BEGIN  >  « •*  END; The F R O M (present state), W H E N (input) and P R O V I D E D  (enabling predicate) clauses  make up the enabling condition portion of a transition type. The TO (destination state) clause  and  BEGIN...END  (action)  program -34-  segment  define  the  operation  of  the  t r a n s i t i o n — E a c h F R O M clause may have more than one W H E N , . P R O V I D E D , TO and B E G I N . . . E N D clauses associated with it„ For example, one may have the following hypothetical transition type definition: FROM s t a t e O WHEN e v e n t l WHEN e v e n t 2 PROVIDED p r e d 2 WHEN e v e n t 3 BEGIN a c t i on 3 ; END; WHEN e v e n t 4 PROVIDED p r e d 4 BEGIN ac t i o n 4 ; END;  TO TO TO  TO  s tat e l ; state2; state3  state4  One advantage of this particular syntax is that " r e l a t e d " transitions may be grouped together. This allows specifications to be condensed and organized modularly. The  ISO  subgroup  has  prepared  an example description  of  the  ISO  transport  protocol using F D T [BoRa82]. Another s p e c i f i c a t i o n technique based on (and very similar to) F D T is the P r o t o c o l Description and Implementation Language (PDIL) f r o m the R H I N project in F r a n c e . It has  provisions  simulation.  A  for  protocol  subset  of  the  descriptions, service ISO  descriptions,  session protocol  has  been  implementation and defined using  PDIL.  [ A C N R 8 3 , A R C h 8 2 ] contains a more detailed discussion of the various elements of PDIL.  (* Transitions - module acts as both sender and receiver *) from ESTAB when P A R . S E N D _ r e q u e s t ( U D a t a ) to A C K _ W A I T . begin send_msg.data:=UData; send_msg.seq:=send seq; S A P . B U F F E R _ s t o r e r s e n d _ b u f , send_msg); N A P . D A T A _ r e q u e s t ( n e t _ d a t a ( D A T . A , s e n d j n s g . s e q , send_msg.data)); SAP.TIMER_request(retran_data, retran_time); end;  -35-  from A C K _ W A I T when SAP.T-IMER_indication(Name) provided Name=fetran_data to same begin send_msg:=SAP.BUFFER_retrieve(send_buf); N A P . D A T A _ r e q u e s t ( n e t _ d a t a ( D A T A , send_msg.seq, send_msg.data)); SAP.TIMER_request(retran_data, retran_time); end; when N A P . D A T A _ i n d i c a t i o n ( N D a t a ) provided N D a t a . i d = A C K and NData.seq=send_seq to E S T A B begin . SAP.BUFFER_remove(send_buf, NData.seq); incr_send_seq; SAP.TIMER_cancel(retran_data); end; from E S T A B , A C K _ W A I T when N A P . D A T A _ i n d i c a t i o n ( N D a t a ) provided N D a t a . i d = D A T A to same begin recv_msg.data:=NData.data; recv_msg.seq:=NData.seq; N A P . D A T A _ r e q u e s t ( n e t _ d a t a ( A C K , r e c v j n s g . s e q , null)); SAP.TIMER_request(retran_ack, retran_time); if NData.seq=recv_seq then begin S A P . B U F F E R _ s t o r e ( r e c v _ b u f , rec.v_msg); incr_recv_seq; end end; when. S A P . T I M E R _ i n d i c a t i o n ( N a m e ) provided Name=retran_ack to same begin recv_msg:=SAP.BUFFER^retrieve(recv_buf); - N A P . D A T A _ r e q u e s t ( n e t _ d a t a ( A C K , recv_msg.seq, null)); SAP.TIMER_request(retran_ack, retran__time); end; when P A P . R E C V _ r e q u e s t ( ) provided not S A P . B U F F E R _ e m p t y ( r e c v _ b u f ) to same begin recv_msg:=SAP.BUFFER_retrieve(recv_buf); PAP.RECV_ihdication(recv_msg.data); S A P . B U F F E R _ r e m o v e ( r e e v _ b u f , recv_msg.seq); end; F i g u r e 11. F D T  transitions of the A B P  -36-  D. A F F I R M  A F F I R M is a system developed at U S C - I S I for the s p e c i f i c a t i o n of abstract data types  and v e r i f i c a t i o n of their  properties [STEG82].  Since the system is based on  transitions of abstract machines, it is suitable for defining communication protocols as well.  Abstract data types and programs in A F F I R M are w r i t t e n in an extended variant of P a s c a l . A data type is specified by a set of "constructors" which create the objects of the type, "extenders" (or "modifiers") which are used to manipulate the objects and "selectors" (or "predicates") which yield values concerning the objects. For example, a stack  may  have  constructors  NEWSTACK  and P U S H , extender  P O P and selector  T O P O F S T A C K . The values (semantic meanings) of data objects are given in terms of their constructors selectors  are  which are " p r i m i t i v e , unspecified" operations. The extenders  defined  axiomatically  with  equations  involving  constructors.  and  These  equations are l e f t - t o - r i g h t rewrite rules which specify the e f f e c t of each function on each of the constructors.  Service and protocol descriptions may be specified f o r m a l l y in terms of abstract data types of A F F I R M . Constructors may be used to represent events and selectors the state variables in a protocol machine. D e f i n i t i o n of the selectors then describe effects of events on the protocol machine.' Selector definitions are grouped by the constructor on which they operate into "axioms". A (abstract data) type in A F F I R M is composed  of  specification  some  declarations  generally  consists  followed of  several  by  axioms  "type"  descriptions.  definitions.  For  A  protocol  example,  the  A F F I R M A l t e r n a t i n g B i t P r o t o c o l representation consists of the type A B P r o t o c o l plus auxiliary types Message, P a c k e t , M e d i u m , Bit and Q u e u e o f P a c k e t s . Only the axioms of the A B P r o t o c o l type is given in the following figure. The complete representation is given in [STEG821  -37-  Once a protocol has been s p e c i f i e d , the next step is to verify c e r t a i n properties which it possesses. One a i m is to show that the protocol s p e c i f i c a t i o n implements the services required (semantic properties). Correspondence between the two specifications may be made by mapping the constructors  and selectors of one onto the other. A  protocol s p e c i f i c a t i o n is " a c c u r a t e " if the axioms of the service s p e c i f i c a t i o n are "theorems" provable  f r o m axioms of the protocol s p e c i f i c a t i o n . Properties  (either  semantic or syntactic) to be shown are specified as theorems i n A F F I R M and are proved  by induction based on the constructors  - structural induction. A " s c h e m a "  outlining the appropriate induction approach accompanies each data type s p e c i f i c a t i o n . AFFIRM facilities  does  not search  are available  f o r or generate  to a i d users  proofs  of theorems  in developing  proofs  by i t s e l f .  Instead,  interactively:  employ  induction, split into subgoals, substitute equalities, and apply l e m m a s . Users  direct  their own proof strategies with A F F I R M carrying out the mechanics of the proofs.  A favourable aspect of A F F I R M ' s abstract data type s p e c i f i c a t i o n is its high l e v e l of abstraction. For instance, actual implementation and size limitations of queues and stacks are of no concern. A l s o , the rewriting rule representation of axioms allow specifications  to be "walked  through"  to determine  their  accuracies.  The main  drawback with A F F I R M is that i t is d i f f i c u l t to model exception handling features due to the strong typing of the operations. Work on this area is s t i l l in progress.  type ABProtocol; needs types Message, P a c k e t , QueueOfMessage, Q u e u e O f P a c k e t , M e d i u m , B i t ; •  axioms Sent(ProtocolSend(p,m)) == if Pending(p) = NewQueueOfPacket then Sent(p). Add m else Sent(p), Sent(lnitializeProtocol). == NewQueueOfMessage; axioms Received(Deliver(p)) == if ReceiverBuffer(p) = NewQueueOfPacket -38-  then Received(p) else Received(p) Add Text(Frqnt(ReceiverBuffer(p))), Received(InitializeProtocol) == NewQueueOfMessage; axioms SenderToReceiver(ProtocolSend(p,m)) == if Pending(p) = N e w Q u e u e O f P a c k e t then Transmit(SenderToReceiver(p), MakePacket(m,SSN(p))) else SenderToReceiver(p), SenderToReceiver(ReceivePacket(p))' == Receive(SenderToReceiver(0)), SenderToReceiver(Retransmit(p)) == if Pending(p) = NewQueueOfPacket then SenderToReceiver(p) else Transmit(SenderToReceiver(p), Front(Pending(p))), SenderToReceiver(l_osePacket(p)) == Receive(SenderToReceiver(p)), SenderToReceiver(InitializeProtocol) == I n i t i a l i z e M e d i u m ; axioms SSN(ReceiveAck(p)) == if Seq(Front(ReceiverToSender(p))) = SSN(p) and ReceiverToSender(p) ~= I n i t i a l i z e M e d i u m then ~SSN(p) else SSN(p), SSN(InitializeProtocol) == InitialSequenceNumber; axioms ReceiverToSender(ReceivePacket(p)) == if SenderToReceiver(p) ~= I n i t i a l i z e M e d i u m and ReceiverBuffer(p) = NewQueueOfPacket and RSN(p) ~= Seq(Front(SenderToReceiver(p))) then Transmit(ReceiverToSenderCp), Front(SenderToReceiver(p))) else ReceiverToSender(p), Receiver ToSender(ReceiverAck(p)) == Receive(ReceiverToSender(p)), ReceiverToSender(Deliver(p)) == if ReceiverBuffer(p) = NewQueueOfPacket then ReceiverToSender(p) else Transmit(ReceiverToSender(p), Front(ReceiveBuffer(p))), ReceiverToSender(LoseAck(p)) == Receive(ReceiverToSenderCp)), ReceiverToSender(InitializeProtocol) == I n i t i a l i z e M e d i u m ; axioms RSN(ReceivePacket(p)) == if Seq(Front(SenderToReceiver(p))) = RSN(p) and SenderToReceiver(p) ~= I n i t i a l i z e M e d i u m then ~RSN(p) else RSN(p), RSN(InitializeProtocol) == InitializeSequenceNumber; axioms Receive Buff er(ReceivePacket(p)) == if Seq(Front(SenderToReceiver(p))) = RSN(p) and SenderToReceiver(p) ~= InitializeMedium then N e w Q u e u e O f P a c k e t A d d Front(SenderToReceiver(p)) else ReceiverBuffer(p), ReceiveBuffer(Deliver(p)) == N e w Q u e u e O f P a c k e t , R e c e i v e B u f f e r ( I n i t i a l i z e P r o t o c o l ) == N e w Q u e u e O f P a c k e t ;  -39-  axioms Pending(ProtocolSend(p,m)) == if Pending(p) = N e w Q u e u e O f P a c k e t then NewQueueOfPacket Add M a k e P a c k e t ( m , SSN(p)) else Pending(p), Pending(ReceiveAck(p)) == if Seq(Front(RecieverToSender(p))) = SSN(p) and ReceiverToSender(p) ~= InitializeMedium then NewQueueOfPacket else Pending(p), Pending(InitializeProtocol) == N e w Q u e u e O f P a c k e t ;  end {ABProtocol};  Figure 12. A F F I R M Axioms of the A B P (from [STEG82])  E. U N I S P E X  As  we  have  seen,  hybrid  models  are  either  directed  towards  automatic  implementation or v e r i f i c a t i o n . It is desirable, however, to have an integrated system suitable for achieving both goals. One such system is U N I S P E X proposed by Vuong and Cowan. [VuCo82]. U N I S P E X is an extended F S A model combining features of F D T (described earlier) and  SPEX,  a  protocol  s p e c i f i c a t i o n language  [Schw81]. P r o t o c o l s p e c i f i c a t i o n in U N I S P E X  aimed at  f a c i l i t a t i n g verifications  consists of three sections: the protocol  machine part, the topology part and the properties part describing the behaviour of each protocol machine, instances of protocol machines and the manner in which they are interconnected, and properties of their interactions, respectively. The protocol machine part of the s p e c i f i c a t i o n include declarations and definitions -40-  of interfaces and events. In addition to state (internal) variables, one may define interface  and channel (external) variables. Interface  variables are shared  between  modules residing on different layers of a protocol machine. Channel variables are used to synchronize interactions with the peer entity layer module. It is v i a these external variables that the protocol machines exchange data and coordinate their activities (see below). (State  variables carry only l o c a l information). Interfaces  to the upper and  lower layers are defined by service primitives and mapping events (plus primitives), respectively. U s e r service requests (network interactions) cause changes in interface (channel)  variables  and  at  the  same t i m e  triggers  occurrences  of  events.  Event  definitions capture the behaviour of the protocol machine in response to interaction with other layers and the system environment. Each event has an assocaited state transition and program segment. Events are assumed to be atomic and has the f o r m : <name> / < c o d e > when ( <pred> [ effect ]  / <origin> )  ->  <dest>:  When an event, either message transmission/reception or t i m e o u t , denoted by <code>  c occurs, and the precondition <pred> holds, a state transition f r o m <origin> to <dest> takes place. In addition, the program segment [ e f f e c t ] is executed. The  topology  part  defines  instances  of  protocol  machine  type(s)  previously  declared in the protocol machine part. These definitions are analogous to declaration of  variables  analogous  to  using Pascal  the  VAR  TYPE  construct  in  Pascal.  (The  definitions). Interconnection  protocol  machine  of instances, either  part  is  across  layer or protocol machine boundaries, are specified using relations involving external variables.  The  properties  part  allows  properties  concerning  the  instances  of  protocol  machines to be described. Both l o c a l (concerning a single protocol machine) and global (concerning the entire layer) invariants may be asserted.  -41-  Validation  of  the  syntactic  properties  of  a protocol  defined  in U N I S P E X  is  achieved via reachability analysis and decomposition of its underlying F S A . This is., achieved by, f i r s t , translating a U N I S P E X  s p e c i f i c a t i o n into FSA's and subsequently  applying existing F S A analysis techniques. Proof of correctness of a protocol's design is by induction on the sequence of events of the global system (using a top down approach). The s p e c i f i c a t i o n is transformed into an "algebraic" data type s p e c i f i c a t i o n which  can then  be fed to  a v e r i f i c a t i o n system such as A F F I R M . The  carrying out such a transformation is yet to be defined.  Events [ SendData / - D A T A / E S T A B — > A C K _ W A I T when (Cmd=send and OutReq=null) [ Sent:=Add(Sent, MsgToSend); OutChannel:=Add(OutChannel, MsgToSend); Pending:=true; SS:=VS; OutReq:=DATA; Cmd:=null; ] R e c e i v e D a t a /+DATA/ E S T A B — > E S T A B 1 or ACK_WAIT — > ACK_WAIT1 when (InReq=DATA and SR=VR) [ Received:=Add(Received, MsgReceived); InChannel:=Remove(InChannel); RecvBuf:=Add(RecvBuf, MsgReceived); VR:=Increment(VR);  ] R e c e i v e D u p l i c a t e /+DATA/ E S T A B — > E S T A B 1 or ACK_WAIT — > ACK_WAIT1 When (InReq=DATA and SR !=VR) [ InChannel:=Remove(InChannel); ] Timeout / timeout / A C K _ W A I T — > A C K _ W A I T When (Timer=timeout and Pending=true and OutReq=null) [ MsgToSend:=Retrieve(SendBuf); SS:=VS; OutChannel:=Add(OutChannel, MsgToSend); OutReq:=DATA; ] -"S  SendAck / - A C K / E S T A B 1 — > E S T A B or A C K W A I T ! — > A C K WAIT -42-  rules  for  When (OutReq=null and InReq=DATA) [ SS:=SR; MsgToSend:=empty; OutReq:=ACK; InReq:=null;  ] R e c e i v e A c k /+ACK/ A C K _ W A I T — > When (InReq=ACK and SR=VS) [ VS:=Increment(VS); Pending :=false; SendBuf:=Remove(SendBuf); InReq:=null;  ESTAB  ] D e l i v e r D a t a /null/ A N Y — > S A M E When (Cmd=receive and RecvBuf!=empty) [ MsgToDeliver:=Remove(RecvBuf); Cmd:=null; ] ] TOPOLOGY [ Instances Station : Array(Side) of A B S t a t i o n Connections Station(i).OutReq <—> Station(OppSideG)). InReq Station(i).OutChannel <—>Station(Oppside(i)),InChannel; ] F i g u r e 13. E v e n t s and T o p o l o g y o f t h e A B P  -43-  UNISPEXification  C h a p t e r VI  F o r m a l S p e c i f i c a t i o n o f t h e ISO S e s s i o n  Protocol  This chapter reports on a f o r m a l s p e c i f i c a t i o n of the ISO session l e v e l p r o t o c o l . The session protocol standard is a set of procedures designed to f a c i l i t a t e dialogue management, document transfer and data flow synchronization and resynchronization between user entities [IS083s]. In the context of the ISO R e f e r e n c e Model [IS082], the session layer provides these services to presentation layer entities by interacting w i t h transport layer entities. There are three subsets of the protocol defined within the ISO standard. In this report we deal with the Basic Combined Subset (BCS) and Basic A c t i v i t y . Subset (BAS) which are the subsets responsible for minimal session service and reliable bulk data transfer s e r v i c e , respectively.  • The s p e c i f i c a t i o n technique employed to define the ISO session protocol f o r m a l l y is  a hybrid state  transition  and programming language  methodology  designed  and  developed by Tenney, et a l . [TeB181] (briefly described in section B of Chapter 5). We first give an overview of the services provided by the session protocol. N e x t , we describe the f o r m a l i s m to be used to define i t . Finally,-.we discuss experiences with s p e c i f i c a t i o n of the session protocol. We present the f o r m a l s p e c i f i c a t i o n of the session protocol using the technique described as the appendix to this thesis.  -44-  A. Overview of the Session Protocol  "The session service provides the means for organized and synchronized exchange of data between cooperating session users" [lS083s]. The service offered is connection based and maybe divided into connection establishment, data transfer and connection release phases. There are three subsets defined within the standard. These w i l l be described after we discuss the connection phases.  Connection Establishment Phase During the connection establishment phase, a session connection is established between users which provides the required quality of transport service as well as negotiated session parameters session  and f u n c t i o n a l i t i e s . Transport  addresses are obtained f r o m the  addresses supplied by the users. Cooperating  users  may identify  "logical"  session connections which may span one or more "physical" session connections. Users may also exchange a l i m i t e d amount of transparent data during this phase.  Data Transfer Phase Exchange of data between session users is coordinated by functions negotiated during the connection establishment phase. These include f a i r l y straightforward concepts such as segmentation and reassembly of user data units, concatenation of c e r t a i n protocol data  units  and expedited  data transfer  f o r conveying  "out of band" data.  Other  concepts require more detailed explanations. Tokens are a means of controlling rights of the users to invoke c e r t a i n services. There are several tokens available depending on the subset of the protocol in use (and user preference) for negotiated release (release token), data exchange (data token), minor synchronization  (minor synchronization  -45-  token) and major synchronization and  activity  management (major synchronization/activity  token), (see below) Except for  the data token, presence of a token implies a v a i l a b i l i t y of the associated s e r v i c e . The data token is required for simplex and half-duplex connections. Only the owner of the data token may send data; however,  transmission of a l i m i t e d amount of data is  possible without the data token via the " t y p e d - d a t a " p r i m i t i v e . For duplex connections, either  side  may  transmit  data  at  any  time.  During  a session, a token may  be  dynamically reassigned to either users (at the discretion of the owner of the token). However, a v a i l a b i l i t y of a token is s t a t i c (determined at session connection time).  Communication between session users may be synchronized by e x p l i c i t definition of synchronization points. Each synchronization point is identified by an automatically incremented synchronization s e r i a l number. There are major and minor synchronization points neither of which carry inherent meaning to the entity providing the session service (service provider). Major and minor synchronization establishment is governed by the major synchronization/activity and minor synchronization tokens, respectively. Major synchronization points are used to structure the data stream into a series of "dialogue units" - - " a l l communication within it is guaranteed to be isolated f r o m a l l communication before and after i t " — whereas minor synchronization points are used to mark the data s t r e a m . Major synchronzatiion points must be acknowledged before further exchange of data is permitted (confirmed service). Acknowledgement of minor synchronization points is optional and entirely up to the user entities. P r i m i t i v e s are also available for users to resynchronize to a (previous) synchronization point (tokens may be reassigned as well).  The  session service  also  provides  primitives  for  management of  activities  —  " l o g i c a l " units of work which may span one or more session connections. There may only be one current a c t i v i t y on a session connection. A v a i l a b i l i t y (and use) of a c t i v i t y management  is  determined  by  the  major  synchronize/activity  token.  If  activity  management is available, normal data must be exchanged within an a c t i v i t y . A l i m i t e d  -46-  amount of data may be passed outside an a c t i v i t y using the capability data feature. There are mechanisms for s t a r t i n g , ending, interrupting, resuming and cancelling an a c t i v i t y . The synchronization serial number is reset to 1 at the start of an a c t i v i t y and  is  automatically  synchronization  incremented  at  the  end  of  the  an  activity.  Other  major  points may be established between the start and end of an a c t i v i t y .  The serial number is set to the user supplied value at resumption of an a c t i v i t y . As mentioned above, the service provider does not associate any semantics with the s e r i a l numbers.  Connection Release Phase If the release token is available, its owner has the authority to initiate a release of the session connection and the acceptor of such a request has the option of rejecting it (negotiated release option). Otherwise, either side may issue a disconnect request the receipient of which must comply. Either users may, irrespective of the placement of the release and data tokens, destructively terminate a session connection by means of the abort  p r i m i t i v e . The connection may also be aborted by the provider  upon  encountering irrecoverable protocol errors or loss of the transport connection.  Protocol Subsets The definition of different subsets within the protocol standard is designed to "achieve simplification, [IS083s].  There  yet are  to provide thre  a variety  service  of capabilities, for  subsets  different  applications"  in the session standard: Basic  Combined  ...Subset (BCS), B a s i c - S y n c h r o n i z e d , Subset (BS) and Basic A c t i v i t y . Subset (BAS). Within each subset, there  are  mandatory  and optional functional units. The functions  for  connection establishment, normal data transfer, release of connection and abort are common to all subsets. A l l subsets expect reliable transport service from the lower layer. -47-  The duplex  B C S provides the minimal session services. Connections may be either half or  (full) duplex.  Other options which implementations may support  include  expedited data transfer (only if expedited transport service is available), typed data, exceptions, token management and negotiated release. The data token (release token) is available if the half duplex (negotiated release) option is enabled. The  BS provides  conversational  oriented  services.  There  are  mechanisms  structuring and resynchronizing the data s t r e a m . Half duplex and optionally connections are supported. Mandatory functionalities include typed data,  for  duplex  negotiated  release, minor and major synchronization, resynchronization and token management. The synchronize  minor, synchronize major/activity, release and possibly data tokens  are available. The underlying transport service must support expedited data transfer which the session provider  uses to achieve reliable resynchronization with the peer  session machine.  The B A S provides a reliable bulk data transfer s e r v i c e . As for BS, half duplex and optionally  duplex  connections  are supported. A c t i v i t y  management, capability  data  exchange, major and minor synchronization, token management and exception reports are mandatory functionalities of this subset. Optional features include typed transfer  and resynchronization.  The  underlying transport  data  expedited service (even if  available) is not used by the session machine.  B. Formal Specification Technique  The basic approach here is to model a protocol using a finite state machine (FSM) augmented  with  program  segments.  An  FSM  . -48-  is  assumed to  have  three  passive  interfaces: the upper layer (users), lower layer and l o c a l system environment. These interfaces are passive in the sense that the means of associating i n i t i a t i o n of an event with its reception  by another entity  as well as the delay between the instance a  protocol entity initiates an event and when it is noticed are unspecified. There is a set  of  well  defined  events  at  each interface  corresponding  to  service  primitives  provided at the i n t e r f a c e . Output parameter(s) specified by the i n i t i a t o r of an event become the input parameter(s) available to the receipient. It is this abstract model of a protocol machine on which the s p e c i f i c a t i o n language is based.  A f o r m a l s p e c i f i c a t i o n consists of several parts: data declaration, state definition, declaration  of  procedures  procedures,  description  and p r i m i t i v e s ,  of  i n i t i a l i z a t i o n of  p r i m i t i v e s , state  transitions  and  variables, definition description  of  of  header  f o r m a t s . Except for descriptions of the p r i m i t i v e operations and header formats which are expressed in natural language, the other sections of the definition are formulated using an extended s p e c i f i c a t i o n language based on P a s c a l . D a t a declarations include definition (using Pascal constructs) of constants, types, structure  of data objects, and declaration of variables. Each s p e c i f i c a t i o n contains  definition of a record type whose fields are the " l o c a l variables" of the F S M and declaration of a variable to be of this type (eg. c a l l this variable Ecs). Statements in the program segments have i m p l i c i t "with Ecs do" prepended to t h e m . A l s o , as part of the data declarations, there are e x p l i c i t definitions of the interface events. Each such event is described by the name of its associated service p r i m i t i v e , parameter(s) and default  value(s) (if  any) for  the parameter(s). (Parameters with default values  are  optional parameters). eg.  interface  [to T:T_DISOONNECT.indication( Reason : reason^type; User data : data type d e f a u l t  NULL  State abbreviations are similar to declaration of sets or constants. They merely  -49-  provide pseudonyms for groups of states. There must be declarations of initial and final states. A n F S M starts off at the i n i t i a l state and ceases to exist when i t reaches the final s t a t e . Any intermediate feasible state must appear in one or more abbreviations. The special abbreviation "same_state" need not be declared and may be used i n state transitions to indicate that the F S M remains in the same s t a t e . A l l procedures  (and functions) appearing in the s p e c i f i c a t i o n must be declared.  These are normal Pascal procedure and function declarations except that in addition to " f o r w a r d " , they may be designated " p r i m i t i v e " to denote that they w i l l only be described functionally and not defined e x p l i c i t l y within the s p e c i f i c a t i o n . It should be noted  here  that  the data  and procedure  declarations  serve  only  to  make the  specification c o m p l e t e . They are not essential for the general understanding of the protocol. However, they are valuable for automated implementation and validation processes.  One of the procedures supplied must be that which initializes the variables of a new F S M . Other procedures (and functions) defined are those which do not introduce implementation dependencies or restrictions. Procedures not satisfying this  criterion  are termed " p r i m i t i v e s " and are defined descriptively to preserve the abstract nature of the s p e c i f i c a t i o n approach. The  bulk of the s p e c i f i c a t i o n is the state transitions. Each state transition is  characterized by a current s t a t e , a resultant s t a t e , an enabling condition (event and possibly predicates), program segment and transition priority: < dest > <-- (p) < origin > [ begin trans i t i on_action_routi ne; end; As  evident  here,  a transition  production rule. Interpretation  from  statement  I:EVENT.type  resembles  a regular  of such a rule is straightforward:  ]  (  (type  pred  )  3) grammar  the F S M at state  origin (either a single state or a state abbreviation), upon occurrence of an event at -50-  interface  I,  if  the  transition_action_routine  enabling  predicate  pred  holds,  will  and proceed to the state dest (either  execute  the  a single state or the  pseudo state "same_state"). The priority p denotes the order which applicable rules are to be used. A rule  without  a priority  has the lowest priority.  Note that enabling  predicates are not to have side effects on the machine variables for obvious reasons. Throughout the s p e c i f i c a t i o n , square brackets ([]) enclose interactions (not necessarily events) with the i n t e r f a c e s . Each interface is identified by a single c a p i t a l l e t t e r (eg. U  for User,  S for_ System and T for Transport  service).  primitve such as T _ C O N N E C T and T _ D A T A . The  E V E N T denotes a service  type of an event may be one of  request, i n d i c a t i o n , response or c o n f i r m . Thus, [to  I:EVENT.type(  argl  :=  vail,  arg2  :=  val2  )]  i n i t i a t e s an event of the specified type at the i n t e r f a c e I; while [from I:EVENT.type] signals  the  occurrence  of  an  event  of  the  specified  type  at  the  interface  I.  Arguments passed by the i n i t i a t o r may be accessed by the acceptor. eg.  ca11ed_address  :=  [ f r o m U:  Ca11ed_address];  Program segments may contain any of the " b r a c k e f e d constructs intermixed pascal assignments, repetition statements, conditionals and procedure  and  with  function  calls.  . C. Specification of the Session Protocol  The accompanying s p e c i f i c a t i o n is that of the B C S and B A S subsets. A l l definition sections mentioned above except for description of header formats (see [IS083p] for details) are included. In a general sense, the s p e c i f i c a t i o n is a translation of the state tables provided in the annex of [IS083p] enhanced with details e x t r a c t e d f r o m the -51-  language descriptions in both [ISQ83s].and [IS083p]. However, perhaps because the ISO document is an early draft proposal of the protocol, the state tables are not complete and some state  transitions  are  derived  directly  from  the  descriptions  (eg.  those  concerning interrupting or discarding a c t i v i t i e s ) . In  addition  to  the  " k e r n e l " functions  (connection  establishment,  normal  data  transfer, connection release, and abort) the following function groups are supported: negotiated release (for BCS), major and minor synchronization, typed data, capability data, exception report, omitted  are  activity  resynchronization  management and token management. The and  expedited  data transfer.  In  addition,  functions transport  connections are torn down, when associated session connections are released, and not reused. Concatenation of SPDU's and fragmentation and reassembly of SSDU's are not considered in the s p e c i f i c a t i o n . Moreover, "category activity, "category  capability  data and typed  1" commands; that  2" commands  (synchronization,  data commands) are depicted as if  is, an  identified by the imbedded category  SPDU  containing  a category  they  were  2 command is  2 command; that is, the category  1 command  which precedes it in the S P D U is ignored. The routines handling the reception and transmission of SPDU's are assumed to hide the distinction from the s p e c i f i c a t i o n .  Most of the above omitted functions could have been included and assumptions deemed unnecessary; however the s p e c i f i c a t i o n stands as it is due to a number of factors.  The  decision to  make all commands appear  homogeneous  (and leave  the  details to actual implementations) is motivated by the belief that emphasis should be placed on conveying a clear representation of the operation of the protocol instead of the actual structure  of SPDU's. This stress on the conceptual understanding of the  protocol also apply to the other s p e c i f i c a t i o n choices.  Concatenation Including  provisions  and for  fragmentation  are  really  local  implementation  these would complicate the reception  -52-  decisions.  and transmission of  SPDU's. Furthermore, the routines associated with handling these options would have been specified as primitives  only  since representation  of  data (buffers) is  highly  implementation dependent.  The reuse of a transport connection is also a provider option. However, the ISO protocol definition clearly (and abstractly) specifies how reuse of a connection is to be achieved. The  reason that reuse of a transport  connection is not included in our  s p e c i f i c a t i o n is the " i n e f f i c i e n t " manner which the s p e c i f i c a t i o n technique allows it to be defined. Reuse of transport connection applies to not only abort but also normal release as w e l l as refusal of a session connection. For each transition going to an unconnected  session  state,  there  would  have  to  be  three  state  transitions  (to  tc_unconnected, tc_reuse_initiator or tc_reuse_acceptor states), each differing only in the  resultant  state  and some details such as issuing disconnect  requests  to  the  transport server or starting timers, e t c . This is a consequence of the r e s t r i c t i o n on the resultant state being a constant. If the resultant state may be a variable, then each transition to an unconnected session state can be represented by a single state transition whose program segment invokes a function to determine the resultant s t a t e . This scheme preserves  the  conciseness of  the  original (without the reuse  option)  protocol.  The expedited data transfer option is omitted because it is not part of the B A S . This appears contradictory with respect to the a c t i v i t y management description. In the ISO  document, arrival  of  expedited  data is queued when  there  is  no a c t i v i t y  in  progress and dequeued once an a c t i v i t y is started (or resumed). It is not clear why this detail is included when one cannot even use the expedited data option with B A S and no  other  subset  has  activity  management  c a p a b i l i t i e s . Other  contradictions  and  ambiguities exist between the verbal descriptions and state table definitions in the document (especially pertaining to the availability of minor synchronization and data tokens and status of an a c t i v i t y ) . The reason for these inconsistencies, as mentioned, -53-  could be due to the f a c t that the document is only an early draft proposal.  -54-  Chapter  VII  Conclusions  As we have seen, many diversed techniques communication  protocols.  The  technique  chosen  are available for formally defining to  specify  a particular  protocol  depends on the complexity of the protocol and the intended use(s) of the s p e c i f i c a t i o n (whether for implementation or v e r i f i c a t i o n purposes). FSA  and  representations Automated  petri  nets  are  easily  analysis  are  useful  understood  techniques  based  for  representing  and on  facilitate transition  simple  analysis models  of  have  protocols.  Such  the  protocols.  been  developed  [ A C D i 8 2 ] , These models, however, are quite l i m i t e d in their ability to handle more complex  protocols.  The  number  of  states  (or  places)  and  transitions  become  unmanageably large very quickly. High level programming languages and f l o w c h a r t s , on the other hand, are quite adequate in fully capturing the details of complex protocols. F u r t h e r m o r e , depending on the target implementation language, such a s p e c i f i c a t i o n may also serve as a natural implementation model. The major drawbacks of these techniques are the lack of abstraction and d i f f i c u l t y in v e r i f i c a t i o n . The buffer history approach attempt to ease the l a t t e r by allowing invariants to be stated on the input/output behaviour  of  communicating processes. However, the only v e r i f i c a t i o n methods available for other program  models are assertion and temporal logic techniques developed for  proving  correctness of programs.  . Extensions  to transition  and program definition techniques -55-  attempt to increase  their applicability of " r e a l " protocols. Usually these extensions result in hybrid models which have means to express both the control and data flow aspects of protocols. Several specification languages based on the hybrid approach have emerged. Some are oriented towards automatic implementation ( F D T , P D I L , F A P L ) while others are aimed at mechanical v e r i f i c a t i o n ( A F F I R M ) and s t i l l others sought  to provide  integrated  implementation and v e r i f i c a t i o n f a c i l i t i e s for protocols ( U N I S P E X ) . Although analysing hybrid  models is not as straightforward  as analysing transition models (due to the  additional program elements), the e x p l i c i t states in both allow one to follow the logic of a protocol's control structure quite easily. This is an advantage over pure program models. Of  course the program elements of hybrid  models provide  the  expressive  power lacking in basic transition techniques. Due to the complexity of most protocols, it appears that hybrid approaches are the most suitable (of the three) in f o r m a l l y specifying communication protocols. The hybrid s p e c i f i c a t i o n technique by Blumer and Tenney offers a straightforward method  of  representing  the  actions and transitions  of  high level  protocols.  Both  control and data flow aspects are captured. Its major advantages over state transition diagrams  and  tables  are  its  expressibility  and  clarity.  Although  the  other  two  approaches offer " g r a p h i c a l " representation, they become cluttered and d i f f i c u l t to follow  when  modelled  protocols  entirely.  of  the  Designers  complexity would  of  no doubt  most high level protocols be able to  define  are to be  a protocol  more  concisely and completely using a tool such as this than to rely on ad hoc methods. Moreover, the s p e c i f i c a t i o n produced is in machine-readable form (and in f a c t , may be used  as input  to  [BlBu82,BlTe82]).  automated implementation generators There  or  are, nevertheless, some awkwardness  path finding  programs  in specifying certain  aspects of the protocol as mentioned (reuse option). Another desirable feature which is not part of  this technique  is to allow grouping of related transitions by common  current states or more appropriately by occurrence of certain events (as is done in the  -56-  ISO F D T description technique [BoRa82]).  -57-  BIBLIOGRAPHY  [ACNR83]  J . P . Ansart, V. C h a r i , M . N e y e r , O. R a f i q , D. Simon, " D e s c r i p t i o n , Simulation and Implementation of C o m m u n i c a t i o n Protocols using P D I L " , Proceedings of the A C M S I G C O M M Conference, p l l 2 - 1 2 0 , Mar 1983.  [ARCh82]  J.P. Ansart, O. Rafiq, V. Chari, "Protocol Description and Implementation Language", Protocol Specification, Testing, and V e r i f i c a t i o n , C.Sunshine (ed.), N o r t h - H o l l a n d Pub. C o . , p l O l - 1 1 2 , .IFIP, 1982.  [ACDi82]  J . M . A y a c h e , J . P . C o u r t i a t , M . D i a z , "The Design and Validation by P e t r i Nets of a Reliable Bus A l l o c a t i o n P r o t o c o l " , I E E E C H , p221-228, 1982.  [Bill82]  J . B i l l i n g t o n , "Specification of the Transport Service using N u m e r i c a l P e t r i N e t s " , P r o t o c o l . S p e c i f i c a t i o n , Testing, and V e r i f i c a t i o n , C.Sunshine (ed.), N o r t h - H o l l a n d Pub. C o . , p77-100, IFIP, 1982.  [BlBu82]  T . P . Blumer, J . C . Burrus, "Generating a Service Specification of a Connection Management P r o t o c o l " , P r o t o c o l S p e c i f i c a t i o n , Testing, and V e r i f i c a t i o n , C.Sunshine (ed.), N o r t h - H o l l a n d . Pub C o . , p l 6 1 - 1 7 0 . IFIP, 1982.  [BlTe82]  T . P . Blumer, R . L . Tenney, " A F o r m a l Specification Technique and Implementation Method f o r P r o t o c o l s " , Computer Networks, V O L 6, p201-217, 1982.  [Boch78]  G.V. Bochmann, " F i n i t e State Description of C o m m u n i c a t i o n P r o t o c o l s " , Computer Networks, V O L . 2 , p361-372, 1978.  [Boch80]  G.V. Bochmann, " A General Transition Model for Protocols C o m m u n i c a t i o n Services", I E E E Transactions on C o m m u n i c a t i o n s , C O M - 2 8 , N O 4, p643-650, Apr 1980.  [BoRa82]  G.V. Bochmann, K . S . Raghunathan, "Example Description of the Transport Service", Contribution to the meeting (July 1982) of the Subgroup B of the ISO TC97/SC16/WG1 ad hoc group on F D T , Jun 1982.  [BoSu80]  G.V. Bochmann, C . A . Sunshine, " F o r m a l Methods in Communication P r o t o c o l Design", I E E E Transactions on C o m m u n i c a t i o n s , V O L C O M - 2 8 , NO 4, p624-631, Apr 1980.  [BCGJ82]  G.V. Bochmann, E. C e r n y , M . Gagne, C . J a r d , A . L e v e i l l e , C . L a c a i l l e , M . Maksud, K . S . Raghunathan, B. Sarikaya, "Some Experience with the Use of F o r m a l Specifications", Protocol S p e c i f i c a t i o n , Testing, and V e r i f i c a t i o n , C.Sunshine (ed.), N o r t h - H o l l a n d Pub. C o . , p l 7 1 - 1 8 5 , IFIP, 1982.  -58-  and VOL  [Dant80]  A . Danthine, " P r o t o c o l Representation with F i n i t e - S t a t e M o d e l s " , IEEE Transactions on Communications, V O L C O M - 2 8 , N O 4, Apr 1980.  [DaBr78]  A . Danthine, J . Bremer, " M o d e l l i n g and V e r i f i c a t i o n of E n d - t o - E n d Transport P r o t o c o l s " , Computer Networks, V O L 2, p381-395, 1978.  [Diaz82]  M . D i a z , "Modeling and Analysis of C o m m u n i c a t i o n and Cooperation Protocols Using P e t r i Net Based Models", C o m p u t e r Networks, V O L 6, p419-441, 1982.  [Divi82]  B.L. D i V i t o , "Integrated Methods for P r o t o c o l Specification and Verification", Protocol Specification, Testing, and Verification, C.Sunshine (ed.), N o r t h - H o l l a n d . Pub. C o . , p411-433, IFIP, 1982.  [Good77]  D. G o o d , "Constructing Verified and R e l i a b l e Communications Procesing Systems", A C M Software Engineering Notes, VOL- 2(5), O c t 1977.  [GoCo78]  D. G o o d , - R . M . C o h e n , " V e r i f i a b l e C o m m u n i c a t i o n Processing in Gypsy", Proceedings of the 17th I E E E Computer Society International Conference ( C O M P C O N ) , p28-35, Sep 1978.  [GoMa78]  M . G . Gouda, . E . Manning, "How to Describe Waterloo C C N G E - R e p o r t E - 7 6 , Mar 1978.  Protocols", University  of  [IS081]  International Organization for Standardization? " A F D T based on Extended State Transition M o d e l " Working D r a f t , Boston, Dec 1981.  an  [IS082]  International Organization for Standardization, "Reference Model of Open System Interconnection", ISO/TC97/SC16, D r a f t ISO/DIS 7498, 1982.  [IS083p]  International Organization Oriented Session P r o t o c o l Mar 1983.  [IS083s]  International Organization for Standardization, "Basic Oriented Session Service D e f i n i t i o n " , ISO/TC97/SC16/WG6, 1983.  [JuVu84]  W. Jurgensen, S.T. Vuong, " C S P and C S P N e t s : A Dual Model for P r o t o c o l - Specification and V e r i f i c a t i o n " , to be published in Proceedings of the Fourth International Workshop on P r o t o c o l S p e c i f i c a t i o n , Testing and V e r i f i c a t i o n , Jun 1984.  [NBS81a]  " S p e c i f i c a t i o n of P r o t o c o l " , Report 1981.  [NBS81b]  " S p e c i f i c a t i o n of the Transport P r o t o c o l , Volume 3: Extended Class P r o t o c o l " , Report No I C S T / H L N P 8 1 - 1 3 , N a t i o n a l Bureau of Standards, 1981.  for Standardization, "Basic Connection S p e c i f i c a t i o n " , ISO/TC97/SC16/WG6, D r a f t , Connection Draft, Mar  the Transport P r o t o c o l , Volume 2: Basic Class No I C S T / H L N P 8 1 - 1 2 , N a t i o n a l Bureau of Standards,  -59-  [NBS83a]  "Specification of a Transport P r o t o c o l for Computer Communications, Volume 2: Class 2 P r o t o c o l " , Report No I C S T / H L N P 8 1 - 1 2 , National Bureau of Standards, 1983.  [NBS83b]  "Specification of a Transport Protocol for Computer C o m m u n i c a t i o n s , Volume 3: Class 4 P r o t o c o l " , Report No I C S T / H L N P 8 1 - 1 2 , N a t i o n a l Bureau of Standards, 1983.  [RWZa78]  H. Rudin, C . H . West, P. Zafiropulo, " A u t o m a t e d Protocol Validation: One C h a i n of Development", Computer Networks, V O L 2 , p373-380, 1978.  [Schi80]  S.. Schindler, " A l g e b r a i c and Model Specification Techniques", Proceedings of the 13th H a w a i i International Conference o n . System Sciences, Jan 1980.  [Schw81]  D . . Schwabe, " F o r m a l Specification and V e r i f i c a t i o n Establishment Protocol", Proceedings of the Communications Symposium, M e x i c o C i t y , O c t 1981.  [Sidh81]  D.P.. Sidhu, "Toward Constructing Verifiable^ C o m m u n i c a t i o n P r o t o c o l s " , P r o t o c o l Testing - Towards P r o o f ? , I N W G / N P L Workshop Proceedings, National Physical Laboratory, Teddington, U . K . , V O L 1, p75-141, May 1981.  [SiKa82]  G . A . Simon, D . J . . K a u f m a n , " A n Extended Finite State Machine Approach to P r o t o c o l ..Specification", P r o t o c o l . S p e c i f i c a t i o n , Testing, and V e r i f i c a t i o n , C.Sunshine (ed.), N o r t h - H o l l a n d Pub. C o . , p l l 3 - 1 3 3 , IFIP, 1982.  [Suns78]  C A . - Sunshine, "Survey of Protocol Definition and Techniques", Computer Networks, V O L 2, p346-350, 1978.  [Suns79]  CA. Sunshine, " F o r m a l Techniques for V e r i f i c a t i o n " , IEEE Computer, Aug 1979.  [Suns81]  C A . . Sunshine, "Formal Modeling of Communication U n i v e r s i t y of Southern C a l i f o r n i a ISI R R - 8 1 - 8 9 , M a r 1981.  [SRWG80]  G . D . Schultz, D . B . Rose, C . H . West, J . P . G r a y , "Executable Description and Validation of S N A " , I E E E Transactions on Communications, V O L C O M - 2 8 , NO 4, p661-676, Apr 1980.  [STEG82]  C A . Sunshine, D . H . Thompson, R.W. E r i c k s o n , S . L . G e r h a r t , D. Schwabe, ''Specification and V e r i f i c a t i o n of C o m m u n i c a t i o n Protocols in A F F I R M using .State Transition Models", I E E E Transactions on Software Engineering, V O L S E - 8 , N O 5, p460-489, Sep 1982.  [TeB181]  R. Tenney , T. Blumer, " A n automated F o r m a l Specification Technique for Protocols", Report No I C S T / H L N P - 8 1 - 1 5 , N a t i o n a l Bureau of Standards, 1981.  -60-  Protocol  of a Connection Seventh Data  Verification  Specification  and  Protocols",  . .[VuCo82].  S.T. Vuong, D.D. C o w a n , " U N I S P E X - A Unified Model for Protocol Specification and V e r i f i c a t i o n " , University of Waterloo Technical Report C S - 8 2 - 5 2 , Nov 1982.  .-[Wats82]  R.W. Watson, " A n Experience in Transport Protocol Specification using an A l g o r i t h m i c Programming Language", P r o t o c o l Specification, Testing; and V e r i f i c a t i o n , C.Sunshine (ed.), N o r t h - H o l l a n d Pub. C o . , p237-247, IFIP, 1982.  -61-  APPENDIX - Specification of the ISO Session Protocol  { constant declarations } const V E R S I O N = 1 ; { protocol version number } MAX_CN_DATA_SIZE MAX_AC_DATA_SIZE M A X _ R F_D A T A_SI Z E MAX_FN_DATA_SIZE M A X _ _D N.__ DA . .T.A . _SIZE MAXJ\IF_DATA_SIZE M A X . AB D A T A SIZE TR_TOKEN MA_TOKEN SY T O K E N DK_TOKEN  = 64; max size of user data field in C N = 64; max size of user data field in A C = 64; max size of user data f i e l d in R F = 32; max size of user data f i e l d in F N = 32; , max size of user data f i e l d in D N } =. 32; f max size of user data field in N F } = 3 ; { max size of user data field in A B }  = $01; { r e l e a s e token mask } = $04; { major sync/activity token mask } = $10; { minor sync token mask } = $40; { data token mask }  C L E A R _ T C = $00; { clear t c when session ends mask} { abort reason masks } U S E R _ A B O R T = $02; { user abort } P R O T _ E R R O R = $04; { protocol error N O _ R E A S O N = $08; { no reason given N O T _ E O A C T = $01; { not end of a c t i v i t y flag } E O A C T = $00; { end of a c t i v i t y flag } EOSSDU. = $01; { mark end of SSDU flag } C O N F I R M . = $01; { c o n f i r m required on minor sync fig} N O T _ C O N C A T = $00; { no concatenation of SPDU's flag } C O N C A T = $01; { concatenation of SPDU's f l a g }.. { session requirement masks } H D U P L E X = $0001;{ half duplex } D U P L E X = $0002;{ f u l l duplex } S _ E X P = $0004;{ session expedited } M I N _ S Y N C = $0008;{ minor synchronization } M A J _ S Y N C = $0010;{ major synchronization } R E S Y N C = $0020;{ resynchronization } A C T = $0040;{ a c t i v i t y management } N E G _ R E L E A S E = $0080;{ negotiated release } C A P = $0100;{ capability data } E X C E P T I O N S = $0200;{ exception reporting } T Y P E D = $0400;{ typed data } QOS = D E F A U L T 1 ; { quality of service } I N I T _ S Y N C _ S E R I A L " = D E F A U L T 2 ; { i n i t i a l synchronize serial no (1) } T A B I N T E R V A L = D E F A U L T 3 ; { abort t i m e r i n t e r v a l } -62-  { implementation dependent options } T C _ D I S C O N N E C T = C L E A R _ T C ; { clear tc when clear session con } T C _ E X P E D I T E D = F A L S E ; { no expedited transport service } P R O T O C O L J D P T I O N S = N O T _ C O N C A T ; { no concatenation of SPDU's }  { d e c l a r a t i o n of  types }  type subset_type - ( { subset of protocol } BASIC_COMBINED, BASIC_SYNCHRONIZED, BASIC_ACTIVITY );  boolean = ( { boolean values } FALSE, TRUE  0;  result_type = ( { connect result reply codes } REASON_NOT_SPECIFIED, PROTOCOL_VERSION_UNKNOWN, SUBSET_NOT_SUPPORTED, U N A C C E P T ABLE_SESS_CON_P A R A M , ACCEPTOR_ADDR_INVALID, USER_REJECT, USER_NOT_CONNECTED, AFFIRMATIVE );  reason type = ( { reason for release of connection } NO_SPECIFIC_REASON, MEMORY_OVERFLOW, LOCALJJSER^ERROR, SEQUENCE_ERROR, DEMAND DATA_TOKEN, PROTOCOL_ERROR, UNDEFINED, TC_GONE, TYPED DATA ); timer_.type = ( { t i m e r types } inactivity } TIN, abort } TAB );  token_type = ( { values taken by tokens } NOT_AV AIL A B L E , INITIATOR_SIDE, ACCEPTOR_SIDE, CHOICE ); -63-  pdu_type = ( { types of SPDU's } C N , A C , R F , { connection } F N , D N , N F , A B , A A , {release/abort } P T , G T , G T A , { tokens } E X , P R , { expedited } C 2 C H , C 2 R H , { secondary mark} DT, { data }• M K B , M C B , M K D , M C D , { synchronize } R S , R A , { resync } A S , A R , A D , A D A , AI, ,AIA, { a c t i v i t y } C D , C D A , { capability } E R , E D { exceptions } );  act_type = ( { a c t i v i t y s w i t c h } NOT_AVAILABLE, ON, OFF ); resync_type. = ( { resynchronization s w i t c h } NOT_AVAILABLE, RESTART, ABANDON, INTERRUPT, DISCARD );  act_begin type = ( { type of a c t i v i t y begin request } S T A R T , ~\ begin } CONTINUE (resume } ); { implementation dependent types } addr_type { session addr: host + t c addr's } h_addr_type { host address type } tc_addr_type { t c address type } int_type { integer type - 16 bits} octet_type { byte - 8 bits } data_type { ptr to string }  -64-  sync_serial_type { synchronization serial number - 6 octets}  5 act_id_type { a c t i v i t y identifier - 3 octets }  5 sess_id_type { session identifier type - max 64 octets}  5 qos_type { quality of service }  5 Pdu = { possible fields in a S P D U } record pversion : o c t e t _ t y p e ; ptype : pdu_type; pinitiator_addr, pacceptor_addr : h_addr_type; ptoken : token_type; preason : reason_type; pno_reason_field : boolean; presult : result_type; p_options : o c t e t _ t y p e ; psess_req : int_type; p C N _ r e f : int_type; psess_id : sess_id_type; pmax_SPDU_in, pmax_SPCU_out : int_type; psync_serial : s.ync_serial_type; pdata : d a t a t y p e ; pqos : qos_type; pnew_act_id, pold_act_id : act_id_type; pmisc : octet_type end; machine = { local machine state variables } record C N _ r e f : int_type; { ref to local F S M structure } C N _ o r i g i n : boolean; { initiator of connection } max _ S P D U _ i n , { max sizes of SPDU's. } m a x _ S P D U _ o u t : int type; sess_req : int_type; •f session requirements } laddr, { l o c a l and foreign session } faddr : addr_type; { addresses } lhost, { l o c a l and foreign host name} fhost : h_addr_type; l t c , { l o c a l and foreign t c addr } f t c : tc_addr_type; user_data : data_type; { user data } reason : reason_type; { reason for release of con } result : result_type; { result of connection req } act_end. conf_pending, { awaiting end of act confirm} duplex, X in duplex mode? } -65-  ec_report, { exception report avail? } e c _ d a t a , { exception data avail ? } tc_expedited, { expedited transport service} session_expedited : boolean; { expedited session s e r v i c e ? } dk_token, { data token } tr_token, { release token } sy_token, { minor s y n c . t o k e n } ma_token : token_type; { major sync/activity token } protocol_opts : octet_type; { protocol options } sync_serial_confirmed, { last confirmed sync s e r i a l } sync_serial : sync_serial_type; { current sync serial no } qos : qos_type; { quality of service } a c t i v i t y : act_type; { status of a c t i v i t y } resync : resync_type; { resynchronization type } sess_id : sess_id_type { session identifier } end;  declaration of interface events and associated parameters } — parameters with default value given are optional } { *********** System interface ************** } interface Name T i me )];  [  to S : TIMER.request : timer_type; : i nt_t ype  (  interface Name  [  from S: TIMER.response : timer type  (  )];  interface Name )]; |  [ :  to S : TIMER.cancel timer_type  *********** T r a n s p o r t  (  interface  ***********  i n t e r f a c e [ to T: T_CONNECT.request ( C a 1 1 e d _ a d d r es s , Cal 1 i ng_address : t.c_addr_type ; Exp_data_option : boolean default Qua 1 _ o f _ s e r v i c e : q o s _ t y p e ; User data : data type d e f a u l t )];  FALSE; NULL  "  i n t e r f a c e [ from T: T_CONNECT.indication ( Ca11ed_address, C a 1 1 i n.g_addr e s s : t c _ a d d r _ t y p e ; Exp_data_option : boolean; Qua 1 _ o f _ s e r v i c e : q o s _ t y p e ; User data : d a t a _ t y p e d e f a u l t NULL )];  -66-  }  i n t e r f a c e [ to T: T_CON\IECT.response ( Qua 1 _ o f _ s e r v i c e : q o s _ t y p e ; R e s p o n d i n g _ a d d r es s : t,c_addr_type ; Exp_data_option : boolean; User_data : data type d e f a u l t  NULL  )];  i n t e r f a c e [ f r o m T : T _ C O N N E C T . c o n f i rm ( Qual_of_service : qos_type; Res p o n d i n g _ a d d r e s s : tc_addr_type; Exp_data_option : boolean; User data : data type d e f a u l t )]; interface Data  [  to  T:  T_DATA.request : data type  interface Spdu )];  [  f r o m T:  interface Data  [  to  [  f r o m T:  NULL  (  )];  T:  T_DATA.indication : Pdu  (  T_EXPEDITED_DATA.request : data_type  (  )];  interface .Spdu  T_EXPEDITED_DATA.indication : Pdu  (  )];  i n t e r f a c e [ to User_data  T:  T_DISOONNECT.request ( : d a t a _ t y p e d e f a u l t NULL  )];  i n t e r f a c e [ f r o m T: Reason User data )]; {  T _ D I S O O N N E C T . i h d i c a t i on ( : result_type; : d a t a _ t y p e d e f a u l t NULL  ********* S e s s i o n U s e r  i n t e r f a c e [ f r om U : I dent i f i er In i t i a t o r _ a d d r , Acceptor_addr Qua 1 _ o f _ s er v Ses s i o n _ r e q , Sync_s e r i a 1 In i t _ d k _ t o k e n , Ini t _ t r _ t o k e h , Ini t _ s y _ t o k e n , Ini t_ma_token User data  interface  *********  S_CONMECT.request : sess_id_type; addr_type; qos_t ype; i nt_type; sync_serial_type  }  (  default  NULL;  token_type default NOT_AVAILABLE; d a t a type d e f a u l t NULL - 6,7 -  )]; interface [ t o U : S CONNECT.indication ( Identifier s es s _ i d _ t y p e ; I ni t i a t o r _ a d d r addr_type; Acceptor_addr qos_type; Qual_of_serv Sess i on_req i nt_t ype; Syn,c_ser i a 1 s y n c _ s e r i a 1_t y p e ; In i t _ d k _ t o k e n , I n i t_t r_token, In i t _ s y _ t o k e n , In i t _ m a _ t o k e n token_t ype; User data d a t a _ t y p e d e f a u l t NULL )]; i n t e r f a c e [ from U: I den t i f i er Acceptor _addr Result Qua 1 _ o f _ s e r v Sess i on_ req Syn,c_ser i a l Ini t_dk_t o k e n , Ini t_,t r_ t o k e n , Ini t_sy_t o k e n , In i t _ m a _ t o k e n U s e r dat a  S_CONNECT.response ( s es s _ i d _ t y p e ; addr_type; result_type; qos_type; i nt_type; syn,c_serial_type;  :  token_type; data type d e f a u l t  NULL  )];  i n t e r f a c e [ to U: S C O N N E C T . c o n f i r m ( Identifier s es s _ i d _ t y p e ; addr_type; Acceptor_addr r e s u l t _ t ype; Res u1t qos_type; Qual_of_serv i n t_t ype; Sess i on_req sync_seri al_type; Sync_ser i a 1 In i t _ d k _ t o k e n , In i t _ t r _ t o k e n , Init_sy_token, : token_type d e f a u l t NOT_AVAILABLE; In i t _ m a _ t o k e n : d a t a _ t y p e d e f a u l t NULL User data )];  "  i n t e r f a c e [ from User data )]; " i n t e r f a c e [ to U: User data  U:  S_RELEASE.request ( : data type d e f a u l t  NULL  S RELEASE.indication : data_type  )];  interface [ Result  from U:  S_RELEASE.response : result type; -68-  (  User_data )];  :  i n t e r f a c e [ to U: Result User_data  data_type  default  NULL  S _ R E L E A 5 E . c o n f i rm ( : result_type; : data_type  )]; i n t e r f a c e [ from U: User data )]; " interface  User  [  to  U:  (  S_U_ABORTorequest  :  data  type  S_U_ABORT.indication  data  :  data  (  type  )];  interface [ Reason  to U:  S_P_ABORT.indication : reason type  interface Data )];  [  from U:  interface Data  [  to U:  interface Data )];  [  from U:  interface Data  [  to U:  interface [ Reason )];  to U:  S_DATA.request : data_type  S_DATA.indication : data type  (  (  (  )];  S_EXPEDITED_DATA.request : data type  (  S_EXPEDITED_DATA.indication : data type  (  )];  interface [ fromU: Reason User data  S_P_EXPECTION_REPORT.indication : reason type S_U_EXPECTION_REPORT.request : reason_type; : d a t a t y p e d e f a u l t NULL  )];  interface [ t o U : Reason User data  S_U_EXPECTION_REPORT.indication : reason_type; : d a t a t y p e d e f a u l t NULL  )];  i n t e r f a c e [ from U: User data )]; ~  S_TYPED_DATA.request : data_type  -69-  (  (  i n t e r f a c e [ to U: User data )]; interface Token  S_TYPED_DATA.indication : data type  [  from U:  [  to U:  S_TOKEN_GI V E . r e q u e s t : octet_type  (  .(  )]; interface Token  S_TGKEN_GIVE.indication : octet_type .  (  )];  i n t e r f a c e [ from U: Token . User data  S_TOKEN_PLEASE.request ( : octet_type; : d a t a _ t y p e d e f a u l t NULL  )];  interface [ t o U : Token User data  S_TOKEN_PLEASE.indication ( : octet_type; : d a t a t y p e d e f a u l t NULL  i n t e r f a c e [ from U: ..Confirm Sync_point User_data  S_SYNC_MINOR.request ( : o c t e t _ t y p e d e f a u l t NULL; : sync_serial_type; : d a t a _ t y p e d e f a u l t NULL  )];  i n t e r f a c e [ to U: Confirm Sync_point User data  S_SYNC_MINDR.indication ( : o c t e t _ t y p e d e f a u l t NULL; : sync_serial_type; : d a t a _ t y p e d e f a u l t NULL  i n t e r f a c e [ from U: „Sync_point User_data i n t e r f a c e [ to U: Sync_point User_data )];  S_SYNC_MIN3R.res ponse ( : s y n c _ s e r i a 1 __t y pe ; : d a t a _ t y p e d e f a u l t NULL  S _ S Y N C ^ M I N O R . c o n f i rm ( : sync_seria 1_type; : d a t a _ t y p e d e f a u l t NULL  interface [ fromU: ,Sync_point User data  S_SYNC_MAJOR.request ( : sync_serial_type; : d a t a _ t y p e d e f a u l t NULL  )];  i n t e r f a c e [ to U: .Sync_point User data )]; ~  S_SYNC_MAJOR.indication ( : s y n c _ s e r i a 1_type; : d a t a _ t y p e d e f a u l t NULL  -70-  i n t e r f a c e [ from U User data )];  :  S_SYNC_MAJCR.res ponse data type  (  "  i n t e r f a c e [ to U: User data )];  :  S _ S Y N C _ M A J C R . c o n f i rm ( : data type  "  interface [,fromU: Activity_id Type 01d_act_id Sync_point 01d_sess_id User data  S_ACTIVITY_BEGIN.request ( : act_id_type; : act_begin_type; : a c t _ i d _ t y p e d e f a u l t NULL; : s y n c _ s e r i a 1_type d e f a u l t NULL; : i n t _ t y p e d e f a u l t NULL; : d a t a _ t y p e d e f a u l t NULL  )];  i n t e r f a c e [ to U: Activity_id Type 01d_act_id Sync_point 01d_sess_id User data )];  S_ACTIVITY_BEGIN.indication ( : act_id_type; : act_begin_type; : a c t _ i d _ t y p e d e f a u l t NULL; : syn.c_ser i a l _ t y p e d e f a u l t NULL; : i n t _ t y p e d e f a u l t NULL; : d a t a type d e f a u l t NULL  "  -  interface [ fromU: Syn.c_point User data )];  S_ACTIVITY_END.request ( : s y n c _ s e r i a 1 _ t y pe ; : d a t a type d e f a u l t NULL  "  i n t e r f a c e [ to U: Sync_point User data )]; "  S_ACTIVITY_EI\D.indication ( : sync_seria 1_type; : d a t a t y p e d e f a u l t NULL  i n t e r f a c e [ from U: User data )];  .  S_ACTIVITY_END.res ponse ( : d a t a type d e f a u l t NULL  "  i n t e r f a c e [ to U: User data )]; " interface  S _ A C T I V I T Y _ E N D . c o n f i rm ( : d a t a t y p e d e f a u l t NULL  [  from U:  [  toU:  interface )];  [  from U:  interface  [  to U:  S_ACTIVITY_INTERRUPT.request  (  )];  interface  S_ACTIVITY_INTERRUPT.indication  (  )]; S_ACTIVITY_INTERRUPT.response  S ACTIVITY  INTERRUPT.confirm  -71-  (  (  )];  interface  [  fromU:  interface  [  to U:  interface  [  fromU:  interface  [  to U:  S ACTIVITY DISCARD.request  (  )];  S ACTIVITY D I S C A R D . i n d i c a t i o n  )];  S_CAPABILITY_DATA.request : data type  (  ( (  "  i n t e r f a c e [ to U: User_data  )3 ;  S ACTIVITY DISCARD.response  S ACTIVITY DISCARD.confirm  )]; interface [ fromU: User data  (  S_CAPABILITY_DATA.indication : data_type  i n t e r f a c e [ from U: User data )]; "  S_CAPABILITY_DATA.response : data type  interface [ fromU: User_data ) ] ;  S_CAPABILITY_DATA.confirm : data_type  (  (  (  state abbreviations } F S M starts at i n i t i a l state and ceases to exist at f i n a l state ; other abbreviations are used in current state f i e l d of a F S M transition } state any_state = ( UNCONNECTED, CALLING, CALLED, IDLE, WAIT_FOR_AC_SPDU, WAIT_FOR_GTA_SPDU, WAIT_FOR_AA_SPDU, WAIT_FOR_DN_SPDU, WAIT_FOR_MCD_SPDU, WAIT_FOR_CDA_SPDU, WAIT_FOR_AIA_SPDU, WAIT_FOR_ADA_SPDU, W A I T _ F O R _ r e c o ver y _ S P D U , WAIT_FOR_S_CONNECT_RESP, WAIT_FOR_S_RELEASE_RESP WAIT_FOR_S_MCD_RESP. WAIT F O R S AI R E S P , -72-  WAIT_FOFTS_AD_RESP, " ^ WAIT_FOR_CDA_RESP, WAIT_FOR_S_recover.y_REQ  abort_allowed = ( { session may be aborted } GALLING,  CALLED, IDLE, WAIT_FOR_S_CONNECT_RESP, WAIT_FOR_S_RELEASE_RESP WAIT_FOR_S_MCD_RESP, WAIT_FOR_S_AI_RESP, WAIT_FOR_S_AD_RESP, WAIT_FOR_CDA_RESP, W AIT_FOR_AC_SPDU, WAIT_FOR_DN_SPDU, WAIT_FOR_MCD_SPDU, WAIT_FOR_GTA_SPDU, W AIT_FOR_CD A_SPDU, WAIT_FOR_AIA_SPDU, WAIT_FOR_ADA_SPDU,  WAIT_FOR_recovery_SPDU, WAIT_FOR_S_recovery_REQ ); pabort_allowed = ( { session may be aborted } CALLED, IDLE, WAIT_FOR_S_CONNECT_RESP, WAIT_FOR_S_RELEASE_RESP WAIT_FOR_S_MCD_RESP, WAIT_FOR_S_AI_RESP, WAIT_FOR_S_AD_RESP, WAIT_FOR_CDA_RESP, W AIT_FO R _ A C _ S P D U , WAIT_FOR DN_SPDU,  W AIT_FOR>1CD_SPDU,  WAIT_FOR_GTA_SPDU, WAIT_FOR_CDA_SPDU, WAIT_FOR_AIA_SPDU, WAIT_FOR_ADA_SPDU, WAIT_FOR_recovery_SPDU, WAIT_FOR_S_recover.y_REQ ); I D L E _ o r _ D N _ G T A _ M C D = ( { idle or awaiting one of D N , G T A , M C D SPDUs } IDLE, WAIT_FOR_DN_SPDU, WAIT_FOR_GTA_SPDU, WAIT_FOR_MCD_SPDU ); I D L E _ o r _ D N - = ( { idle or awaiting an D N S P D U }  -73-  IDLE, WAIT_FOR_DN_SPDU ); I D L E _ o r _ M C D =• ( { idle or awaiting an M C D S P D U } IDLE, WAIT_FOR_MCD SPDU ); IDLE_or R E L R = ( { idle or awaiting a session release response} IDLE, WAIT_FOR S R E L E A S E RESP );  I D L E _ o r _ M C D R = ( { idle or awaiting a response for a sync ind } IDLE,. WAIT_FOR_S_MCD_RESP ); I D L E _ o r _ R E L R _ M C D R = ( { idle or awaitng a response for either a release or synchronization indication } IDLE, W A I T _ F O R_S_R E L E A SE_R E S P , WAIT F O R S M C D R E S P ); " " I D L E _ o r _ D N _ M C D = ( { idle or awaiting a D N or M C D S P D U } ' IDLE, WAIT_FOR_MCD_SPDU WAIT_FOR_DN_SPDU, ); IDLE_or_GTA_MCDR = ( { idle synchronization response } IDLE, WAIT_FOR_S_MCD_RESP, WAIT_FOR G T A SPDU  or  awaiting  a  give  token  ack , S P D U  );  .  I D L E _ o r _ r e e _ R E Q = ( { idle or awaiting a recovery request } IDLE, WAIT_FOR_S_recovery_REQ ); I D L E _ o r _ r e c _ S P D U = ( { idle or awaiting a recovery S P D U } IDLE, WAIT_FOR_recovery_SPDU w a i t _ D N _ M C D _ S P D U = ( { waiting for either a D N or M C D S P D U } WAIT_FOR_MCD_SPDU, WAIT_FOR_DN_SPDU );  -74-  or  initial = U N C O N N E C T E D ; final = U N C O N N E C T E D ;  { i n i t i a l state } { f i n a l state }  • declaration of functions and procedures } 'primitive' described verbally } 'forward' defined } function acceptable_CN( CN_pdu : Pdu ) : boolean; primitive; function a c c e p t a b l e _ A C ( AC_pdu : Pdu ) : boolean; primitive; function AC_reject_reason( AC_pdu : Pdu ) : result_type; primitive; function CN_reject_reason( CN_pdu : Pdu ) : result_type; primitive; function a l l o c _ r e f : int_type; primitive; function arith_and( a r g l , arg2: octet_type ): boolean; primitive; procedure assign_token_accept( token_item : octet_type ); forward; procedure assign_token_give( token_item : octet_type ); forward; procedure clear_session; primitive; function get_host( sess_addr : addr type ): h_addr_type; primitive; function get_tc_addr( sess_addr : addr_type ): tc_addr_type; primitive; procedure increment_sync( ss: sync_serial_type ); primitive; procedure i n i t i a l i z e _ m a c h i n e ; forward; function intersect( a r g l , arg2: octet_type ): o c t e t _ t y p e ; primitive; procedure intersect_sr( sess_requirements : int_type ); primitive; function isatokenin( token, token_item : octet_type ): boolean; primitive; function mapSaddr( haddr : h_addr_type; tc_addr : tc_addr_type ): addr_type; -75-  primitive; function min( a, b: int_type ): int_type; primitive; function other_side( token : token_type ): boolean; forward; function set_qos( qos : qos_type ) : qos_type; primitive; procedure set_sr( session_requirements : int_type ); primitive; procedure set_tokens( token_item : octet_type); primitive; function size( data unit : data_type ): int_type; primitive; function tc_disc_jeason( reason : reason_type ): result_type; primitive; function testSaddr( sess_addr : addr_type ): boolean; primitive; function this_side( token : token_type ): boolean; forward; function token_other_side( t o k e n _ i t e m : octet_type ): boolean; forward; function token_this_side( token_itenru: octet_type ): boolean; forward; function union( a r g l , arg2: octet_type ): o c t e t _ t y p e ; primitive; function valid_sp( sync : sync_serial_type ) : boolean; primitive; function pduCN( C N _ r e f e r e n c e : int_type; C N _ i d : sess_id_type; version : o c t e t _ t y p e ; lhost, fhost : h_addr_type; dk_token, rl_token, sm_token, ma_token : token_type; protocol_options: o c t e t _ t y p e ; in_max_SPDU, o u t _ m a x _ S P D U : int_type; i n i t j n a r k : sync_serial_type; session_req : i n t _ t y p e ; user_data : data_type ): data_type; p r i m i t i v e ; function pduAC( C N _ r e f e r e n c e : int_type; -76-  C N _ i d : sess_id_type; version : o c t e t _ t y p e ; lhost, fhost : h_addr_type; dk_token, rl_tqken, smjtoken, ma_token : token_type; protocol_options: o c t e t _ t y p e ; in_max_SPDU, o u t _ m a x _ S P D U : int_type; init_mark : sync_serial_type; session_req : i n t _ t y p e ; user_data : data_type ): data_type; p r i m i t i v e ; function pduRF( C N _ r e f e r e n c e : int_type; tc_disconnect : o c t e t _ t y p e ; version : o c t e t _ t y p e ; result : result_type; session_req : int_type; user_data : data_type ): data_type; p r i m i t i v e ; function p d u C K pdu_code : pdu_type; { F N , D N , N F , A B , A A , P T , G T , G T A , P R } C N _ i d : int_type; a r g l : o c t e t _ t y p e ; { tc_disc : F N , . A B , P T } token i t e m : P T , G T { prepare type : P R } user_data : data_type { F N , D N , N F , A B , P T } ): data_type; p r i m i t i v e ; function pduDT( pdu_code : pdu_type; { D T , E X , E R , C D A , C D , A D , AI } C N _ i d : int_type; data : data_type ): data_type; p r i m i t i v e ; function pduC2s( pdu_code : pdu_type; { ' M K B , M C B , M K D , M C D , R S , R A , E D } C N _ i d : int_type; serial_no : sync_serial_type; { M K B , M C B , M K D , M C D , R S , sync_item : o c t e t _ t y p e : { M K B , M K D , R S , E D } user_data : data_type { M K B , M K D , R S , R A , E D } ): data_type; p r i m i t i v e ; ;  function pduC2a( pdu_code : pdu_type; { A S , A R } C N _ i d : int_type; serial_no : sync_serial_type; o a c t i v i t y _ i d : act_id_type; AS } n a c t i v i t y _ i d : act_id_type; { A S , A R } user_data : data_type { A S , A R } ): data_type; p r i m i t i v e ;  { definition of 'forward' functions and procedures }  function other_side( token ): boolean; { T R U E if 'token' is on peer side } begin other side := ( C N _ o r i g i n and (token s A C C E P T O R _ S I D E ) ) or ( (not CN_origin) and (token = INITIATOR_SIDE) ); end; function this_side( token ): boolaen; { T R U E if 'token' is on this side } begin this_side := ( C N _ o r i g i n and (token = INITIATOR_SIDE) ) or ( (not CN_origin) and (token = A C C E P T O R _ S I D E ) end;  );  function token_this_side( t o k e n _ i t e m : octet_type ): boolean; . { s p e c i f i e d tokens are on this side } var here: boolean; begin  if ( isatokenin(TR_TOKEN, token item) ) then here := this_side( tr_tokenT else here := T R U E ;  if ( i s a t o k e n i n ( D K _ T O K E N , token_item)) then here := here and this_side( dk_token); if ( i s a t o k e n i n ( S Y _ T O K E N , token_item)) then here := here and this_side( sy_token); if ( i s a t o k e n i n ( M A _ T O K E N , token_item ) then here : = here and this_side( ma_token); token_this_side := here end; function token_other side( t o k e n _ i t e m : octet_type ): boolean; { s p e c i f i e d tokens are on peer entity side } var there: boolean; begin if (isatokeninCTRJTOKEN, token_item)) then there other_side( tr_token) else there := T R U E ; if ( i s a t o k e n i n ( D K _ T O K E N , token_item)) then there : - there and other_side( dk_token); if ( i s a t o k e n i n ( S Y _ T O K E N , token_item)) then there := there and other_side( sy_token); if ( i s a t o k e n i n ( M A _ T O K E N , token_item)) then there := there and other_side( ma_token); token other side := there -78-  end; procedure assign_token accept( token_item ); { assign tokens to this side } var token_value: token_type; begin if (CN_origin) then token_value := I N I T I A T O R _ S I D E else token_value := A C C E P T O R _ S I D E ; if (isatokenin(TPy_TOKEN, token_item)) then tr_token := token_value; if ( i s a t o k e n i n ( D K _ T O K E N , token_item)) then dk token := token_value; if (isatokeninTSY_TOKEN, token_item)) then sy_token := token_value; if ( i s a t o k e n i n ( M A _ T O K E N , token_item)) then ma_token := token_value end; procedure assign_token_give( token_item ); { assign tokens to peer entity side } var token_value: token_type; begin if (CN_origin) then token_value := A C C E P T O R _ S I D E else token_value := I N I T I A T O R _ S I D E ; if (isatokenin(TR_TOKEN,- token_item)) then tr token := token_value; if ( i s a t o k e n i n T D K _ T O K E N , token_item)) then dk token : - token_value; if (isatokeninTSY_TOKEN, token_item)) then sy_token := token_value; if ( i s a t o k e n i n ( M A _ T O K E N , token_item)) then ma_token := token_yalue end; { i n i t i a l i z a t i o n routine to set up F S M } procedure i n i t i a l i z e _ m a c h i n e ; begin C N _ r e f := R E F J J N D E F I N E D ; laddr := A D D R J J N D E F I N E D ; faddr := A D D R _ U N D E F I N E D ; lhost := H O S T J J N D E F I N E D ; fhost : = H O S T J J N D E F I N E D ; l t c := T C J J N D E F I N E D ; f t c := T C J J N D E F I N E D ; C N _ o r i g i n .:= F A L S E ; m a x _ S P D U _ i n := M A X _ S P D U _ I N ; max_SPDU_out:= M A X _ S P D U _ O U T ; userjdata := N U L L ; act_end_conf_pending := F A L S E ; duplex := F A L S E ; ec_report i- F A L S E ;  -79-  ec_data := F A L S E ; session_expedited := F A L S E ; tc_expedited := T C _ E X P E D I T E D ; dk_token := N O T _ A V A I L A B L E ; rl_token := N O T _ A V A I L A B L E ; sm_token := N O T _ A V A I L A B L E ; ma_token : = N O T _ A V A I L A B L E ; protocol_opts := P R O T O C O L _ O P T I O N S ; qos := Q O S ; sync_serial := I N I T _ S Y N C _ S E R I A L ; sync_serial_confirmed := I N I T _ S Y N C _ S E R I A L ;  Primitive Procedures This section gives verbal descriptions of the primitive procedures and functions used in the s p e c i f i c a t i o n . The exact operation of these are determined by l o c a l implementation choices and r e s t r i c t i o n s . primitive acceptable_CN( CN_pdu ) This primitive returns a boolean value depending on whether the parameters of the C N S P D U is acceptable to the session machine. Some of the reasons for rejecting the C N S P D U may be unmatching protocol version numbers, protocol subset not supported, invalid acceptor address, insufficient resources to support another connection, unacceptable protocol options or i n i t i a l token assignments. Other l o c a l reasons for rejecting a C N may be also be considered. primitive a c c e p t a b l e _ A C ( AC_pdu ) This primitive returns a boolean value depending on whether the parameters of the accept ( A C ) S P D U is acceptable to the session machine. Some of the reasons for rejecting an A C S P D U may be unmatching protocol version numbers, protocol subset not supported, unsatisfactory max S P D U sizes/token assignments/protocol options, e t c . Other l o c a l reasons for rejecting an A C may be also be considered. primitive AC_reject_reason(  AC_pdu)  This primitive returns the reason the A C S P D U machine, (see a c c e p t a b l e _ A C primitive).  was rejected  by the session  was rejected  by the session  primitive CN_reject_reason( CN_pdu ) This primitive returns the reason the C N S P D U machine, (see acceptable C N primitive). -80-  primitive alloc_ref This primitive returns a valid number to be used as the connection i d e n t i f i e r . p r i m i t i v e arith_and( a r g l , arg2 ) This primitive returns a boolean value depending on whether the a r i t h m e t i c 'and' of its argument results in a non-zero value.  primitive clear_session This primitive connection.  releases  and resets  buffer  space and variables relevant  to  the  primitive get_host( sess_addr ) This primitive extracts given (session) address.  and returns  the host address(or  name) specified in the  primitive get^tc_addr( sess_addr ) This primitive extracts (session) address.  and returns the transport address specified in the  given  primitive increment_sync( sync_serial ) This primitive increments the synchronize s e r i a l number by one. (This is specified as a p r i m i t i v e - due to the implementation dependent nature of the length .of the number). primitive intersect( a r g l , arg2 ) This primitive returns the a r t h i m e t i c 'and' of its two arguments. primitive intersect_sr( sess_req ) This primitive readjusts the session requirement flags by intersecting the current values with that given in sess_req. primitive isatoken( token, token_item ) This primitive returns a boolean value depending on whether token is one of the tokens specified in token_item (arithmetic 'and' yields non-zero value). primitive mapSaddr( haddr, tc_addr ) -81-  This primitive returns the session address constructed by combining the given host and transport addresses.  p r i m i t i v e min( a r g l , arg2 ) This primitive returns the minimum of its two arguments. p r i m i t i v e set_qos( qos ) This primitive returns the quality of service according to the given qos and l o c a l quality of service parameters.  primitive set_sr( sess_req ) This primitive sets the session requirement flags according to the given sess_req and l o c a l requirements. primitive set_tokens( tokens_values ) This primitive sets the values of the token variables according to the parameter given and the token's existing values. (A token's value is only altered if its current value is C H O I C E — acceptor had the choice of i n i t i a l placement of tokens). p r i m i t i v e size( buf ) This primitive returns the length of the specified buffer (data_type  entity).  p r i m i t i v e tc_disc_reason( reason ) This primitive returns a result_type value from the given reason for release of the transport connection. primitive testSaddr( sess_addr ) This primitive address is v a l i d .  returns  a boolean value depending on whether  the given session  primitive union( a r g l , arg2 ) This primitive returns the arthmetic 'or' of its arguments. p r i m i t i v e valid_sp( sync_point ) than  This primitive returns a boolean value indicating if the given sync_point is greater the last confirmed synchronization number but less than or equal to the -82-  0  synchronization primitive).  number  of  the  last  synchronization  request,  (see  increment_sync  p r i m i t i v e pduXX( arglist... ) These primitives are responsible for constructing and returning. SPDU's f r o m given parameters.  -83-  State  Transitions  The operation of the session protocol is defined in the following state transitions. Each transition is accompanied by comments explaining its e f f e c t s . The transitions are grouped into categories of connection establishment, connection release, abort, data transfer, exception data, capability data, token management, minor major synchronization and a c t i v i t y management.  -84-  synchronization,  ( c l)  < C A L L I N G > <-- < U N C O N N E C T E D > [from U: 5 _ C O N N E C T . r e q u e s t ] ( testSaddr( [from U:Initiator_addr] ) and testSaddr( [from U:Acceptor_addr] ) and size( [from U: User_data] ) <= M A X _ C N _ D A T A _ S I Z E ) begin C N _ r e f := a l l o c _ r e f ; C N _ o r i g i n := T R U E ; sess_id := [from U: Identifier]; qos :=» set_qos( [from U:Qual_of_serv] ); laddr := [from U:Initiator_addr]; faddr : - [from U:Acceptor_addr]; lhost := get_host( laddr ); fhost : - get_Jiost( faddr ); l t c := get_to_addr( laddr ); f t c : - get_tc addr( faddr ); dk_token := [from U:Init_dk_token]; tr_token := [from U:Init_tr_token]; sy_token := [from U:Init_sy_tokenj; ma_token : - [from U:Init_ma_token]; sess_req := [from U:Session_req]; set_sr( sess_req ); sync_serial := [from U:Sync_serial]; user_data := [from U:User_data]; [to T: T _ C O N N E C T . r e q u e s t ( Called_address := f t c , Calling_address := l t c , Exp_data_option := tc_expedited and session_expedited, Qual_of_service := qos )]; end;  } ENABLING CONDITION A S _ C O N N E C T . r e q u e s t event occurs at the User i n t e r f a c e ; this indicates that the user wishes to establish a session connection. The session addresses supplied by the user are valid and the data the user has asked to be transmitted in the S P D U is of acceptable length.  C U R R E N T STATE The session machine is in the unconnected s t a t e .  ACTION The session machine extracts the transport address with which it w i l l attempt to establish a transport connection. The machine saves parameters f r o m the user request for constructing the connect (CN) S P D U later on. The session machine then attempts to establish, a transport connection to a peer transport entity by i n i t i a t i n g a T _ C O N N E C T . r e q u e s t event. -85-  RESULTANT STATE The session machine awaits a T _ C O N N E C T . c o n f i r m event which w i l l c o n f i r m the establishment of the transport connection.  -86-  ( c2 )  } < C A L L E D > <-- < U N C O N N E C T E D  > [from  T_CONNECT.indication]  begin CN_ref:= alloc_ref; l t c := [from T:Called_address]; f t c := [from T:Calling_address]; tc_expedited := tc_expedited and [from T:Exp_data_option]; qos := set_qos( [from T:Qual_of_service] ); [ to T: T_CONNECT.response( Qual_of_service := qos, Responding_address : = l t c , Exp_data_option := tc_expedited )]; end;  {  }  ENABLING CONDITION A T _ C O N N E C T . i n d i c a t i o n event occurs at the Transport i n t e r f a c e ; this indicates an incoming request for a transport connection.  C U R R E N T STATE The session machine is in the unconnected s t a t e .  ACTION The session machine accepts the request for the specified transport connection by i n i t i a t i n g a T _ C O N N E C T . r e s p o n s e event.  RESULTANT  STATE  The session machine awaits the connect request (CN) S P D U .  -87-  ( c3 )  } < UNCONNECTED  > <-- < C A L L I N G > [from T:T  DISCONNECT.indication]  begin [to U : S _ C O N N E C T . c o n f i r m ( Identifier := sess_id, Acceptor_addr .:= faddr, Result := tc_disc_reason( [from TtReason] ), Qual_of_serv := qos, Session_req := sess_req, Sync_serial := sync_serial, User_data : = [from T:User_data] )]; clear_session; end;  } ENABLING CONDITION A T_DISCONNECT.indication event occurs at the Transport i n t e r f a c e ; indicates that establishment of the transport connection is unsuccessful.  this  C U R R E N T STATE The session machine awaits the establishment of a transport connection.  ACTION The session machine initiates a S _ C O N N E C T . c o n f i r m event to inform the user of the failure to establish a connection with the peer transport e n t i t y .  RESULTANT  STATE  The session machine goes to the unconnected s t a t e .  -88-  ( c4 )  } < WAIT_FOR_AC_SPDU  > <~ < C A L L I N G > [from T: T _ C O N N E C T . c o n f i r m ]  begin [to T: T_DATA.request. ( D a t a := pduCN( C N _ r e f , sess_id, VERSION,lhost, fhost, dk_token, tr_token, sy_token, . ma_token, PROTOCOLJDPTIONS, max_SPDU_in, max_SPDU_out, sync_serial, sess_req, user data end;  ))];  ENABLING  CONDITION  A T _ C O N N E C T . c o n f i r m event occurs at the Transport i n t e r f a c e ; this indicates a transport connection has been established.  CURRENT  STATE  The session machine awaits establishment of a Transport connection.  ACTION The session machine constructs and sends a connect (CN) S P D U . to the session entity to request the establishment of a session connection.  RESULTANT STATE The session machine awaits the arrival of the accept (AC)  -89-  SPDU.  peer  ( c5 ). -  —  }  < U N C O N N E C T E D > <-- < C A L L E D > [from T : T _ D A T A . i n d i c a t i o n ] (( [from T:Spdu.ptype] = C N ) and not ( acceptable_CN( [from T:Spdu] ) )) begin [to T: T_DATA.request( D a t a := pduRF( C N _ r e f , TC_DISCONNECT, VERSION, . , CN_reject_reason( [from TrSpdu] ), [from T:Spdu.psess req], [from T:Spdu.pdata] ))];  clear_session; end;  {  }  ENABLING CONDITION A T _ D A T A . i n d i c a t i o n event occurs at the Transport i n t e r f a c e ; this indicates the arrival of a connect (CN) S P D U f r o m the peer session entity. The connection requested is N O T acceptable to the session machine.  CURRENT  STATE  The session machine may participate in incoming session connection requests.  ACTION The session machine determines the reason for rejecting the connection request and transmits a R F S P D U to signal to the peer session entity that the request has been ..refused.  RESULTANT  STATE  The session machines goes to the unconnected s t a t e .  -90-  ( c6 )  {  }  < W A I T _ F O R _ S _ C O N N E C T _ R E S P > <-- < C A L L E D > [from T: T _ D A T A . i n d i c a t i o n ] ( ([from T:Spdu.ptype] = C N ) and acceptable_CN( [from T:Spdu] ) ) begin C N _ o r i g i n := F A L S E ; sess_id := [from T:Spdu.psess_id}; lhost := [from T:Spdu.pacceptor_addr]; fhost := [from T:Spdu.pinitiator_addr]; laddr := mapSaddr( lhost, l t c ); faddr := mapSaddr( fhost, f t c ); set_tokens( [from T:Spdu.ptoken] ); m a x _ S P D U _ i n := m i n ( M A X _ S P D U _ I N , [ f r o m T:Spdu.pmax_SPDU_in]); max_SPDU_out := m i n ( M A X _ S P D U _ O U T , [ f r o m T:Spdu.pmax_SPDU_out]); protocol_opts := intersect( [from T:Spdu.p_options], P R O T O C O L _ O P T I O N S ); [to U : S _ C O N N E C T . i n d i c a t i o n ( Identifier := sess_id, Initiator_addr := faddr, Acceptor_addr := laddr, Qual_of_serv : - qos, Session_req := [from T:Spdu.psess_req], . S y n c _ s e r i a l := [from T:Spdu.psync_serial],Init_dk_token := dk_token, Init_tr_token := .tr_token, Init_sy_token := sy_token, Init_ma_token := ma_token, User_data [from T:Spdu.pdata] )]; end; {  _  _  _  _  }  ENABLING CONDITION An T _ D A T A . i n d i c a t i o n event occurs at the Transport i n t e r f a c e ; this indicates the arrival of a connect request (CN) S P D U f r o m the peer session e n t i t y . The connection requested is acceptable to the session machine. CURRENT  STATE  The session machine may participate in incoming connection requests. ACTION The session machine saves the information contained in the C N S P D U , and initiates a S _ C O N N E C T . i n d i c a t i o n event to inform the user of the arrived request. RESULTANT The  STATE  session  machine  waits  for the user  -91-  to accept  or reject  the requested  connection.  -92-  ( c7 )  •  --}  < U N C O N N E C T E D > <-- < W A I T _ F O R _ S _ C O N N E C T _ R E S P > [from U : S _ C O N N E C T . r e s p o n s e ] not ( [from U : R e s u l t ] = A F F I R M A T I V E ) . ' ' " begin [to T: T _ D A T A . r e q u e s t ( D a t a := pduRF( C N _ r e f , TC_DISCONNECT, VERSION, [from U : R e s u l t ] , [from U:Session_req], [from U:User_data] ))]; clear_session; end;  {  }  ENABLING CONDITION A S _ C O N N E C T . r e s p o n s e event occurs at the User i n t e r f a c e ; the user has rejected the connection request.  C U R R E N T STATE The session machine is waiting for the user to accept or reject the requested connection.  ACTION The session machine sends indicating the user's decision.  a  refuse  (RF)  SPDU  RESULTANT STATE The session machine is in the unconnected s t a t e .  -93-  to  the  peer  session  entity  ( c8 )  {  }  < IDLE > < -  < WAIT_FOR_S_CONNECT_RESP > [from U : S C O N N E C T . r e s p o n s e ] ( ([from U:ResultI= A F F I R M A T I V E ) and (size([from U:User_data]) <= M A X _ A C _ D A T A _ S I Z E ) ) begin laddr := [from U : A c c e p t o r _ a d d r ] ; lhost := get_host( laddr ); sync_serial := [from U:Sync_serial]; qos := set_qos( [from U:Qual_of_serv] ); sess_req := [from U:5ession_req]; intersect_sr( sess_req );  if( if( . if( if(  dk_token = C H O I C E - ) dk_token := [from U:Init_dk_token]; tr_token = C H O I C E ) tr_token := [from U:Init_tr_token]; sy_token = C H O I C E ) sy_token := [from U:Init_sy_token]; ma_token = C H O I C E ) ma_token := [from U:Init_ma_token];  [to T: T_DATA.requ.est ( D a t a := pduAC( C N _ r e f , sess_id, VERSION, lhost, fhost, dk_token, tr_token, sy_token, ma_token, protocol_opts, max_SPDU_in, max_SPDU_out, sync_serial, sess_req, [from U:User_data] ))]; end; {_  ENABLING  }  CONDITION  A S _ C O N N E C T . r e s p o n s e event occurs at the User i n t e r f a c e ; the user has accepted the session connection request. The data to be sent to the peer session entity is of acceptable s i z e . CURRENT  STATE  The session machine is waiting for the user to accept or reject the requested connection. ACTION  -94-  The session machine adjusts the connection parameters according to the user response. The session requirements for the connection are those s p e c i f i e d in both the C N and A C S P D U s . If the user was given the choice for i n i t i a l placement of the tokens, the new values of the tokens are set. An accept (AC) S P D U is.constructed and sent to the peer session entity.  RESULTANT STATE The session machine is in the idle (data transfer) s t a t e .  -95-  ( c9 )  { < U N C O N N E C T E D > <-- < W A I T _ F O R _ A C _ S P D U > [from T : T _ D A T A . i n d i c a t i o n ] ([from T:Spdu.ptype] = R F ) begin [to U : S _ C O N N E C T . c o n f i r m ( Identifier := sess_id, A c c e p t o r addr := laddr, Result :=~Lfrom TrSpdu.presult], Qual_of_serv := qos, Session_req := [from T:Spdu.psess_req], Sync_serial := s y n c _ s e r i a l , User_data := [from T:Spdu.pdata] )]; . [to T:  T_DISCONNECT.request];  clearsession; end;  {. ENABLING  CONDITION  A T _ D A T A . i n d i c a t i o n event occurs at the Transport i n t e r f a c e ; this indicates the arrival of a connection refuse (RF) S P D U f r o m the peer session entity: the connection request was r e j e c t e d . CURRENT  STATE  The session machine awaits arrival of a connection accept (AC) S P D U . ACTION The session machine initiates a S _ C O N N E C T . c o n f i r m event to notify the user that the connection request was refused by the peer session e n t i t y . The session machine also issues a T _ D I S C O N N E C T . r e q u e s t at the transport interface to terminate the transport connection. RESULTANT  STATE  The session machine goes to the unconnected s t a t e .  -96-  ( clO )  < W A I T _ F O R _ A A _ S P D U > <-- < W A I T _ F O R _ A C _ S P D U [from T : T _ D A T A . i n d i c a t i o n ] (([from T:Spdu.ptype] = A C ) and not a c c e p t a b l e _ A C ( [from T:Spdu] ))  >  begin set_tokens( [from T:Spdu.ptoken] ); result := AC_reject_reason( [from T:Spdu] ); [to U : S _ C O N N E C T . c o n f i r m ( Identifier := sess._id, Acceptor_addr := laddr, Result := result, Qual_of_serv :=. [from TrSpdu.pqos], Session_req : = [from T:Spdu.psess_req], Sync_serial := [from T:Spdu.pinit_mark], Init_dk_token := dk_token, Init_tr_token := t r _ t o k e n , Init_sy_token := sy_token, Init_ma_token := ma_token, User_data := [from TtSpdu.pdata] )]; [to T: T_DATA.request( D a t a := p d u C K A B , CN_ref, . , union( T C _ D I S C O N N E C T , P R O T _ E R R O R ), NULL ))];  [to S: Timer.request( Name := T A B , Time := T A B I N T E R V A L )]; end;  ENABLING CONDITION A T _ D A T A . i n d i c a t i o n event occurs at the Transport i n t e r f a c e ; this indicates the arrival of a connection accept (AC) S P D U from the peer session entity: the connection request was a c c e p t e d . However, the negotiated parameters in the A C S P D U is N O T acceptable to the session machine.  CURRENT  STATE  The session machine awaits arrival of a connection accept (AC) S P D U .  ACTION  -97-  The session machine initiates a S _ C O N N E C T . c o n f i r m event to notify the user that the connection negotiation has f a i l e d . The session machine issues an abort (AB) S P D U to abort the connection. The abort timer is started to wait for the A A S P D U to arrive. RESULTANT  STATE  The session machine waits for the a r r i v a l of an abort accept (AA) S P D U .  -98-  ( ell )  {  }  < IDLE > < -  < WAIT_FOR_AC_SPDU > [from T : T _ D A T A . i n d i c a t i o n ] (( [from T:Spdu.ptype] = A C ) and a c c e p t a b l e _ A C ( [from T:Spdu] ))  begin set_tokens( [from T:Spdu.ptoken] ); m a x _ S P D U _ i n := [from T:Spdu.pmax_SPDU_in]; max_SPDU_out := [from T:Spdu.pmax_SPDU_out]; sync_serial : = [from T:Spdu.psync_serial]; qos := [from TtSpdu.pqos]; protocol_opts := [from T:Spdu.p_options]; sess_req := [from T:Spdu.psess_req]; intersect_sr( sess_req ); lhost := [from T:Spdu.pacceptor_addr]; laddr := mapSaddr( lhost, l t c ); [to U: S _ C O N N E C T . c o n f i r m ( Identifier := sess_id, Acceptor_addr := laddr, Result := A F F I R M A T I V E , Qual_of_serv := qos, Session_req := sess_req, Sync_serial := s y n c _ s e r i a l , Init_dk_token := dk_token, Init_tr_token := t^r_tbken, Init_sy_token := sy_token, Init_ma_token := ma_token, User_data := [from TrSpdu.pdata] )]; end;  ENABLING CONDITION A T _ D A T A . i n d i c a t i o n event occurs at the Transport i n t e r f a c e ; this indicates the arrival of a connection accept (AC) S P D U f r o m the peer session entity: the connection request was accepted. The A C S P D U parameters are acceptable to the session machine.  CURRENT  STATE  The session machine awaits the a r r i v a l of an accept ( A C ) S P D U .  ACTION The session machine saves the negotiated parameters given by the A C S P D U and initiates an S _ C O N N E C T . c o n f i r m event to notify the user of the establishment of the connection with the peer session e n t i t y . The functional units available for the -99-  connection are the intersection of the functional units specif ed in the C N and A C S P D U session requirements. RESULTANT  STATE  The session machine is in the connected state (ready to transfer data with its peer session entity).  -100-  ( rl )  { < W A I T _ F O R _ D N _ S P D U > <-- < I D L E > [from U : S _ R E L E A S E . r e q u e s t ] ( ((dk_token = N O T _ A V AIL A B L E ) or this_side( dk_token )) and ((tr_token = N O T _ A V A I L A B L E ) or this_side( tr_token )) ) begin [to T: T _ D A T A . r e q u e s t ( D a t a := p d u C l ( F N , CN_ref, TC_DISCONNECT, [from U:User_data]  ))3;  end;  {. ENABLING CONDITION A S _ R E L E A 5 E . r e q u e s t event occurs at the User i n t e r f a c e ; this indicates that the user wishes to terminate the session connection. Either the data token is not available or the data token is on this side. Similarly with the release token.  CURRENT  STATE  The session machine is in the idle state (ready for data transfer).  ACTION The session machine constructs and sends a finish (FN) entity.  RESULTANT  S P D U to its peer session  STATE  The session machine awaits termination of the connection.  arrival  of  -101-  a disconnect  (DN)  SPDU  to  confirm  ( r2 ) _-___}  < W A I T _ F O R S _ R E L E A S E _ R E S P > <-- < I D L E >  Tfrom T: T_DATA.indication] ( ([from T:Spdu.ptype] = FN") and  ((dk_token  = NOT_AVAILABLE)  other_side( dk_token )) and  begin  or  ((tr_tok.en = N O T _ A V A I L A B L E ) or other side( tr_token )) )  [to U: S_RELEASE.indication( User_data : - [from T:Spdu.pdata] )];  end; {_  }  ENABLING CONDITION A T _ D A T A . i n d i c a t i o n event occurs at the Transport i n t e r f a c e ; this indicates the arrival of a finish. (FN) S P D U f r o m the peer session entity. The data token is either not available or is on the peer session entity side. Similarly w i t h the release token.  C U R R E N T STATE The session machine is in the idle state (ready for data transfer).  ACTION The session machine initiates an S _ R E L E A S E . i n d i c a t i o n event to notify the user of the arrival of the finish S P D U .  RESULTANT  STATE  The session machine waits for a response from the user to accept or reject the disconnect request. The user may only reject the disconnect request if the release token is available.  -102-  ( r3 )  {  }  < W A I T _ F O R _ S _ R E L E A S E _ R E S P > <-- < W A I T _ F O R _ D N _ S P D U [from T : T _ D A T A . i n d i c a t i o n ] ( ([from T:Spdu.ptype] = F N ) and (tr_token = N O T _ A V A I L A B L E ) )  >  begin [to U: S _ R E L E A S E . i n d i c a t i o n ( User_data := [from T:Spdu.pdata] )]; end;  {  }  ENABLING CONDITION A T _ D A T A . i n d i c a t i o n event occurs at the Transport i n t e r f a c e ; this indicates arrival of a finish (FN) S P D U f r o m the peer session entity. The connection does not have the negotiated release option.  CURRENT  STATE  The session machine awaits termination of the connection.  arrival  of  a disconnect  (DN)  SPDU  to  confirm  ACTION The session machine notifies the session user of the arrival of the F N S P D U by i n i t i a t i n g a S _ R E L E A S E . i n d i c a t i o n event.  RESULTANT  STATE  The session machine awaits response from the user to either accept or reject the termination request.  -103-  ( r4  {  )  }  < W A I T _ F O R _ S _ R E L E A S E _ R E S P > <-- < W A I T _ F O R _ M C D _ S P D U > [ from T: T _ D A T A . i n d i c a t i o n ] ( ([from T:Spdu.ptype] = FN) and ( d k j o k e n = N O T _ A V A I L A B L E ) and (tr_token = N O T _ A V A I L A B L E ) ) begin [to U: S _ R E L E A S E . i n d i c a t i o n ( User_data := [from TrSpdu.pdata] )]; end;  {  ,  }  ENABLING CONDITION A T _ D A T A . i n d i c a t i o n event occurs at the Transport i n t e r f a c e ; this indicates the arrival of a finish (FN) S P D U f r o m the peer session entity. Neither the data token nor the release token is available.  CURRENT  STATE  The session machine awaits the arrival of a major mark confirmation or a c t i v i t y end acknowledgement (MCD) S P D U .  ACTION The session machine initiates an S _ R E L E A S E . i n d i c a t i o n event to notify the user of the arrival of the F N S P D U .  RESULTANT  STATE  The session machine waits for the user to respond to the disconnect request.  ( r5 )  } < IDLE > < - < WAIT_FOR_S_RELEASE_RESP > [from U: S_RELEASE.response] ( not ([from UrResult] = A F F I R M A T I V E ) and not (tr_token = N O T _ A V A I L A B L E ) ) begin [to T: T_DATA.request( D a t a := pduCl( N F , CN_ref, NULL,^ [from LhUser data] ))]; end;  {  }  ENABLING CONDITION A S _ R E L E A S E . r e s p o n s e event occurs at the User i n t e r f a c e ; this indicates that the user has rejected the disconnect request.. The connection has the negotiated release option.  CURRENT  STATE  The session machine is waiting for the user to accept or reject the disconnect request.  ACTION The session machine constructs session entity.  RESULTANT  and sends a not finish (NF)  STATE  The session machine goes back to the idle s t a t e .  -105-  S P D U . to the  peer  ( r6 )  {  }  < UNCONNECTED > <- < WAIT_FOR_S_RELEASE_RESP > [from U : S _ R E L E A S E . r e s p o n s e ] ([from UrResult] = A F F I R M A T I V E ) begin [to T : T _ D A T A . r e q u e s t ( Data : = pduCK D N , CN_ref, NULL, [from U:User_data] ))]; clear_session; end;  {  }  ENABLING CONDITION A S _ R E L E A S E . r e s p o n s e event occurs at the User i n t e r f a c e ; this indicates that the user has accepted the disconnect request.  CURRENT  STATE  The session machine disconnect request.  is  waiting for  the  user  to  either  accept  or  reject  the  ACTION The session machine constructs and sends a disconnect confirmation (DN) S P D U to the peer session entity.  RESULTANT  STATE  The session machine goes into the unconnected s t a t e .  -106-  ( r7 )  } < same_state> <-- < W A I T _ F O R _ S _ R E L E A S E _ R E S P [from T : T _ D A T A . i n d i c a t i o n ] ( ([from T:Spdu.ptype] = D N ) and (tr_token = N O T _ A V A I L A B L E ) )  >  begin [to U: S _ R E L E A S E . c o n f i r m ( Result := A F F I R M A T I V E , User_data := [from T:Spdu.pdata] )]; end;  {  }  ENABLING CONDITION A T _ D A T A . i n d i c a t i o n event occurs at the Transport i n t e r f a c e ; this indicates arrival of a disconnect confirmation (DN) S P D U . The connection does not have negotiated release.  CURRENT  STATE  The session machine is waiting for the user to either accept or reject a disconnect request f r o m the peer session entity.  ACTION The session machine notifies the session user of the arrival of the D N S P D U by i n i t i a t i n g a S _ R E L E A S E . c o n f i r m event.  RESULTANT  STATE  The session machine remains in the same s t a t e .  -107-  ( r8 )  {  }  < U N C O N N E C T E D > < - < WAIT_FOR_DN_SPDU [from T : T _ D A T A . i n d i c a t i o n ] ([from T:Spdu.ptype] = D N )  >  begin [to U: S _ R E L E A S E . c o n f i rm( Result := A F F I R M A T I V E , User_data : - [from TrSpdu.pdata] )]; [to T: T J D I S C O N N E C T . r e q u e s t ] ; clear_session; end; {_  }  ENABLING CONDITION A T _ D A T A . i n d i c a t i o n event occurs on the Transport i n t e r f a c e ; this indicates the arrival of a disconnect (DN) S P D U : the peer session entity has accepted the disconnect request.  CURRENT  STATE  The session machine is waiting for the arrival of the D N S P D U .  ACTION The session machine initiates a S _ R E L E A S E . c o n f i r m event to inform the user of successful termination of the connection. The transport connection is released by a T _ D I S C O N N E C T . r e q u e s t event.  RESULTANT  STATE  The session machine is in the unconnected s t a t e .  -108-  ( r9 )  {  }  < I D L E > < - < W A I T _ F O R _ D N _ S P D U > [from ( ([from T:Spdu.ptype] = N F ) and not (tr_token = N O T _ A V AIL A B L E ) )  T:T_DATA.indication]  begin [to U: S _ R E L E A S E . c o n f i r m ( Result := U S E R _ R E J E C T , . . User_data := [from T:Spdu.pdata] )]; end;  }  {. ENABLING CONDITION  A T _ D A T A . i n d i c a t i o n event occurs at the Transport i n t e r f a c e ; this indicates the arrival of a not finish (NF) S P D U f r o m the peer session entity rejecting the disconnect request. The release token must be available (the connection has the negotiated release option).  CURRENT  STATE  The session machine awaits termination of the connection.  arrival  of  a disconnect  (DN)  SPDU  to  confirm  ACTION The session machine notifies the user of the peer session entity's refusal of the disconnect request by i n i t i a t i n g a S _ R E L E A S E . c o n f i r m event.  RESULTANT  STATE  The session machine goes back to the idle s t a t e .  -109-  ( abl ) __}  {  < W A I T _ F O R _ A A _ S P D U > <-- < abort_allowed > [from U: S _ U _ A B O R T . r e q u e s t ] begin [to T: T_DATAorequest( D a t a := p d u C K A B , CN_ref, union( T C _ D I S C O N N E C T , U S E R _ A B O R T ), [from U:User data]  »]; [to S: Timer.requestC Name := T A B , Time := T A B J N T E R V A L )]; end;  {  }  ENABLING CONDITION A S_U_ABORT.request occurs at the User i n t e r f a c e ; this indicates that the user wishes to abort the connection.  C U R R E N T STATE The session machine is at an abortable s t a t e .  ACTION The session machine constructs and sends an abort (AB) S P D U to the peer session entity. The session machine also issues a request to the system to start an abort timer.  RESULTANT  STATE  The session machine awaits arrival of an abort accept (AA) S P D U .  -110-  ( ab2 ) {.  }  < UNCONNECTED  >  < abort_allowed > [from T:  T_DATA.indication]  ( [from T:Spdu.ptype] = A B ) begin if (arith_and( [from T:Spdu.pmisc], U S E R _ A B O R T )) then [to U : S _ U _ A B O R T . i n d i c a t i o n ( User_data := [from T:Spdu.pdata] )] else begin if (arith_and( [from T:Spdu.pmisc], P R O T _ E R R O R )) then reason := P R O T O C O L _ E R R O R else reason : = N O _ S P E C I F I C _ R E A S O N ; [to U : S _ P _ A B O R T . i n d i c a t i o n ( Reason := reason )] end; [to T:  T_DISCONNECT.request];  clear_session; end;  {  }  ENABLING CONDITION A T _ D A T A . i n d i c a t i o n event occurs at the Transport i n t e r f a c e ; this indicates the arrival of an abort (AB) S P D U .  CURRENT  STATE  The session machine is in an abortable s t a t e .  ACTION The session machine notifies the user of the aborted state by i n i t i a t i n g a S _ U _ A B O R T . i n d i c a t i o n or S _ P _ A B O R T . i n d i c a t i o n event depending on the reason specified in the A B S P D U . (Since the transport connection is not kept, an A A is not sent). The transport connection is cleared by a T _ D I S C O N N E C T . r e q u e s t event.  RESULTANT  STATE  The session machine goes into the unconnected s t a t e .  -Ill-  ( ab3 )  { < same_state > < - < W A I T _ F O R _ A A _ S P D U > [from T: T _ D A T A . i n d i c a t i o n ] ( [from T:Spdu.ptype] = A B ) begin end;  {ENABLING CONDITION A T _ D A T A . i n d i c a t i o n event arrival of an abort (AB) S P D U .  occurs  at  the  Transport  i n t e r f a c e ; this  indicates  C U R R E N T STATE The session machine awaits arrival of an abort accept (AA) S P D U from the peer session entity.  ACTION No action is t a k e n .  RESULTANT  STATE  The session machine remains in the same s t a t e .  -112-  ( ab4 )  {  }  < U N C O N N E C T E D > <-- < W A I T _ F O R _ A A _ S P D U ( [from T:Spdu.ptype] = A A )  > [from T:  T_DATA.indication]  begin [to T: T _ D I S C O N N E C T . r e q u e s t ] ; [to S: Timer.cancel( Name := T A B )]; clear_session; end;  {_  }  ENABLING CONDITION A T _ D A T A . i n d i c a t i o n event occurs at the Transport i n t e r f a c e ; this indicates the arrival of an abort accept (AA) S P D U f r o m the peer session entity.  CURRENT  STATE  The session machine awaits arrival of an A A S P D U to confirm abortion of the connection.  ACTION The session machine initiates a T _ D I S C O N N E C T . r e q u e s t event to release the transport connection. It also stops the abort timer by issuing a T i m e r . c a n c e l request to the s y s t e m .  RESULTANT  STATE  The session machine goes into the unconnected s t a t e .  -113-  ( ab-5 )  {  }  < UNCONNECTED > <- < WAIT_FOR_AA_SPDU > [from S: Timer.response] ( [from S:Name] = T A B ) begin [to T:  T_DISCONNECT.request];  clear_session; end; {  _}  ENABLING CONDITION A Timer.response event occurs at the System i n t e r f a c e ; this indicates that the abort timer has timed out.  C U R R E N T STATE The session machine awaits arrival of an abort accept ( A A ) S P D U from the peer session entity.  ACTION The session machine proceeds T _ D I S C O N N E C T . r e q u e s t event.  RESULTANT  to  terminate  the  STATE  The session machine goes into the unconnected s t a t e .  -114-  connection  by  initiating  a  ( ab6 )  { < UNCONNECTED [from T:  > <- < WAIT_FOR_AA_SPDU > TjDISCONNECT.indication]  begin [to S: Timer .cancel( Name := T A B )]; clear_session; end;  { ENABLING CONDITION A T_DISCONNECT.indication event occurs at the Transport i n t e r f a c e ; indicates that the peer transport entity wishes to terminate the connection.  this  C U R R E N T STATE The session machine awaits arrival of an abort accept (AA) S P D U from the peer session entity.  ACTION The session connection.  RESULTANT  machine  stops  the  abort  timer  (Timer .cancel)  STATE  The session machines goes to the unconnected s t a t e .  -115-  and  clears  the  ( ab7 )  {  }  < UNCONNECTED  > <-- < pabort_allowed > [from T: T _ D I S C O N N E C T . i n d i c a t i o n ]  begin [to U : S _ P _ A B O R T . i n d i c a t i o n ( Reason := T C _ G O N E clear_session; end;  )];  }  {ENABLING  CONDITION  A T_DISCONNECT.indication event occurs at the Transport indicates that the transport connection is no longer available. CURRENT  interface;  this  STATE  The session machine is U N C O N N E C T E D , C A L L I N G or  in a provider abortable WAIT_FOR_AA_SPDU).  state  (any  state  except  ACTION The session machine notifies the user of the loss of connection by i n i t i a t i n g a S _ P _ A B O R T . i n d i c a t i o n event. RESULTANT  STATE  The session machine goes into the unconnected s t a t e .  -116-  (dl)  .< same_state > <-- < I D L E > [ from U: S_DATA.request ( ((activity = N O T _ A V A I L A B L E ) or (activity = ON)) and ((dk_token = N O T _ A V A I L A B L E ) or this side( dk token )) )  ]  begin [to T: T _ D A T A . r e q u e s t ( D a t a := pduDT( D T , CN_ref, [from U : D a t a ] ))]; end;  {ENABLING CONDITION A S_DATA.request event occurs at the. User i n t e r f a c e ; this indicates the user wishes to send data to the peer session entity. Either there is no a c t i v i t y management or there is an a c t i v i t y in progress. A l s o , either the data token is not available or the data token is on this side.  CURRENT  STATE  The session machine is in the idle s t a t e .  ACTION The session machine constructs and sends a data (DT) entity.  RESULTANT  STATE  The session machine remains in the same s t a t e .  -117-  S P D U to the peer session  ( d2 )  } < same_state > <-- < W A I T _ F O R _ S _ M C D _ R E S P [ from U: S p A T A . r e q u e s t ] (dk_token = N O T _ A V AIL A B L E ) .  >  begin [to T: T _ D A T A . r e q u e s t ( D a t a := pduDT( DT, CN_ref, [from U : D a t a ] ))]; end;  {  }  ENABLING  CONDITION  A S_DATA.request event occurs at the User i n t e r f a c e ; this indicates the wishes to send data to the peer session entity. The data token is not available.  CURRENT  user  STATE  The session machine is waiting for the user to respond to a a c t i v i t y end indication or a major mark indication.  ACTION The session machine constructs entity.  and sends a data (DT)  RESULTANT STATE The session machine remains in the same s t a t e .  -118-  S P D U to the peer session  ( d3 )  {  }  < W A I T _ F O R _ r e c o v e r „ y _ S P D U > <-- < W A I T _ F O R _ S _ M C D _ R E S P > [ f r o m T: T _ D A T A . i n d i c a t i o n ] ( ([from T:Spdu.ptype] = DT) and (dk_token = N O T _ A V A I L A B L E ) ) begin [to U: S _ P _ E X C E P T I O N _ R E P O R T . i n d i c a t i o n ( Reason := P R O T O C O L _ E R R O R ; )];  [to T: T_DATA.request( D a t a := pduDT( E R , CN_ref, [from T:.Spdu] ))]; end;  {  }  ENABLING CONDITION A T _ D A T A . i n d i c a t i o n event occurs at the Transport i n t e r f a c e ; this indicates the arrival of a data (DT) S P D U . The data token is not available.  C U R R E N T STATE The session machine is waiting for the user to respond to a a c t i v i t y end indication or a major mark i n d i c a t i o n .  ACTION A S _ P _ E X C E P T I O N _ R E P O R T . i n d i c a t i o n event is i n i t i a t e d to inform the user of a protocol error. The session machine constructs and sends a exception report (ER) . S P D U to the peer session e n t i t y .  RESULTANT  STATE  The session machine awaits arrival of a 'recovery' S P D U (it is in an error state).  i  -119-  ( d4 )  } < same_state > <~ < WAIT_FOR_recover,y_SPDU > [ f r o m T: T _ D A T A . i n d i c a t i o n ] ( ([from T:Spdu.ptype] = DT) and . . not (dk_token = N O T _ A V A I L A B L E ) ) begin end; {_  }  ENABLING  CONDITION  A T _ D A T A . i n d i c a t i o n event occurs at the Transport i n t e r f a c e ; this indicates the arrival of a data (DT) SPDU= The data token is available.  CURRENT  STATE  The session machine is awaiting a r r i v a l of a 'recovery' S P D U (it is in the error state).  ACTION No action is taken (the incoming data is ignored).  RESULTANT STATE The session machine remains in the same s t a t e .  -120-  ( d5 )  {  }  < same_state > <-- < I D L E > [ f r o m T: T _ D A T A . i n d i c a t i o r i ] ( ([from T.:Spdu.ptype] = DT) and ((activity = NO T_A V A I L A B L E ) or (activity = ON)) and ((dk_token = NO T_A V A I L A B L E ) or other_side( dk_token )) ) begin [to U: S D A T A . i n d i c a t i o n ( D a t a := [from T:Spdu.pdata] )]; end;  {  }  ENABLING CONDITION A T _ D A T A . i n d i c a t i o n event occurs at the Transport i n t e r f a c e ; this indicates the arrival of a data (DT) S P D U . Either there is no a c t i v i t y management or there is an a c t i v i t y in progress. A l s o , either the data token is not available or the data token is not on this side.  C U R R E N T STATE The session machine is in the idle s t a t e .  ACTION The session machine notifies the user of the a r r i v a l of the data.  RESULTANT  STATE  The session machine remains in the same s t a t e .  -121-  ( d6 )  < same_state > <-- < W A I T _ F O R _ D N _ S P D U [ from T: T_DATA.indication ]  >  ( ([from T:Spdu.ptype] = DT) and  ((activity = N O T _ A V A I L A B L E ) or (activity = ON)) and ((dk_token = N O T _ A V A I L A B L E ) or (othersideC dk_token ) and (tr token = N O T A V A I L A B L E ) ) ) )  begin [to U: S D A T A . i n d i c a t i o n ( D a t a := [from T.:Spdu.pdata] )]; end;  {ENABLING CONDITION A T _ D A T A . i n d i c a t i o n event occurs at the Transport i n t e r f a c e ; this indicates the arrival of a data (DT) S P D U . Either there is no a c t i v i t y management or there is an a c t i v i t y in progress. A l s o , either the data token is not available or the data token is not on this side and the release token is not available.  CURRENT The SPDU.  STATE  session machine awaits the arrival of a disconnect acknowledgement  ACTION The session machine notifies the user of the arrival of the data.  RESULTANT  STATE  The session machine remains in the same s t a t e .  -122-  (DN)  ( d7 )  } < same_state > < - < W A I T _ F O R _ M C D _ S P D U [ f r o m T: T _ D A T A . i n d i c a t i o n ] ( ([from TrSpdu.ptype] = DT) and (dk_token = N O T _ A V A I L A B L E ) )  >  begin [to U: S_DATA.indication( D a t a : - [from T:Spdu.pdata] )]; end;  }  {. ENABLING CONDITION  A T_DATA.indication event occurs at the Transport i n t e r f a c e ; arrival of a data (DT) S P D U . The data token is not available.  CURRENT  STATE  The session machine is waiting for the a r r i v a l of a M C D S P D U .  ACTION The session machine notifies the user of the arrival of the d a t a .  RESULTANT STATE The session machine remains in the same s t a t e .  -123-  this  indicates  ( el ) _______  }  < same_state >. <-- < I D L E > [ f r o m U: S _ T Y P E D _ D A T A . r e q u e s t ((activity = N O T _ A V A I L A B L E ) or (activity = ON))  ]  begin [to T: T_DATA.request( D a t a := pduC2s( E D , CN_ref, NULL, TYPED_DATA, [from U:User_data] ))]; end;  {  }  ENABLING CONDITION A S _ T Y P E D _ D A T A . r e q u e s t event occurs at the User i n t e r f a c e ; this indicates that the user wishes to send 'typed' data — not constrained by the presence of the data token. Either there is no a c t i v i t y management or there is an a c t i v i t y in progress.  CURRENT  STATE  The session machine is in the idle s t a t e .  ACTION The session machine constructs and sends an exception data (ED) S P D U w i t h no reason parameter.  RESULTANT  STATE  The session machine remains in the same s t a t e .  -124-  ( e2 )  } < same_state > <~ < I D L E _ o r _ M C D > [ from T: T _ D A T A . i n d i c a t i o n ] ( ([from TrSpdu.ptype] = ED) and [from T:Spdu.pno_reason_field] and ((activity = N O T _ A V A I L A B L E ) or (activity = ON)) )  ENABLING CONDITION A T _ D A T A . i n d i c a t i o n event occurs at the Transport i n t e r f a c e ; this indicates the arrival of a typed data (ED) S P D U (it has no reason parameter). There is either no a c t i v i t y management or there is an a c t i v i t y in progress.  CURRENT  STATE  The session machine is in the idle state or awaiting synchronization/activity end acknowledgement (MCD) S P D U .  arrival  ACTION The session machine notifies the user of the arrival of the typed data.  RESULTANT  STATE  The session machine remains in the same s t a t e .  -125-  of  a  major  ( e3 )  } < same_state > <~ < W A I T _ F O R _ D N _ S P D U > [ f r o m T: T _ D A T A . i n d i c a t i o n ] ( ([from T:Spdu.ptype] = ED) and [from T:Spdu.pno_reason_field] and ((activity = ON) or (activity = N O T _ A V A I L A B L E ) ) and (dk_token = NO T_A V A I L A B L E ) ) begin [to U: S _ T Y P E D _ D A T A . i n d i c a t i o n ( User data := [from T:Spdu.pdata] end; {_  }  ENABLING CONDITION A T _ D A T A . i n d i c a t i o n event occurs at the Transport i n t e r f a c e ; this indicates the arrival of a typed data (ED) S P D U (it has no reason parameter). The data token is not available.  CURRENT  STATE  The session machine is waiting for a disconnect acknowledgement (DN) S P D U .  ACTION The session machine notifies the user of the arrival of the typed data.  RESULTANT  STATE  The session machine remains in the same s t a t e .  -126-  ( e4 )  {  }  < same_state > < - < W A I T _ F O R _ D N _ S P D U > [ f r o m T: X _ D A T A . i i n d i c a t i o n ] ( ([from TrSpdu.ptype] = ED) and ((activity = ON) or (activity = N O T _ A V A I L A B L E ) ) and not (dk_token = N O T _ A V A I L A B L E ) and (tr_token = N O T _ A V AIL A B L E ) ) begin if ( [from T:Spdu.pno_reason_field] ) then . . [to U: S _ T Y P E D _ D A T A . i n d i c a t i o n ( User_data := [from TrSpdu.pdata] )] else [to U: S_U_EXCEPTION_REPORT.indication( Reason := [from TrSpdu.preason], User_data := [from TrSpdu.pdata] )]; end; {_  }  ENABLING CONDITION A T _ D A T A . i n d i c a t i o n event occurs at the Transport i n t e r f a c e ; this indicates the arrival of a E D S P D U - The data token is available. The release token is not available.  CURRENT  STATE o  The session machine is waiting for the a r r i v a l of a disconnect (DN) S P D U .  ACTION The session machine notifies the user of the arrival of the S P D U . If there is a reason on the S P D U , ' t h e n it is exception data otherwise it is typed data.  RESULTANT  STATE  The session machine remains in the same s t a t e .  -127-  ( e5 )  {  }  < W A I T _ F O R _ r e c o v e r y _ S P D U > <-- < I D L E > [ from U: S_U_EXCEPTION_REPORT.request ( ((activity = N O T _ A V AIL A B L E ) or (activity = ON)) and other_side( dk_token ) ) begin [to T: T _ D A T A ; r e q u e s t ( D a t a := pduC2s( E D , CN_ref, NULL, [from U:Reason], [from U:User_data]  ]  ))3; end;  }  {. ENABLING CONDITION  A S_U_EXCEPTION_REPORT.request event occurs at the User i n t e r f a c e ; this indicates the user wishes to signal a user exception to the peer session e n t i t y . Either there is no a c t i v i t y management or there is an a c t i v i t y in progress. The data token is on the other side.  C U R R E N T STATE The session machine is in the idle s t a t e .  ACTION The session machine constructs and sends an exception data (ED) reason parameter as s p e c i f i e d on the user request.  RESULTANT  SPDU  with  STATE  The session machine goes into an error s t a t e ; it awaits arrival of a recovery. S P D U f r o m the peer session entity.  -128-  ( e6 )  -  -}  < same_state > <— < I D L E _ o r _ M C D > [ f r o m T: T _ D A T A . i n d i c a t i o n ] ( ([from TrSpdu.ptype] = ED) and ( ((activity = N O T _ A V A I L A B L E ) or (activity = ON)) and not [from TrSpdu.pno reason_field] and other side( dk token") ) begin [to Ur S_U E X C E P T I O N _ R E P O R T . i n d i c a t i o n ( Reason r= [from TrSpdu.preason], User_data r= [from TrSpdu.pdata] )];end;  {ENABLING CONDITION A T _ D A T A . i n d i c a t i o n event occurs at the Transport i n t e r f a c e ; this indicates the arrival of a exception report (ED) S P D U (it contains a reason parameter). Either there is no a c t i v i t y management or there is an a c t i v i t y in progress. A l s o , the data token is on the other side.  CURRENT  STATE  The session machine is in the idle state or is awaiting synchronization/activity end acknowledgement (MCD) S P D U .  arrival  of  ACTION The session machine notifies the user of the arrival of the exception report.  RESULTANT  STATE  The session machine remains in the same s t a t e .  -129-  major  ( el )  {  }  < WAIT_FOR_recovery_REQ > < - < IDLE or_MCD > [ f r o m T: T J D A T A . i n d i c a t i o n J ( ([from T:Spdu.ptype] = ED) and ((activity = N O T _ A V A I L A B L E ) or (activity = ON)) and not [from T.:Spdu.pno reason_field] and this_side( dk_token )7 begin [to U: S _ U _ E X C E P T I O N _ R E P O R T . i n d i c a t i o n ( Reason := [from TrSpdu.preason], User_data := [from T:Spdu.pdata] )];  end;  {  }  ENABLING CONDITION A T _ D A T A . i n d i c a t i o n event occurs at the Transport i n t e r f a c e ; this indicates the arrival of a exception report (ED) S P D U (it contains a reason parameter). Either there is no a c t i v i t y management or there is an a c t i v i t y in progress. The data token is on the this side.  CURRENT  STATE  The session machine is in the idle state or synchronization/activity end acknowledgement (MCD) S P D U .  is  awaiting  a  major  ACTION The session machine notifies the user of the arrival of the exception report.  RESULTANT The report.  STATE  session machine awaits  response f r o m  -130-  the  user  concerning the  exception  ( cdl ) < WAIT_FOR_CDA_SPDU > < - < IDLE > [from, U:S C A P A B I L I T Y _ D A T A . r e q u e s t ] ( this_sideT ma_token ) and (this_side( sy_token ). or ( s y j o k e n = N O T _ A V A I L A B L E ) ) and (this_side( dk_token ) or (dk_token = NOT A V A I L A B L E ) ) and (activity = O F F )T begin [to T : T _ D A T A . r e q u e s t ( D a t a := pduDT( C D , CN_ref, [from U:User_data] ))];  end;  {ENABLING CONDITION A S _ C A P A B I L I T Y _ D A T A . r e q u e s t event occurs at the User i n t e r f a c e ; this indicates that the user wishes to send capability data (a l i m i t e d amount of transparent data outside activities) to the peer session entity. The synchronization major/activity token is on this side. The data token (and synchronization minor token) is either not available or is on this side. There is no a c t i v i t y in progress. That is, this session machine has the right to start the next a c t i v i t y .  CURRENT  STATE  The session machine is in the idle s t a t e .  ACTION The session machine constructs and sends a capability data (CD) S P D U to the peer session entity.  RESULTANT STATE The session machine awaits acknowledgement for the capability d a t a .  -131-  ( cd2 )  {  }  < W A I T _ F O R _ C D A _ R E S P X - < I D L E > [from T: ( ([from T:Spdu.ptype] - C D ) and other_side( ma_token ) and (other_side( sy_token ) or (sy_token = NO T_A V A I L A B L E ) ) and (other_side( dk_token ) or (dk_token = NOT A V A I L A B L E ) ) and (activity = O F F )T  T_DATA.indication]  begin [to U : S _ C A P A B I L I T Y _ D A T A . i n d i c a t i o n ( User_data := [from T:Spdu.pdata] )];  end;  {ENABLING CONDITION A T _ D A T A . i n d i c a t i o n event occurs at the Transport i n t e r f a c e ; this indicates the arrival of a capability data (CD) S P D U . The synchronization major/activity token is on the other side. The synchronization minor and data tokens are on the peer entity side or are not available. There is no a c t i v i t y in progress.  C U R R E N T STATE The session machine is in the idle s t a t e .  ACTION The session machine notifies the user of the a r r i v a l of the C D S P D U by i n i t i a t i n g a S _ C A P A B I L I T Y _ D A T A . i n d i c a t i o n event.  RESULTANT  STATE  The session machine awaits response f r o m the user concerning the capability d a t a .  -132-  ( cd3 )  { < I D L E > <-- < W A I T _ F O R _ C D A _ R E S P > [from U:S_CAPABILITY_DATA.response] begin [to T : T _ D A T A . r e q u e s t ( D a t a := pduDT( C D A , CN_ref, [from U:User data]  '  ))1; end;  ENABLING CONDITION A S_CAPABILITY_DATA.response event occurs at the User i n t e r f a c e ; this indicates that the user wishes to acknowledge previously received capability data.  CURRENT  STATE  The session capability data.  machine is  awaiting response  from  the  user  to  acknowledge  the  ACTION The session machine constructs and sends ( C D A ) S P D U to the peer session entity.  RESULTANT  STATE  The session machine goes to the idle s t a t e .  -133-  a capability  data  acknowledgement  ( cd4 )  {  }  < I D L E > <-- < W A I T _ F O R _ C D A _ S P D U > [from T: ([from TrSpdu.ptype] = C D A )  TJDATA.indication]  begin [to U : S _ C A P A B I L I T Y _ D A T A . c o n f i r m ( User data := [from T:Spdu.pdata] )]; end;  {  }  ENABLING CONDITION A. T _ D A T A . i n d i c a t i o n event occurs at the Transport i n t e r f a c e ; this indicates the arrival of a capability data acknowledgement ( C D A ) S P D U .  CURRENT  STATE  The session machine is waiting for the arrival of a C D A S P D U .  ACTION The session machine confirms the user's capability data request S_CAPABILITY_DATA.confirm event.  RESULTANT STATE The session machine goes to the idle s t a t e .  -134-  by i n i t i a t i n g a  (tl)  {  }  < same_state > <— < I D L E _ o r _ G T A _ M C D R > [from U : S _ T O K E N _ P L E A S E , r e q u e s t ] begin [to T : D A T A . r e q u e s t ( D a t a := p d u C K PT,. CN_ref, [from U:Token], [from U:User data] ))]; end;  {......  }  ENABLING CONDITION A S _ T O K E N _ P L E A S E . r e q u e s t event occurs at the User i n t e r f a c e ; this indicates that the user wishes to ask the peer session entity for one (or more) token(s).  C U R R E N T STATE The session machine is in the idle state or expecting a G T A S P D U or. awaiting a response f r o m the user concerning a major synchronization indication or a c t i v i t y end indication.  ACTION The session machine constructs and sends a please token (PT) session entity.  RESULTANT  STATE  The session machine remains in the same s t a t e .  -135-  S P D U to the peer  ( t2 ) { < same_state > < - < I D L E _ o r _ D N _ G T A _ M C D [from T: T _ D A T A . i n d i c a t i o n ] ([from TrSpdu.ptype] = PT)  >  begin [to U : S _ T O K E N _ P L E A S E . i n d i c a t i o n ( Token := [from TrSpdu.ptoken], User_data : - [from TrSpdu.pdata] )]; end; { —  ENABLING CONDITION A T _ D A T A . i n d i c a t i o n event occurs at arrival of a request for token (PT) S P D U .  CURRENT  the  Transport  interface;  this  indicates  STATE  The session machine may accept please token SPDU's (it is in the idle state or expecting a D N , G T A or M C D SPDU).  ACTION The session machine notifies the session user of the (PT) request by i n i t i a t i n g a S _ T O K E N _ P L E A S E . i n d i c a t i o n event.  RESULTANT  STATE  The session machine remains in the same s t a t e .  -136-  ( t3 )  {  }  < same_state > < - < I D L E _ o r _ M C D R > [from U: S_TOKEN_GIVE.request] ( token_this_side( [from UrToken] ) and ((activity = ON) or (activity = N O T _ A V A I L A B L E ) ) ) begin [to T : D A T A . r e q u e s t ( D a t a := p d u C K G T , CN_ref, [from UrToken], NULL ))]; assign_token_give( [from UrToken] ); end;  ENABLING CONDITION A S_TOKEN_GIVE.request event occurs at the User i n t e r f a c e ; this indicates that the user wishes to give one (or more) token(s) to the peer session e n t i t y . The token(s) is on this side and either there is no a c t i v i t y management available or an a c t i v i t y is in progress.  C U R R E N T STATE The session machine is in the idle state or is awaiting response f r o m the user concerning a major synchronize/activity end i n d i c a t i o n .  ACTION The session machine constructs and sends a give token (GT) session entity- The'token(s) is now on the other side.  RESULTANT  STATE  The session machine remains in the same s t a t e .  -137-  S P D U to the peer  ( t4 )  {. < W A I T _ F O R _ G T A _ S P D U > <-- < I D L E > [from U : S_TOKEN_GIVE.request] ( token_this_side( [from U:Token] ) and (activity = O F F ) ).. begin [to T : D A T A . r e q u e s t ( D a t a := p d u C K G T , CN_ref, [from UrToken], NULL ))]; assign_token_give( [from U:Token] ); end;  ENABLING CONDITION A S_TOKEN_GIVE.request event occurs at the User i n t e r f a c e ; this indicates that the user wishes to give one (or more) token(s) to the peer session entity. The token(s) is on this side and there is no a c t i v i t y in progress.  C U R R E N T STATE The session machine is in the idle s t a t e .  ACTION The session machine constructs and sends a give token (GT) session entity. The token(s) is now on the other side.  RESULTANT  S P D U to the peer  STATE.  The session machine awaits arrival of an acknowledgement for the G T S P D U .  -138-  ( t5 )  {  }  < same_state > <~ < I D L E _ o r _ D N _ M C D > [from T: T _ D A T A . i n d i c a t i o n ] ( ([from TrSpdu.ptype] = GT) and token_other_side( [from T:Spdu.ptoken] ) ) begin [to U : S _ T O K E N _ G I V E . i n d i c a t i o n ( Token := [from T:Spdu.ptoken] )]; if ( a c t i v i t y = O F F ) then [to T: T _ D A T A . r e q u e s t ( D a t a := p d u C l ( G T A , CN_ref, N U L L , N U L L ))]; assign_token_accept( [from T:Spdu.ptoken] )]; end;  ENABLING CONDITION A T _ D A T A . i n d i c a t i o n event occurs at the Transport i n t e r f a c e ; this indicates arrival of a give token (GT) S P D U f r o m the peer session entity. The peer session entity has possession of the said token(s).  CURRENT  STATE  The session machine is either in the idle state or is waiting for the arrival of a disconnect (DN) or major synchronize/activity end acknowledgement (MCD) S P D U .  ACTION The session machine notifies the session user of the (GT) S P D U by i n i t i a t i n g a S_TOKEN_GIVE.indication event. If n o » _ a c t i v i t y is in progress, a give token acknowledgement (GTA) S P D U is sent to the peer session e n t i t y . The specified token(s) is now on this side.  RESULTANT  STATE  The session machine remains in the same s t a t e .  -139-  ( t6 )  } < I D L E > <-- < W A I T _ F O R _ G T A _ S P D U > [from T: T _ D A T A . i n d i c a t i o n ] ( [from T:Spdu.ptype] = G T A ) begin end;  {  }  ENABLING CONDITION A T _ D A T A . i n d i c a t i o n event occurs at the Transport i n t e r f a c e ; this indicates the arrival of a give token acknowledgement (GTA) S P D U .  CURRENT  STATE  The session machine is awaiting a r r i v a l of a give token acknowledgement SPDU.  ACTION No action is t a k e n .  RESULTANT  STATE  The session machine goes to the idle s t a t e .  -140-  (GTA)  ( t7 )  {  _  .  _  _  }  < I D L E > <-- < WAIT_FOR_S_reco.very_REQ > [from U : S_TOKENLGIVE.request] ( i s a t o k e n i n ( D K _ T O K E N , [from UrToken]) and token_this_side( [from UrToken] ) ) begin [to TrDATA.request( D a t a r= p d u C K G T , CN_ref, [from UrToken], NULL ))]; assign_token_give( [from UrToken] ); end;  ENABLING CONDITION A S_TOKEN_GIVE.request event occurs at the User i n t e r f a c e ; this indicates that the user wishes to give the data token (and possibly other tokens) to the peer session e n t i t y . The token(s) is on this side.  C U R R E N T STATE The session machine is waiting for a 'recovery' request from the user to exit the error s t a t e .  ACTION The session machine constructs and sends a give token (GT) session entity. The token(s) is now on the other side.  RESULTANT  STATE  The session machine goes to the idle s t a t e .  -141-  S P D U to the peer  ( t8 )  {  }  < I D L E > <-- < W A I T _ F O R _ r e c o v e r y _ S P D U > [from T: T _ D A T A . i n d i c a t i o n ] ( ([from T:Spdu.ptype] = GT) and i s a t o k e n i n ( D K _ T O K E N , [from T:Spdu.ptoken]) and token_other_side( [from T:Spdu.ptoken] ) ) begin [to U : S _ T O K E N _ G I V E . i n d i c a t i o n ( Token := [from T:Spdu.ptoken] )]; assign_token_accept( [from TrSpdu.ptoken] ); end;  {  }  ENABLING CONDITION A T _ D A T A . i n d i c a t i o n event occurs at the Transport i n t e r f a c e ; this indicates arrival of a give token (GT) S P D U f r o m the peer session e n t i t y . One of the token(s) is the data token and the token(s) is not on this side.  C U R R E N T STATE The session machine is awaiting a 'recovery' S P D U to exit the error s t a t e .  ACTION The session machine notifies the session user of the a r r i v a l of the GT S P D U by i n i t i a t i n g a S _ T O K E N _ G I V E . i n d i c a t i o n event. The token(s) is reassigned to this side.  RESULTANT STATE The session machine goes to the idle s t a t e .  -142-  ( syl )  } < same_state > <-- < I D L E > [from U : S _ S Y N C _ M I N O R . r e q u e s t ] ( ((activity = N O T _ A V A I L A B L E ) or (activity = ON)) and this_side( sy_token ) and ((dk_token - N O T _ A V A I L A B L E ) or this_side( dk_token )) ) begin [to T: T_DATA.request( D a t a := pduC2s( M K B , CN_ref, sync_serial, [from U : C o n f i r m ] , [from U:User_data] ))]; increment_sync( sync_serial ); end;  {  }  ENABLING CONDITION A S _ S Y N C _ M I N O R . r e q u e s t event occurs at the user wishes to establish a minor synchronization management or there is an a c t i v i t y in progress. The side., The data token is either not available or is on  User i n t e r f a c e ; this indicates the point. Either there is no a c t i v i t y synchronize minor token is on this this side.  C U R R E N T STATE The session machine is in the idle s t a t e .  ACTION A synchronize-minor (MKB) S P D U is constructed and sent to the peer session e n t i t y . The internal synchronization serial number is i n c r e m e n t e d .  RESULTANT  STATE  The session machine remains in the same s t a t e .  -143-  ( sy2 )  ) < same_state > <— < I D L E > [from T : T _ D A T A . i n d i c a t i o n ] ( ([from T:Spdu.ptype] = M K B ) and ((activity = N O T _ A V A I L A B L E ) or (activity = ON)) and other_side( sy_token ) and ((dk_token = N O T _ A V A I L A B L E ) or other_side( dk_token )) ) begin [to U : S _ S Y N C _ M I N O R . i n d i c a t i o n ( C o n f i r m := [from T: Spdu.pmisc], Sync_point := [from T: Spdu.psync_ serial], User_data := [from T r S p d u . p d a t a ] ) ] ; -  increment_sync( sync_serial ); end;  } ENABLING CONDITION A T _ D A T A . i n d i c a t i o n event occurs at the Transport i n t e r f a c e ; this indicates the peer session entity wishes to establish a minor synchronization point. Either there is no a c t i v i t y management or there is an a c t i v i t y in progress. The synchronize minor token is on the other side. The data token is not available or is on the other side.  C U R R E N T STATE The session machine is the idle s t a t e .  ACTION A synchronize-minor indication is given to the user. The internal synchronization serial number is i n c r e m e n t e d .  RESULTANT  STATE  The session machine remains in the same s t a t e .  -144-  ( sy3 )  { < same_state > <-- < W A I T _ F O R _ D N _ S P D U > [from T : T _ D A T A . i n d i c a t i o n ] ... ( ([from TrSpdu.ptype] = M K B ) and ((activity = N O T _ A V A I L A B L E ) or (activity = ON)) and other_side( sy_^token ) and (dk_token =. N O T _ A V A I L A B L E ) ) begin [to U : S _ S Y N C _ M I N O R . i n d i c a t i o n ( C o n f i r m := [from T : S p d u . p m i s c ] , Sync_point := [from T: Spdu.psync serial], User_data := [from T:, Spdu.pdata] )]; -  increment_sync( sync_serial ); end;  {ENABLING CONDITION A T _ D A T A . i n d i c a t i o n event occurs at the Transport i n t e r f a c e ; this indicates the peer session entity wishes to establish a minor synchronization point. Either there is no a c t i v i t y management or there is an a c t i v i t y in progress. The synchronize minor token is on the other side. The data token is not available.  CURRENT  STATE  The session machine is awaiting arrival of a disconnect (DN) S P D U to complete the termination process.  ACTION A synchronize-minor indication is given to the user. The internal synchronization serial number is incremented.  RESULTANT  STATE  The session machine remains in the same s t a t e .  -145-  ( sy4 )  } < W A I T _ F O R _ A A _ S P D U > <-- < W A I T _ F O R _ S _ M C D _ R E S P > [from T : T _ D A T A . i n d i c a t i o n ] ( (([from T:Spdu.ptype] = M K B ) or ([from TrSpdu.ptype] = MCB)) and not (sy_token = N O T _ A V AIL A B L E ) ) begin [to U: S _ P _ E X C E P T I O N _ R E P O R T . i n d i c a t i o n ( Reason := P R O T O C O L _ E R R O R )]; [to T: T _ D A T A . r e q u e s t ( D a t a := p d u C K A B , CN_ref, union( T C _ D I S C O N N E C T , P R O T _ E R R O R ), N U L L ))]; [to S: T.imer_re quest ( Name := T A B , Time := T A B J N T E R V A L )]; end; {_  }  ENABLING CONDITION A T _ D A T A . i n d i c a t i o n event occurs at the Transport i n t e r f a c e ; this indicates the arrival of a minor synchronization establishment or c o n f i r m a t i o n ( M K B or M C B ) S P D U . The synchronize minor token is available.  C U R R E N T STATE The session machine is awaiting response f r o m the user for an a c t i v i t y end or major synchronization i n d i c a t i o n .  ACTION A protocol exception report is indicated to the user. The session connection is aborted.  RESULTANT  STATE  The session machine awaits a r r i v a l of an acknowledgement for the abort S P D U .  -146-  ( sy5 )  } < same_state > <~ < W A I T _ F O R _ r e c o v e r y _ S P D U [from T : T _ D A T A . i n d i c a t i o n ] ( (([from T:Spdu.ptype] = M K B ) or ([from T:Spdu.ptype] = MCB)) and not (sy_token = N O T _ A V A I L A B L E ) ) begin end;  >  {  }  ENABLING CONDITION A T _ D A T A . i n d i c a t i o n event occurs at the Transport i n t e r f a c e ; this indicates the arrival of either a minor synchronization establishment or confirmation ( M K B or M C B ) S P D U . The synchronize minor token is available.  CURRENT  STATE  The session machine is awaiting arrival of a recovery. S P D U from the peer session entity to exit the error state.  ACTION No action is t a k e n .  RESULTANT  STATE  The session machine remains in the same s t a t e .  -147-  ( sy6 ) { < same_state > <-- < I D L E _ o r _ R E L R _ M C D R > [from U : S _ S Y N C _ M I N O R . r e s p o n s e ] ( ((activity = NO T_A V A I L A B L E ) or (activity = ON)) and not ( sy token = N O T _ A V AIL A B L E ) and valid_spT [from U:Sync_point] ) ) begin [to T : T _ D A T A . r e q u e s t ( D a t a := pduC2s( M C B , CN_ref, ' [from U:SyncjDoint], NULL, NULL ))]; sync_serial_confirmed := [from U:Sync_point]; end; {_  ENABLING CONDITION A S_SYNC_MINOR.response event occurs at the User i n t e r f a c e ; this indicates the user wishes to respond to a peer i n i t i a t e d minor synchronization request. Either there is no a c t i v i t y management or there is an a c t i v i t y in progress. The synchronize minor token is available. The synchronization point the user wishes to c o n f i r m is v a l i d .  C U R R E N T STATE The session machine is in the idle state or is awaiting response from the user concerning a release request or a major synchronize/activity end signal f r o m the peer session entity.  ACTION A synchronize-minor confirmation (MCB) S P D U is constructed and sent to the peer session entity. The synchronize s e r i a l number in the response is recorded.  RESULTANT STATE The session machine remains in the same s t a t e .  -148-  ( sy7 )  { < same_state > <-- < I D L E _ o r _ D N _ M C D > [from T : T _ D A T A . i n d i c a t i o n ] ( ([from TrSpdu.ptype] = M C B ) and ((activity = N O T _ A V A I L A B I _ E ) or (activity = ON)) and not ( sy token = N O T _ A V A I L A B L E ) and valid_spT [from T:Spdu.psync_serial] ) ) begin [to U: S _ S Y N C _ M I N O R . c o n f i r m ( . Sync_point : = [from T: Spdu.psync_serial], User_data := [from T: Spdu.pdata] )];  sync_serial_confirmed := [from T:Spdu.psync_serial]; end;  {ENABLING CONDITION A T _ D A T A . i n d i c a t i o n occurs at the Transport i n t e r f a c e ; this indicates arrival of a minor synchronization c o n f i r m a t i o n (MCB) S P D U . Either there is no a c t i v i t y management or there is an a c t i v i t y in progress. The synchronize minor token is available. The synchronization point the peer session entity wishes to c o n f i r m is v a l i d .  C U R R E N T STATE The session machine is in the idle state or awaiting a r r i v a l of a disconnect (DN) or major synchronize/activity end acknowledgement ( M C D ) S P D U .  ACTION A synchronize minor c o n f i r m a t i o n synchronization s e r i a l number is recorded.  is  given  RESULTANT STATE The session machine remains in the same s t a t e .  -149-  to  the  user.  The  confirmed  ( mal )  {  }  < W A I T _ F O R _ M C D _ S P D U > < - < I D L E > [from ( ((activity = N O T _ A V A I L A B L E ) or (activity = ON)) and this_side( ma^token ) and ((dk_token = , N O T_A V A I L A B L E ) or this side( dk_token )) and ((sy_token = N O T _ A V AIL A B L E ) or this_side( sy_token )) ) begin [to T: T _ D A T A . r e q u e s t ( D a t a := pduC2s( M K D , CN_ref, sync_serial, NOT_EOACT, [from UrUser data] ))];  U:S_SYNC_MAJOR.request]  increment_sync( sync_serial ); act_end_conf_pending : - F A L S E ; end; {_  }  ENABLING  CONDITION  A S _ S Y N C _ M A J O R . r e q u e s t event occurs at the User i n t e r f a c e ; this indicates the user wishes to establish a major synchronization point. Either there is no a c t i v i t y management or there is an a c t i v i t y in progress. The major/activity token is on this side. The data token is either not available or is on this side. The synchronize minor token is either not available or is on this side. CURRENT  STATE  The session machine is in the idle s t a t e . ACTION A synchronize-major ( M K D ) S P D U is constructed and sent to the peer session entity. The internal synchronization serial number is incremented. RESULTANT  STATE  The session machine synchronization S P D U .  awaits  arrival  of  -150-  an  acknowledgement  for  the  major  ( ma2 ) {  _  _  _  _  _  _  }  < I D L E > <-- < W A I T _ F O R _ S _ M C D _ R E S P > [from ( not act_end_conf_pending ) begin [to T:T DATA.r.equest( D a t a := pduC2s( M C D , CN_ref, sync_serial, NULL, [from U:User_data] ))];  U:S_SYNC_MAJOR.response]  sync_serial_confirmed := sync_serial; end;  E N A B L I N G C O N D l f ION A S _ S Y N C _ M A J O R . r e s p o n s e event occurs at the User i n t e r f a c e ; this indicates that the user wishes to respond to a peer i n i t i a t e d major synchronization request. The session machine is awaiting response for a major synchronization point (and not an a c t i v i t y end) i n d i c a t i o n .  CURRENT  STATE  The session machine is awaiting response from the user concerning a synchronization request or an a c t i v i t y end signal f r o m the peer session entity.  major  ACTION A synchronize-major confirmation ( M C D ) S P D U is constructed and sent to the peer session entity. The synchronization response confirms all previous minor synchroniation points.  RESULTANT  STATE  The session machine goes to the idle s t a t e .  -151-  ( ma3 )  _..} < same_state > <-- < W A I T _ F O R _ D N _ S P D U > [from T : T _ D A T A . i n d i c a t i o n ] ( ([from TrSpdu.ptype] - M K D ) and ((activity = N O T _ A V A I L A B L E ) or (activity = ON)) and other_side( ma_token ) and (dk_token = N O T _ A V A I L A B L E ) and ((sy_token = N O T _ A V A I L A B L E ) or other_side( sy_token)) ) begin if( [from T:Spdu.psync_item] = N O T E O A C T ) then begin [to U : S _ S Y N C _ M A J O R . i n d i c a t i o n ( ,Sync_point : = [from T: Spdu.psync serial], User_data := [from T: Spdu.pdata]")]; act_end_conf_pending := F A L S E ; end else begin [to U : S _ A C T I V I T Y END.indication( ,Sync_point := [from T: Spdu.psync serial],. User_data := [from T: Spdu.pdata]")]; act_end_conf_pending := T R U E ; a c t i v i t y := O F F ; . end; increment_sync( sync_serial ); end;  '  }  {. ENABLING CONDITION  A T _ D A T A . i n d i c a t i o n event occurs at the Transport i n t e r f a c e ; this indicates that the peer session entity wishes to establish a major synchronization point or end an a c t i v i t y . Either there is no a c t i v i t y management or there is an a c t i v i t y in progress. The synchronize major/activity token is on the other side. The data token is not available. The synchronize minor token is either not available or is on the other side.  C U R R E N T STATE The session machine is awaiting a r r i v a l of a disconnect (DN) S P D U to complete the termination process.  ACTION A synchronize-major or end of a c t i v i t y indication is given to the user. The internal synchronization serial number is incremented. If the peer session entity request is to end the current a c t i v i t y , set the a c t i v i t y s w i t c h to O F F . A flag.-is set denoting whether the incoming S P D U is an a c t i v i t y end indication or not. -152-  RESULTANT  STATE  The session machine remains in the same s t a t e .  -153-  ( ma4 )  {  }  < W A I T _ F O R _ S _ M C D _ R E S P > <-- < I D L E > [from ( ([from T:Spdu.ptype] = M K D ) and ((activity = N O T _ A V A I L A B L E ) or (activity = ON)) and other_side( ma_token ) and ((dk_token = N O T _ A V A I L A B L E ) or other_side( dk_token)) and ((sy_token = N O T _ A V A I L A B L E ) or other_side( sy_token)) ) begin if( [from T:Spdu.psync_item] = N O T _ E O A C T ) then [to U : S _ S Y N C _ M A J O R . i n d i c a t i o n ( -Sync_point := [from T: Spdu.psync serial], User_data := [from T: Spdu.pdata] )] else [to U : S _ A C T I V I T Y _ E N D . i n d i c a t i o n ( ,Sync_point := [from TY Spdu.psync_serial]j" User_data := [from T: Spdu.pdata] )];  T:T_DATA.indication]  -  increment_sync( sync_serial ); end; {_  }  ENABLING CONDITION A T _ D A T A . i n d i c a t i o n event occurs at the Transport i n t e r f a c e ; this indicates the peer session entity wishes to establish a major synchronization point or end an a c t i v i t y . Either there is no a c t i v i t y management or there is an a c t i v i t y in progress. The synchronize major/activity token is on the other side. The data token is either not available or is on the other side. The synchronize minor token is either not available or is on the other side.  C U R R E N T STATE The session machine is in the idle s t a t e .  ACTION A synchronize-major or end of a c t i v i t y indication is internal synchronization s e r i a l number is incremented.  RESULTANT  given  to  the user.  The  STATE  The session machine awaits response synchronization or a c t i v i t y end i n d i c a t i o n .  -154-  from  the  user  concerning  the  major  ( ma5 )  } < W A I T _ F O R _ A A _ S P D U > <-- < W A I T _ F O R _ S _ M C D _ R E S P > [from T : T _ D A T A . i n d i c a t i o n ] ( (([from TrSpdu.ptype] = M K D ) or ([from TrSpdu.ptype] = MCD)) ) begin [to U: S _ P _ E X C E P T I O N _ R E P O R T . i n d i c a t i o n ( Reason := P R O T O C O L _ E R R O R . • ) ] ; [to T: T _ D A T A . r e q u e s t ( D a t a := p d u C K A B , CN_ref, union( T C _ D I S C O N N E C T , P R O T _ E R R O R ), N U L L ))]; [to S: Timer_request( Name := T A B , Time := T A B J N T E R V A L )]; end;  {_  „_____}  ENABLING CONDITION A T _ D A T A b d i c a t i o n event occurs at the Transport i n t e r f a c e ; this indicates the arrival of a major synchronization/activity end establishment or c o n f i r m a t i o n ( M K D or MCD) SPDU.  C U R R E N T STATE The session machine is awaiting response f r o m the user on an a c t i v i t y end/major synchronization i n d i c a t i o n .  ACTION A protocol exception report is indicated to the user. The session connection is aborted.  RESULTANT The SPDU.  STATE  session machine awaits the a r r i v a l of an acknowledgement for the  -155-  abort  ( ma6 )  {  ,  }  < I D L E > <-- < W A I T _ F O R M C D _ S P D U > [from ([from T:Spdu.ptype] = M C D )  T:T_DATA.indication]  begin if act_end_conf_pending then begin [to U: S ^ A C T I V I T Y _ E N D . c o n f i r m ( User_data := [from T:. Spdu.pdata] )]; a c t i v i t y := O F F ; end else [to U: S _ S Y N C _ M A J O R . c o n f i r m ( User_data := [from T: Spdu.pdata] )]; sync_serial_confirmed := s y n c _ s e r i a l ; end;  {ENABLING CONDITION A T _ D A T A . i n d i c a t i o n occurs at the Transport i n t e r f a c e ; this indicates arrival of a major synchronization/activity end confirmation (MCD) S P D U .  CURRENT  STATE  The session machine is awaiting a r r i v a l of the M C D S P D U .  ACTION A synchronize major/activity end c o n f i r m a t i o n is given to the user. The s e r i a l number of the synchronization point confirms a l l previous minor synchronization points. If the acknowledment S P D U is for the end of an a c t i v i t y , set the a c t i v i t y switch to O F F . -  RESULTANT  STATE  The session machine goes to the idle s t a t e .  -156-  ( ma7 )  {  }  < W A I T _ F Q R recovery_SPDU > <-- < WAIT_FORJ-ecovery_SPDU > Tfrom T:T_DATA.indication] ( ([from TrSpdu.ptype] = M K D ) and not (ma_token = N O T _ A V A I L A B L E ) ) 0  begin  end;  }  {. ENABLING CONDITION  A T _ D A T A . i n d i c a t i o n event occurs at the Transport i n t e r f a c e ; this indicates the arrival of a major synchronization/activity end (MKD) S P D U . The synchronize major/activity token is available. C U R R E N T STATE The session machine is awaiting arrival of a 'recovery' S P D U from the peer session entity to exit the error state. ACTION No action is taken. RESULTANT STATE The session machine remains in the same s t a t e .  -157-  ( al )  < same_state > <-- < I D L E > [ from U: S_ACTIVITY_BEGIN.request ] ((activity = O F F ) and this_side( ma_token ) and (this_side( sy_token ) or (s,y_token = N O T _ A V A I L A B L E ) ) and ((dk_token = N O T _ A V A I L A B L E ) or this_side( dk_token )) ) begin activity = O N ; if( [from U:Type] - S T A R T ) then begin sync_serial := I N I T _ S Y N C _ S E R I A L ; user_data := pduC2a(AS, CN_ref, NULL, NULL, [from U : A c t i v i t y _ i d ] , [from U:User_data] );  end; else begin ,„ . ^ sync_serial := [from U:Sync_point]; user_data := pduC2a(AR, CN_ref, _ sync_serial, [from U:01d_act_id], [from U : A c t i v i t y _ i d ] , [from U:User data] );  end; [to T : T _ D A T A . r e q u e s t ( D a t a : = user data; )]; end; {_  }  ENABLING CONDITION A S_ACTIVITY_BEGIN.request event occurs „at the User i n t e r f a c e ; this indicates the user wishes to begin or resume an a c t i v i t y . There is currently no activity in progress. The synchronization major/activity token is on this side. The data token (synchronization minor token) is either not available or is on this side.  CURRENT  STATE  The session machine is in the idle s t a t e . -158-  ACTION The session machine constructs and sends either an a c t i v i t y start (AS) or an a c t i v i t y resume (AR) S P D U to the peer session entity depending on the type specified in the user request. If it is a S T A R T request, then reset the internal synchronization serial number; otherwise set it to the user supplied value. The a c t i v i t y switch is set to ON.  RESULTANT  STATE  The session machine remains in the same s t a t e .  -159-  ( a2 )  {  }  < same_state > <~ < I D L E _ o r _ D N > [ from T: T _ D A T A . i n d i c a t i o n ] ( ([from T:Spdu.ptype] = AS) and (activity = O F F ) and other_side( ma_token ) and ((sy_token = N O T _ A V A I L A B L E ) or other_side( sy__to,ken )) and ((dk_token = N O T _ A V AIL A B L E ) or other_side( dk_token )) ) begin sync_serial : = I N I T _ S Y N C _ S E R I A L ; [to U:S_ACTIVITY_BEGIN.indication( A c t i v i t y _ i d := [from T:Spdu.pnew_act_id], Type := S T A R T , User_data := [from T:Spdu.pdata] )]; activity = O N ; end;  {  }  ENABLING CONDITION A T _ D A T A . i n d i c a t i o n event occurs at the Transport i n t e r f a c e ; this indicates the arrival of an a c t i v i t y start (AS) S P D U . There is currently no a c t i v i t y in progress. The synchronize major/activity token is not on this side. The data token (synchronize minor token) is either not available or is on the other side. CURRENT  STATE  The session machine is acknowledgement (DN) S P D U .  in  the  idle  state  or  is  awaiting  a  disconnect  ACTION The internal synchronization serial number is reset. The session, machine notifies the user by i n i t i a t i n g an S _ A C T I V I T Y _ B E G I N . i n d i c a t i o n event. The a c t i v i t y switch is set to O N . RESULTANT  STATE  The session machine remains in the same s t a t e .  -160-  ( a3 )  {  }  < same_state > <-- < IDI_E_or_DN > [ f r o m T: T _ D A T A . i n d i c a t i o n ] ( ([from TrSpdu.ptype] = A R ) and (activity = O F F ) and other_side( ma_token) and ((sy_token = N D T _ A V AIL A B L E ) or other_side( sy token )) and ((dk_token = N O T _ A V AIL A B L E ) or other_side( dt_token )) ) begin sync_serial := [from T:Spdu.psync_serial]; [to U : S _ A C T I V I T Y _ B E G I N . i n d i c a t i o n ( Activit.y_id := [from T:Spdu.pnew_act_id], Type := C O N T I N U E , 01d_act_id := [from T:Spdu.pold_act_id], ,Sync_point := s y n c _ s e r i a l , User_data := [from TrSpdu.pdata] )];  activity = O N ; end;  {ENABLING CONDITION A T _ D A T A . i n d i c a t i o n event occurs at the Transport i n t e r f a c e ; this indicates the arrival of an a c t i v i t y resume (AR) S P D U . There is currently no a c t i v i t y in progress. The major synchronization/activity token is on the peer entity side. The data token (minor synchronization token) is not available or is on the other side.  CURRENT  STATE  The session machine is in the idle state or is waiting for arrival of a disconnect acknowledgement (DN) S P D U .  ACTION The internal synchronization serial number is set to the received serial number. The session machine notifies the user by i n i t i a t i n g an S_ACTIVITY_BEGIN.indication event. The a c t i v i t y switch is set to O N .  RESULTANT  STATE  The session machine remains in the same s t a t e .  -161-  ( a4 )  }  {.  < W A I T _ F O R _ M C D _ S P D U > <-- < I D L E > [from U : S _ A C T I V I T Y _ E N D . r e q u e s t ] ( (activity = ON) and this_side( ma_token ) and ((dk_token = N O T _ A V A I L A B L E ) or this_side( dk_token )) and ((sy_token = N O T _ A V A I L A B L E ) or this_side( sy_token )) ) begin [to T: T_DATA.request( D a t a := pduC2s( M K D , CN_ref, , sync_serial, EOACT, [from U i U s e r data] . ))]; increment_sync( sync_serial ); act_end_conf_pending := T R U E ; end;  {  }  ENABLING  CONDITION  A S _ A C T I V I T Y _ E N D . r e q u e s t event occurs at the User i n t e r f a c e ; this indicates the user wishes to terminate an a c t i v t y . There is an a c t i v i t y in progress. The synchronize major/activity token is on this side. The data token is either not available or is on this side. The synchronize minor token is either not available or is on this side. CURRENT  STATE  The session machine is in the idle s t a t e . ACTION A synchronize-major ( M K D ) S P D U is constructed and sent to the peer session entity. The internal synchronization serial number is incremented. RESULTANT  STATE  The session machine awaits arrival of an acknowledgement for the a c t i v i t y end (MKD) S P D U .  -162-  ( a5 )  } < I D L E > <-- < W A I T _ F O R _ S _ M C D _ R E S P > [from U:S_ACTIVITY_END.response] ( act_end_conf_pending ) begin [to T : T _ D A T A . r e q u e s t ( D a t a := pduC2s( M C D , CN_ref, sync_serial, NULL, [from U:User data] ))];  sync_serial_confirmed := s y n c _ s e r i a l ; a c t i v i t y := O F F ; end;  {  }  ENABLING CONDITION A S_ACTIVITY_END.response event occurs at the User i n t e r f a c e ; this indicates the user wishes to respond to a peer i n i t i a t e d a c t i v i t y end request. The session machine is awaiting a response for an end of a c t i v i t y (and not a major synchronization) i n d i c a t i o n .  C U R R E N T STATE The session machine is awaiting response f r o m the user concerning an a c t i v i t y end signal f r o m the peer session entity.  ACTION A synchronize major ( M C D ) S P D U is constructed and sent to the peer session entity. The a c t i v i t y end response confirms a l l previous minor synchroniation points. The a c t i v i t y switch is set to O F F .  RESULTANT  STATE  The session machine goes to the idle s t a t e .  -163-  ( a6 )  {  }  < W A I T _ F O R _ A I A _ S P D U > <-- < I D L E _ o r _ r e c _ R E Q > [from U : S _ A C T I V I T Y _ I N T E R R U P T . r e q u e s t ] ( (activity = ON) and this_side( ma_token ) and ((dk_token = NO T R A V A I L A B L E ) or this_side( dk_token )) ) begin [to T: T_DATA.request( D a t a := pduDT( AI, CN_ref, NULL ))]; end;  ENABLING CONDITION A S _ A C T I V T T Y _ I N T E R R U P T . r e quest event occurs at the User i n t e r f a c e ; this indicates the user wishes to interrupt the current a c t i v i t y . There is an a c t i v i t y in progress. The synchronize major/activity token is on this side. The data token is either not available or is on this side.  C U R R E N T STATE The session machine is in the idle or error s t a t e .  ACTION A a c t i v i t y interrupt (AI) S P D U is constructed and sent to the peer session e n t i t y .  RESULTANT  STATE  The session interrupt S P D U .  machine  awaits  arrival  of  -164-  an acknowledgement  for  the  activity  ( a7 )  {  }  < W A I T _ F O R _ S _ A I _ R E S P > <-- < IDLE_or r e c _ S P D U > [ f r o m T: T _ D A T A . i n d i c a t i o n T ( ([from TrSpdu.ptype] = Al) and other_side( ma_token ) and (activity = ON) and ((dk_token = N O T _ A V A I L A B L E ) or other_side( dk_token )) ) begin [to end;  U:S_ACTIVITY_INTERRUPT.indication];  {  }  ENABLING CONDITION A T _ D A T A . i n d i c a t i o n event occurs at the Transport i n t e r f a c e ; this indicates that the peer session entity wishes to interrupt the current a c t i v i t y . The synchronize major/activity token is not on this side. There is an a c t i v i t y in progress. The data token is either not available or is on the other side.  C U R R E N T STATE The session machine is in the idle or error s t a t e .  ACTION The session machine notifies S _ A C T I V I T Y _ I N T E R R U P X . i n d i c a t i o n event.  RESULTANT  the  user  by  initiating  an  STATE  The session machine interrupt request.  awaits  response  from  -165-  the  user  concerning the  activity  ( a8 )  } < I D L E > <-- < W A I T _ F O R _ S _ A I R E S P > [from U : S _ A C T I V I T Y _ I N T E R R U P T . r e s p o n s e ] begin ~ [to T:T_DATA.request( D a t a := pduDT( A I A , CN_ref, NULL. ))]; a c t i v i t y := O F F ; end; {_  }  ENABLING CONDITION A S_ACTIVITY_INTERRUPT.response event occurs at the User i n t e r f a c e ; this indicates the user wishes to respond to a peer i n i t i a t e d a c t i v i t y interrupt.  C U R R E N T STATE The session machine is awaiting response f r o m the user concerning an a c t i v i t y interrupt f r o m the peer session entity.  ACTION A n a c t i v i t y interrupt acknowledgement (AIA) S P D U is constructed and sent to the peer session e n t i t y . The a c t i v i t y switch is set to OFF...  RESULTANT  STATE  The session machine goes to the idle s t a t e .  -166-  ( a9 )  {  }  < I D L E > <-- < W A I T _ F O R _ A l A _ S P D U > [ f r o m T: T _ D A T A . i n d i c a t i o n ] ([from TrSpdu.ptype] - AIA) begin [to U:S_ACTIVITY_INTERRUPT.confirm]; a c t i v i t y := O F F ; end;  {.  „}  ENABLING CONDITION A T _ D A T A . i n d i c a t i o n event occurs at the Transport i n t e r f a c e ; this indicates that the peer session entity wishes to acknowledge the a c t i v i t y interrupt.  C U R R E N T STATE The session machine is acknowledgement (AIA) S P D U .  awaiting  the  arrival  of  an  activity  interrupt  ACTION The session machine S_ACTIVITY_INTERRUPX.confirm  RESULTANT  notifies the user by initiating event. The a c t i v i t y s w i t c h is set to O F F .  STATE  The session machine goes to the idle s t a t e .  -167-  an  ( alO )  } < W A I T _ F O R _ A D A _ S P D U > <-- < I D L E _ o r _ r e c _ R E Q [from U : S _ A C T I V I T Y _ D I S C A R D . r e q u e s t ] ( (activity = ON) and this_side( ma_token ) and ((dk_token = N O T _ A V A I L A B L E ) or this_side( dk_tokeh )) ) begin [to T: T_DATA.request( D a t a := pduDT( A D , CN_ref, NULL.  >  ))]; end;  ..}  {_ ENABLING CONDITION  A S_ACTIVITY_DISCARD.request event occurs at the User i n t e r f a c e ; this indicates the user wishes to cancel the current a c t i v i t y . There is an a c t i v i t y in progress. The synchronize major/activity token is on this side. The data token is either not available or is on this side.  C U R R E N T STATE The session machine is in the idle or error s t a t e .  ACTION A a c t i v i t y discard (AD) S P D U is constructed and sent to the peer session e n t i t y .  RESULTANT  STATE  The session machine awaits arrival of an acknowledgement for the a c t i v i t y discard SPDU.  -168-  ( all )  {  }  < W A I T _ F O R _ S _ A D _ R E S P > <-- < I D L E _ o r _ r e c _ S P D U > [ from T: T _ D A T A . i n d i c a t i o n ] ( ([from TrSpdu.ptype] = AD) and other_side( ma_token ) and (activity = ON) and ((dk_token = N O T_A V A I L A B L E ) or other_side( dk_token )) ) begin [to end;  U:S_ACTIVITY_DISCARD.indication];  {  }  ENABLING CONDITION A T _ D A T A . i n d i c a t i o n event occurs at the Transport i n t e r f a c e ; this indicates that the peer session entity wishes to cancel the current a c t i v i t y . The synchronize major/activity token is on the peer entity side. There is an a c t i v i t y in progress. The data token is either not available or is on the other side.  C U R R E N T STATE The session machine is in the idle or error s t a t e .  ACTION The session machine S_ACTIVITY_DISCARD.indication  RESULTANT  notifies event.  the  user  by  initiating  an  STATE  The session machine awaits response f r o m the user concerning the a c t i v i t y discard request.  -169-  ( al2 )  } < I D L E > <-- < W A I T _ F O R _ S _ A D _ R E S P > [from U:S_ACTIVITY_DISCARD.response] begin [to T:T_DATA.request( D a t a := pduDT( A D A , CN_ref, NULL  a c t i v i t y := O F F ; end;  {ENABLING CONDITION A S_ACTIVITY_DISCARD.response event occurs at the User i n t e r f a c e ; indicates the user wishes to respond to a peer i n i t i a t e d a c t i v i t y c a n c e l l a t i o n .  this  C U R R E N T STATE The session machine is awaiting response from the user concerning an a c t i v i t y cancellation f r o m the peer session entity.  ACTION An a c t i v i t y discard acknowledgement ( A D A ) S P D U is constructed and sent to the peer session entity. The a c t i v i t y s w i t c h is set to O F F . .  RESULTANT  STATE  The session machine goes to the idle s t a t e .  -170-  

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

Comment

Related Items