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

PROTOCOL SPECIFICATION TECHNIQUES AND SPECIFICATION OF THE ISO SESSION L A Y E R PROTOCOL By Roselyn K a m Yiu^Lee B . S c , The University of Brit ish Columbia , 1982 A THESIS SUBMITTED IN P A R T I A L F U L F I L L M E N T OF THE R E Q U I R E M E N T S F O R THE D E G R E E OF M A S T E R OF SC IENCE 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 THE UNIVERSITY OF BRITISH C O L U M B I A May 1984 © R o s e l y n K a m Y iu Lee , 1984 In presenting t h i s thesis i n p a r t i a l f u l f i l m e n t of the requirements fo r an advanced degree at the University of B r i t i s h Columbia, I agree that the Library s h a l l make i t f r e e l y a v a i l a b l e for reference and study. I further agree that permission for extensive copying of t h i s thesis for s c h o l a r l y purposes may be granted by the head of my department or by his or her representatives. I t i s understood that copying or publi c a t i o n of t h i s thesis f o r f i n a n c i a l gain s h a l l not be allowed without my written permission. Department of COMPUTER SCIENCE The University of B r i t i s h Columbia 1956 Main Mall Vancouver, Canada V6T 1Y3 Date MAY 30, 1984 DE-6 (3/81) A B S T R A C T Communicat ion between computers on a network is coordinated by sets of rules known as communication protocols. It is the formal izat ion of the definitions of such protocols which is the focus of this thesis. Formal specif ications play a key role in the design, implementation and ver i f icat ion 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 specif icat ions. There have been extensive research in the area of formal definit ion of protocols. The techniques introduced generally fa l l into categories of transition models, program models and hybrid (transition and program combined) models. In this thesis, we review various methods in these classes and i l lustrate them with specif ications of the alternating bit protocol . To demonstrate the applicabil i ty of these specif icat ion techniques, we also specify the ISO session layer protocol using one of the (hybrid) methods described. i i T A B L E O F C O N T E N T S A B S T R A C T ii T A B L E OF F IGURES v A C K N O W L E D G E M E N T S vi I. Introduction 1 II. Specif ication of Protocols 3 III. Transition Models 6 A. F in i te State Automaton Models 7 State Transition Diagrams 8 State Decision Tables 9 Formal Grammars 10 Extended State Machine 11 B. Petr i Net Models 12 Coloured Petr i Nets 1 14 Predicate-Transit ion Petr i Nets 14 Numer ica l Petr i Nets 15 Timed Petr i Net 15 IV. Program Models 17 A . Programming Languages 18 B. Flowcharts 20 C . Buffer Histories 21 D. Sequence Expressions 24 V. Hybrid Models 26 A . F A P L 28 B. Specif ication Technique for Protocols 31 C . FDT and PDIL 34 D. A F F I R M 37 E. UNISPEX 40 i i i T A B L E OF CONTENTS (cont.) VI. Formal "Specification of the ISO Session Protocol 44 A. Overview of the Session Protocol 45 Connect ion Establishment Phase 45 Data Transfer Phase 45 Connection Release Phase 47 Protocol Subsets 47 B. Formal Specif ication Technique 48 C . Specif ication of the Session Protocol 51 VII. Conclusions 55 B I B L I O G R A P H Y 58 A P P E N D I X - Specif ication of the ISO Session Protocol 62 iv T A B L E O F FIGURES Figure 1. General View of the Layered Protocol Structure 3 Figure 2. State Diagram for the Alternat ing Bit Protocol 9 Figure 3. State Decision Table for the A B P 10 Figure 4. Formal Grammar for the A B P 11 Figure 5. Pseudo program for the Alternat ing Bit Protocol • 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 for the A B P - 25 .Figure 9. F A P b . FSM's for the Alternat ing Bit Protocol 30 Figure 10. A B P State Transitions - Blumer and Tenney Method 33 Figure 11. FDT transitions of the A B P 36 Figure 12. A F F I R M Axioms of the A B P (from [STEG82]) - 40 Figure 13. Events and Topology of the A B P UNISPEXi f i ca t ion 43 v A C K N O W L E D G E M E N T S I would l ike to acknowledge Dr . Son Vuong whose strong interest in protocol specif icat ion and validation led me to the subject of this work. Dr . 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 c r i t i ca l 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 l ike to express my appreciation for the f inancial support of the Natural Sciences and Engineering Research Counci l of Canada. 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 leve l , this "means" is the protocol, i .e. the procedures which communicating entities must fol low in order to exchange information. Many communication protocols, either in-house or standard, exist to serve various functions. Most of these are extremely complicated due to either their attempt to be general purpose or merely their inherent complexi ty . As a result , problems arise in managing all 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 di f f icult ies is to have a formal ism for defining protocols clearly and concisely. Natural language is a popular approach to describing protocols. Although such descriptions are undoubtedly useful for conveying a general understanding of a protocol , they tend to be not only lengthy but also open to conf l ict ing interpretations. Furthermore, when one is concerned with ver i f icat ion 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 speci f icat ion and analysis of programming algorithms. The approaches basically fa l l into three categories: transition models, program models and hybrid models combining the f i rst two methodologies. Transition models are based on state transitions of f ini te machines. They are ideal for -1-capturing the control features of protocols. Methods in this category include f inite state automata(FSA), petri nets and grammars. A t the other end of the spectrum, program models are able to depict the data flow and algorithmic nature of the protocols. Flowcharts and high level or pseudo programming languages belong to this class of approach. Specif ication techniques, however, do not fa l l s t r ic t ly into these two classi f icat ions. In fac t , there are a wide range of techniques lying between the two extremit ies . Of these, we can distinguish a group known as event models which are concerned with the sequence of interact ion events and could be considered closer to (or belonging to) the program model approach. Examples of event models are sequence expressions and buffer histories. Due to the inherent l imitat ions of the transition and program models, the most pract ical methods combine the two philosophies to obtain advantages of both - the hybrid models. Often hybrid models consist of a high level programming language augmented with state transition funct ional i t ies. One such hybrid technique, by Blumer and Tenney, is examined in detail and applied to the ISO session layer protocol . In the fol lowing chapter, we discuss what is meant by protocol spec i f icat ion . Chapters 3, 4 and 5 survey various transit ion, program (including event) and hybrid modell ing techniques, respectively. Descriptions of the alternating bit protocol (ABP) [STEG82,Boch78] using these methods are given as examples. Chapter 6 contains a description of the hybrid speci f icat ion technique by Blumer and Tenney as wel l as discussions of experiences in applying it to the ISO session layer protocol . The actual speci f icat ion is included in the appendix. - 2 -Chapter II Specification of Protocols In our discussions, we view a communication system as being composed of a hierarchy of protocol layers as described in the ISO Open System Archi tecture 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 rom the N -1 lower layers. It is useful for a user to consider al l layers beneath it col lect ively as a "black box". Thus at any given layer, one is concerned local ly 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). L A Y E R n + l U S E R S < : : : : : : : : : : : : : : : : : s e r v i c e i n t e r f a c e : : : : : : : : : : : : : : : : : > A A I I I I V V + + + + I L A Y E R n I > I L A Y E R n I I PROTOCOL. | \ | PROTOCOL I I E N T I T Y |< I E N T I T Y I + + + + A A I I V V + + I COMPOSITE OF L A Y E R S 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 speci f icat ion . It contains abstract descriptions of the allowable sequences of service pr imit ives, their ef fects , as wel l 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 w h a t is available rather than how i t is achieved. The specif icat ion 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 specif icat ion of the protocol" [Sidh81] is known as the (internal) protocol spec i f icat ion . It describes appropriate actions by a protocol in response to al l interactions with the user (commands), lower layer entity (incoming messages from the peer entity) and local system environment (timeouts). Although a great deal more details must be outlined (than in the service specif ications) , a high level of abstraction is nevertheless desirable. Ideally, a specif icat ion should "define each entity to the degree necessary to ensure compatibi l i ty with other ent i t ies, but no further" ,[BoSu80]. In other words, there should be no ambiguities which may consequently af fect the interaction of communicating ent i t ies. Y e t , the amount of details should not restr ict or bias implementation choices needlessly. It is this description of protocols to which formal specif icat ion techniques generally are applied. There have been discussions in the l i terature concerning exactly what constitutes a complete protocol (service and internal) speci f icat ion [BoSu80,SiKa82]. General ly , a speci f icat ion 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 specif icat ion is that of the protocol entity: its overall operation, the types and formats of messages exchanged, and rules governing its actions. Other nonessential sections may be included to elaborate on execution environment requirements and implementation strategies or ef f ic iency issues. Obviously, a • -4 -specif icat ion cannot be presented entirely in english or entirely in some formal notation but must be a combination of both. General ly , formal techniques are applied in defining the service interfaces and operation of the protocol entity , although most concentrate on the lat ter . It is suff ic ient for the remainder of the speci f icat ion to be given in prose. [SiKa82] outlines the requirements for the various components of a complete protocol spec i f icat ion . Let us now turn our attention to the various techniques for describing protocols. - 5 -Chapter III Transition Models Protocols are character ized 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 far . State transition models are natural for depicting such systems. There are two main types of state transit ion speci f icat ion techniques: those based on f inite state automata (FSA) and those based on petri nets. F S A have the advantage of being more easily understood but lack the expressibil ity of petri nets in modell ing concurrent processes. Both, however, provide concrete models on which proofs of general properties of protocols (liveness, safety , etc) may be based. Proof methodologies founded on transition models including reachabil i ty analysis and analysis by invariants have been successfully automated [RWZa78,ACDi82] . While the control f low of a protocol can be clearly displayed using transit ion models, its semantic details are not so apparent. Moreover, the readabil ity of F S A state diagrams and petri nets is not always preserved as the more complex protocols have unmanageable numbers of states and transit ions. In part icular , 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 t imers. Since at any given state, al 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-t imer value) space - possibly inf in i te . Extensions to the basic F S A and petri net models for rect i fy ing some of these shortcomings have been proposed. It should be noted that the further a model strays from a pure transition model , the less applicable are the properties of a transition model to the augmented model . And hence, the ver i f icat ion 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 f inite state automaton (FSA) [Dant80,Boch78]. A F S A consists of the 5-tuple, <S, I, O, X,. A> where, S is a f ini te set of states I is a f ini te set of inputs , • is a f ini te 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 in i t ia l state is usually defined as we l l . A t a given state, the next input, applicable state transit ion 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 the transmittor and receiver modules. - 7 -F S A have the virtue of being readily represented as state transit ion diagrams, as decision tables and as formal grammars. Since these are merely representations of F S A , they inherit the l imitat ions associated with F S A . Thus there is a need to extend the basic F S A model . We wi l l look at some such attempts after we discuss the representation techniques. State Transition Diagrams A FSA is most commonly represented graphically by a state transit ion diagram - a directed graph whose nodes indicate states and whose arcs denote transit ions. There are various notations for labell ing the arcs in a state diagram. One convention is to associate an arc with either the transmission or reception of a message, e.g. +DATA 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 r e q u e s t d e n o t e s r e c e p t i o n o f an open r e q u e s t and CONNECT s u b s e q u e n t t r a n s m i s s i o n o f a CONNECT m e s s a g e State transition diagrams are useful for pictor ial ly displaying the control structure and basic mechanisms of simple protocols or subsets (or phases) of more complex protocols. However, it is awkward to include features other than reception and transmission of messages in the diagrams. Moreover, once the number of states reaches a certain threshold, the diagrams become cluttered and d i f f icu l t to fo l low. At this point the other two representation schemes are more appropriate. -8-Sender Rece i ve r + E , + D 1 , [ T ] +E,+D0,[T] Figure 2. State Diagram for the Alternating Bit Protocol State Decision Tables A FSA may be represented as a state transition matr ix or often referred to as a decision table. States are l isted as column headings and the possible events (messages or commands) as row headings (or vice versa). A c e l l , corresponding to the intersection of a state and an event, contains the resultant state (and action) for the occurrence of the event at the former state . An empty ce l l may be used to signify that an event occuring at a certain state is inval id or requires response which is implementation dependent. A large protocol may be described using several tables for its various modules (phases). Decision tables, although infeasible to carry a large amount of detai ls, are handy as quick reference guides or summaries. For instance, the document of the ISO session layer protocol definit ion has decision tables included as annexes [!S083p]. -9-S e n d e r R e c e i v e r EVENTS STATES sO | wO | s i I w l I STATES EVENTS| rO I r l I s e n d |SendDO r e q u e s t I I wO I S e n d D l 1 1 w l + — — — — . _ i i i 1SendDl 1 1 w l R e c v D O I c o n s ume 1SendAO 1 r l 1SendAO 1 r l R e c v A O | 1 s i 1 1 1 R e c v D l 1 S e n d A l 1 I rO I c o n s ume I S e n d A l 1 rO R e c v A l | ISendDO 1 wO 1 1 1 1 sO R e c v E R l S e n d A l I rO — 1SendAO 1 r l R e c v E R l 1SendDO 1 wO 1 1 1 S e n d D l 1 w l T i m e o u t 1 S e n d A l 1 rO 1SendAO 1 r l T imeou t I 1SendDO 1 wO ! I S e n d D l 1 w l Figure 3. State Dec i s ion Tab le for the A B P F o r m a l Grammars There is a direct translation from a F S A description of a protocol to a formal grammar. Transitions are mapped to production rules of the grammar. States correspond to nonterminal symbols and input/output events to terminal symbols. The in i t ia l state, of course, is represented by the start ing symbol of the grammar. The sentences of the formal 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 input and output symbols (except in the mnemonics assigned to them). -10-Sender R e c e i ve r SO DO WO = <get 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 RO : : = R e c v D a t a O ( c o n s u m e ) AO I R e c v D a t a l A l I R e c v E r r A l I T i m e o u t A l : : = S e n d A c k O R I 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 AO SI DI W l = <get m e s s a g e ) D I = S e n d D a t a l W l = R e c v A c k l SO R I : : = R e c v D a t a l ( c o n s u m e ) A l 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 I R e c v A c k O D I I R e c v E r r D I I T i m e o u t D I A l : : = S e n d A c k l RO Figure 4. Formal Grammar for the ABP 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 modif icat ions, are adequate in representing the control structure of the protocols. Str ict ly 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 anal izabi l i ty" . States and events are grouped into classes to increase readabil i ty and compactness of the descriptions. This c lass i f icat ion technique enables more complex protocols to be handled. I n - fac t , specif icat ions of the A R P A T C P and IP protocols have been prepared according to the guidelines described in [SiKa82]. The "hierarchy of state machine" concept is also introduced; that is, the overal l state machine is divided into logical submachines such as connection establishment phase, data transfer phase or connection release phase modules. These - 1 1 -subordinate machines may be "invoked" from the top level state machine analogous to the invocation of subroutines in programming environments. Further- extensions to FSA are discussed in the chapter on hybrid models. B. Petri Net Models Petr i nets were in i t ia l ly introduced to model act iv i t ies of concurrent systems. Since communication protocols fa l l into this c lass i f icat ion, various protocol specif icat ion techniques have been developed based on petri nets and their extensions [Diaz82,Bi l l82,JuVu84]. A petri net can be described formal ly 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: PxT -> N; where N is the set of integers) Q is the output or backward incidence function (O: PxT -> N) Graphical ly , petri nets are represented as directed graphs with arcs interconnecting places (circles) and transitions (bars). An 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 may be used to - 1 2 -represent incoming/outgoing messages, commands, conditions or other quantit ies. An assignment of tokens to places is known as the marking of a petri net- A marking is analogous to a F S A state. In the formal sense, a definit ion of a petri net is incomplete without speci f icat ion of its in i t ia l marking. Markings are modif ied according to the incidence functions. The operation of a protocol machine may be traced by the sequence of markings of its corresponding petri net. Arcs may have weights associated with them (the default weight is 1). (When al l weights are 1, the petri net is said to be "safe"). For an input arc , its weight is the number of tokens its associated place must contain before the arc is "enabled". When al l input arcs to a transition is enabled, the transition is said to be enabled. An enabled transit ion may " f i re" . F i r ing 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 labell ing the corresponding input and output arcs. During the f i r ing of a transit ion, the number of tokens need not be preserved. New tokens may be created and "old" ones destroyed. This fac i l i tates the modell ing of parallel processing such as execution of two child processes spawned f rom a parent process during a transit ion. Although petri nets are able to model expl ic i t ly 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 identif ied - coloured petri nets; relationships may be imposed on tokens - predicate transit ion nets; predicated actions may label transitions - numerical petri nets; and f i r ing t ime intervals may be associated with transitions -t imed petri nets. Many of these extensions have equivalent counterparts in FSA models. While some of these s impl i fy the modell ing process, they do not increase the power of the basic petri nets. The numerical petri nets are the exceptions because they are actual ly hybrid models. The paper by D iaz [Diaz82] contains a comprehensive - 1 3 -description of petri nets and their variants, which are summarized in the fol lowing, as wel l as a petri net description of the alternating bit protocol . Coloured Petri Nets In basic petri nets, tokens do not have identi t ies. This is quite adequate for modell ing boolean or quantitative entit ies. 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 ia 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 lass i f ied. The concepts of enabling and f i r ing have to be extended as w e l l . Arcs are labelled with "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 f i re 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 specif ies the tokens to be assigned to the output places upon f i r ing . The introduction of coloured tokens greatly simplif ies 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 suff ic ient ; one needs to be able to define relationships on the tokens to fac i l i ta te modell ing of such systems. In predicate-transit ion nets, the tokens of the input places must satisfy expressions specif ied in corresponding input arcs to a transit ion, in order for that transit ion to f i re . Predicates on the output arcs determine relationships between tokens added to the output places. Predicate- t ransi t ion nets are no more powerful -14-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 needs to be able to specify, for instance, systems in which messages may 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 features in a -15-communication protocol. Chapter IV Program Models Another view of communication protocols is as sets of procedures. As such, it seems appropriate to specify protocols using the same techniques used to define programming algorithms. There are a variety of program description techniques including conventional approaches such as f lowcharts and high level programming languages, and event-based schemes which concentrate on the sequence history of operations of interact ing entit ies. The lat ter 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 d i f f icu l t to "separate the essential features of what the program is supposed to do f rom the particular way chosen to accomplish those functions" [Suns79]. Not only are implementation decisions biased but the speci f icat ion may be cluttered up with unnecessary details. A higher level of abstraction is often sought. Furthermore, a program description often hides the control f low structure of the protocol making it very cumbersome to fol low the logic of the protocol . It becomes d i f f icu l t to analyze the protocols as well as verify or validate them. Assertion and other methods used in verifying correctness of programs can be generalized to apply to protocols. Hbwever, program ver i f icat ion is itself a nontrivial task, and so, the situation is worst for protocol ver i f icat ion . - 1 7 -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 as describing programs or algorithms using such languages. One simply recognizes the fact that a protocol is just another type of algorithm.. Complex protocols can be handled relat ively easily since variables can be used to store as much status information as required. The speci f icat ion also serves as a natural implementation model (depending on what the target implementation and speci f icat ion languages are, of course). As mentioned, however, a higher level of abstraction is often preferred. One way of achieving a higher level of abstraction is to specify as l i t t le of the protocol as possible using programming languages. In [Wats82], Pascal is used to specify the "legal protocol operation" and English for "environment detai ls" of a transport protocol . The approach, given the name "abstract behavioural spec i f icat ion" , is aimed at expressing operations on objects in a nonprocedural manner. User interfaces, operating environment, addressing, f low contro l , buffer management, e tc . , are described in English (about half of the entire description) while details pertaining to correct protocol operation, such as transmission/reception of data and t imer events, are written in Pasca l . Although there is a higher level of abstraction gained in specify ing some aspects of the protocol in natural language, the authors admit that there is s t i l l an undesirable amount of restr ict ion imposed on implementation choices. - 1 8 -procedure Sender i := 0; repeat getdata( D(i) ); repeat send( D(i) ); startt imer( 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 - 1 9 -B. Flowcharts Just as flowcharts are used to pictor ial ly represent algorithms, they are used to model protocols as we l l . Conventional f lowchart ing 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 protocol machines) using flowcharts._ Such a f lowchart , cal led a protocol sequence graph, describes the actions of one communicating ent i ty ; that is , it gives a local rather than a global speci f icat ion. There are four types of nodes used corresponding to the wr i te , read, assignment and conditional statements in high level languages, respectively: send node - denotes transmission of a specif ied message to a designated destination. It is represented by a square with one output arc (or edge). receive node - denotes reception of a message from a set of expected messages f rom a designated source. It is represented by a c i rc le with as many output arcs as expected messages plus a " t imeout" arc . The timeout arc is taken if none of the expected messages arrive by a specif ied period of t ime. assignment node - denotes specif ied operations and assignments to be performed. It is represented by a bar with one output arc . 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 Binary Synchronous Communicat ion (BiSync) Protocol is defined using protocol sequence graphs. , Since each f lowchart has a corresponding equivalent program, f lowchart ing techniques have the same power as the programming language methods discussed above. -20-S e n d e r R e c e i v e r V I NV V \JS + + I I i <- 0 m E + + I D ( i ) I A ( j ) i <- i+1 [ T ] E j <- 0 I D ( i ) J - < - j+-l + + A ( j ) Figure 6. Protocol Sequence Graph for the ABP C. Buffer Histories Buffer histories refer to records of messages sent and received between processes communicating via message passing. States are not modelled expl ic i t ly 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 was not designed specifically for defining communication protocols but for concurrent systems in 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 of the goals of the language is to facilitate automatic verification of properties of the systems defined). References [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. A process' (local) state vector is updated when an event occurs, reflecting a 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 histories or expressions involving -22-histories". This technique is geared towards mechanical verif ications of system operations. It is , however, quite l imited in modell ing the control aspects of a protocol due to separate histories being kept for incoming and outgoing data. In fac t , the authors point out that with the existing speci f icat ion technique, it is not possible to describe the connecting phase of a protocol . The fol lowing is a process description of the A B P ; it does not include the decision table definitions of the event handlers. process ABP (input source: message; output sink: message) = begin buffers( sndr_pkt, rcvr_pkt : packet; sndr_ack, rcvr_ack: natural ; cobegin sender( source, sndr_ack, sndr_pkt ); receiver( rcvr_pkt , sink, rcvr_ack ); medium( sndr_pkt, rcvr_pkt ); medium( rcvr_ack, sndr_ack ); end end; process medium (input in_buf: T; output out_buf: T) = pending; process sender (inputs source: message; ack_in : natural ; output pkt_out: packet) = begin state vector( seq: natural ; in_transit : boolean; to_t ime: natural); initiallyC 0, false, 0 ); events true => on receipt of ack from ack_in handle by ack_hdlr ; in_transit => after to_t ime handle by st imeout_hdlr ; not in_transit => on receipt of mess f rom source handle by source_hdlr; end end; process receiver (input pkt_in: packet; outputs sink: message; ack_out: natural) = begin state vector( next: natural ; in_transit : boolean; to_t ime: natural ); init ial ly( 0, false, 0 ); events true => on receipt of pkt f rom pkt_in handle by pkt_hdlr; in_transit => after to_t ime handle by rt imeout_hdlr ; end end; Figure 7. Seguential Processes of the ABP -23-D. Sequence Expressions Sequence expressions is an "algebraic" approach to specifying protocols. The operation of the protocol is defined by a sequence of regular expressions. In the formal sense, sequence regular expressions are neither true program nor transit ion models. Expressions correspond to FSA and (type 3) formal grammars; however, they contain neither expl ic i t states nor impl ic i t 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 fol lowing operators: * arbitrary repetit ion (Kleene closure), -> followed by, and spaces-within-brackets alternatives. Schindler [Schi80] has suggested additional features to the basic scheme to make sequence expressions more suitable for modell ing protocols. . Terms within an expression may be labelled with "rejection predicates" composed of parameters of current and previous operations and of the number of operations of a certain type previously executed. An operation which contains a term whose predicate is false becomes inval id . An expression may be divided into "blocks", each of which corresponds to a nonterminal symbol in formal grammars or, f rom another point of view, to a program procedure or funct ion. Blocks may have mult iple exit blocks in order for exceptions to be easily handled. The paper by_ Schindler contains more details on speci f icat ion of protocols using sequence expressions. -24-SENDER := { DATAO -> D A T A 1 }* ; D A T AO := J s.DO -> RECVO } ; RECVO := { (r.AO -> DATA1) ( r . A l -> DATAO) }, X I := DATAO; D A T A 1 := { s . D l -> R E C V 1 } ; R E C V 1 := { ( r . A l -> DATAO) (r.AO -> DATA1) }, X I := D A T A 1 ; RECEIVER := { DATO -> D A T 1 }* ; DATO := { (r.DO -> SENDO) ( r .D l . -> SEND1) }, X I := S E N D 1 ; SENDO := { s.AO -> D A T 1 }; D A T 1 := { ( r .D l -> SEND1) (r.DO -> SENDO) }, X I := SENDO; SEND1 := { s . A l -> 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 ABP -25-Chapter V Hybrid Models As we have seen, transition techniques are suited to displaying the control f low of protocols whereas program models are ideal for handling their semantic details (variables and parameters). Methods in either category are, however, quite l imited by themselves when " rea l " 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 them. The "state portion" summarizes the overal l control structure of a protocol . The "program portion" specifies the actions, accompanying state changes, according to values of the context variables and input message parameters (eg. sequence numbers). A typical hybrid technique employs a high level programming language "spiced-up" with special constructs for real iz ing state transit ions. Many hybrid models have been developed. Of these, there are two main schools of thought: one aimed at automatic implementation [BlTe82,SRWG80,ACNR83, ISO81] ; the other at ver i f icat ion and validation [STEG82,DaBr78,Sehw81, JuVu84]. A unified implementation and ver i f icat ion oriented model has also been proposed, [VuCo82]. Implementing a complex communication protocol is a nontr iv ial and tedious task, to say to least. If we have a wel l -def ined language for specifying protocols, we must also have a "syntax-checker" available to verify that protocols are specif ied in the - 2 6 -correct syntax. The basic idea behind automatic implementation of protocols is to take this one step further: provide a compiler which not only checks the syntax of specif ications but also translates them into some high level programming language. Of course, only code for the implementation independent portions may be automatical ly generated. Hence, we actually have only semi -automat ic implementation schemes. . Specif icat ion languages in this category include F A P L , the ."Specification Technique for Protocols", FDT and. PDIL . If constructs are avai lable, in a speci f icat ion language, for stat ing invariants about various aspects of a protocol , one could conceivably verify properties of the specif ied protocol based on the actions and transitions defined. Systems have been developed to automate ver i f icat ion of protocols described using hybrid techniques. Ver i f icat ion of hybrid models is considerably less complex than that of pure program models since the "transit ion portions" of the models may be used in the proofs. An example of a specif icat ion language concerned with ver i f icat ion is A F F I R M . Most of the (semi) automatic implementation oriented speci f icat ion techniques are general enough that some features for ver i f icat ion may be included as w e l l . One definit ion scheme which, at its design, incorporates both implementation and ver i f icat ion capabil it ies is U N I S P E X , a "unif ied approach to specif icat ion and ver i f icat ion" . In this chapter, we discuss the various hybrid model speci f icat ion languages named above. The focus is on the general approach taken by each rather than specif ic detai ls. Where appropriate, the methods are compared. -27-A. F A P L The Format and Protocol Language (FA^L) evolved from an effort to define IBM's Systems Network Archi tecture (SNA) formal ly [SRWG80], It augments PL/1 with capabil it ies for representing state models. The subset of PL/1 used includes the statements: ASSIGN, C A L L , D E C L A R E , DO, E N D , P R O C E D U R E , R E T U R N , . I F - T H E N - E L S E , and S E L E C T groups. In addition to the standard PL/1 data types, the basic data-element construct in F A P L is the "entity" . Entit ies (and their data fields) are defined using ENTITY statements. Subsequently, entities may be C R E A T E d and D ISCARDed dynamical ly . Typical 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 NEWLIST, D E S T R O Y , INSERT and R E M O V E . A particular type of l i s t , a data queue, may contain only one entity type. INSERTing (REMOVEing) an entity to (from) a data queue corresponds to queuing (dequeuing) an i tem with a specif ied pr ior i ty . The overall protocol (SNA) structure is successively refined into "basic" f inite state automata (referred to in F A P L as FSMs). An FSM is defined using a state transition matr ix . Each state name has a corresponding state number. Columns of the matr ix are identi f ied by state name and number pairs. Input conditions (abbreviated) are contained in the row headings. Input (and output) codes referenced within the matr ix are defined outside the matr i x . . A ce l l in the matr ix 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. An F S M described using such a matr ix may be referenced by - 2 8 -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 ( FSM_fsmname[(fsm_input)] ) T H E N . . . The latter "checking" F S M reference does not cause a state transit ion or output action to be executed except when the selected next state indicator is ">"- It is used for screening out error conditions before committ ing to a state change. Typical ly , checking references of "a l l appl icable" FSM's always precede "normal" type references. FSM's may also be referred to by generic names. F A P L specif ications are translated by a preprocessor into PL/1 programs. Each FSM matrix becomes a . P L / 1 procedure. A lso , there is a validation system developed which is applied to the data flow control layer of SNA defined in F A P L . F SM_ I N P U T D E F I N I T I ON: /* s y m b o l s u s e d i n t h e " i n p u t s " c o l u m n o f t h e s t a t e t r a n s i t i o n m a t r i x */ MESS F S M I N P U T = ' U S E R S E N D ' ; AO ACK = 0 ; A l - ACK = 1 ; SEQO SEQ = 0 ; SEQ1 . SEQ = 1 ; ERR BAD P A C K E T ; 1 T IMEOUT ' F S M I N P U T = ' T I M E O U T ' ; END F S M _ I N P U T _ D E F I N I T I O N ; F SM_ S ENDER: F S M D E F I N I T I O N CONTEXT (ABP) ; INPUTS STATE N A M E S - - - > | S E N D OI STATE NUMBERS ->1 01 1 WAITO | SEND1 02 | 03 I W A I T l I 04 MESS 12(SO ) 1 - | 4 ( S 1 ) 1 -AO 1 - 1 3 I - l - ( S l ) A l 1 - 1 -Cso) | - 1 1 ERR 1 - 1 - ( S O ) | - l - ( S l ) ' T IMEOUT ' 1 - 1 - ( S O ) | - l - ( S l ) - 2 9 -OUTPUT CODE\ FUNCTION SO I C A L L S E N 3 _ D A T A ( 0 ) ; / *s e nd d a t a O * / . SI C A L L S E N D _ D A T A ( 1 ) ; / * s e n d d a t a l * / END F S M _ S E N D E R ; F S M _ R E C E I V E R : F S M - D E F I N I T I O N CONTEXT(ABP) ; INPUTS STATE N A M E S - - - > I D A T A O I D A T A 1 STATE N U M B E R S - > | 01 | 02 SEQO | 2 ( C 0 ) | - ( R 0 ) SEQ1 l - ( R l ) I K C l ) ERR | - ( R 1 ) | - ( R 0 ) ' T IMEOUT ' | - ( R 1 ) | - ( R 0 ) OUTPUT CODE FUNCTION RO 1 C A L L S E N D _ A C K ( 0 ) ; / * r e t r a n s m i t a c k O * / R I I C A L L S E N D _ A C K ( 1 ) ; / * r e t r a n s m i t a c k l * / CO 1 C A L L CONSLME_DATA ; C A L L S E N D _ A C K ( 0 ) ; C I 1 C A L L CONSUME_DATA; C A L L S E N D _ A C K ( 1 ) ; END F S M _ R E C E I V E R ; Figure 9. F A P L FSM's for the Al ternat ing Bi t Protocol - 3 0 -B. Specification Technique for Protocols The "specif icat ion technique for protocols" is a formal ism introduced by Blumer and Tenney [BlBu82,BlTe82,TeB181]., The speci f icat ion technique is a transit ion model augmented with . Pasca l . Pascal CONST and T Y P E declarations are avai lable. In addition, (user, lower layer and system) interface events are included in the data declaration sect ion. Implementation dependent functions may be declared as "pr imit ive"s to denote that they wi l l only be described functionally and not defined expl ic i t ly within the spec i f icat ion . The bulk of the speci f icat ion is the state transit ions. Each transit ion is modelled expl ic i t ly and independently (of other transitions). A state transit ion is character ized by a current state, a resultant state, an enabling condition (event and possibly predicates), program segment and transition pr ior i ty : < d e s t > < - - (p ) < o r i g i n > [ f r o m I : E V E N T . t y p e ] ( p r e d ) b e g i n t r a n s i t i o n _ a c t i o n _ r o u t i n e ; e n d ; As evident here, a transition statement resembles a regular (type 3) grammar production rule. Interpretation of such a rule is straightforward: the FSM 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, wi l l execute the transit ion_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 pr ior i ty . Note that enabling predicates are not to have side effects on the machine variables for obvious reasons. Throughout the spec i f icat ion , square brackets ([]) enclose interactions with the various interfaces. Each interface is identif ied by a single capita l letter (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, indicat ion, - 3 1 -response or conf i rm. Thus, [ t o I : E V E N T . t y p e ( a r g l := v a i l , a r g 2 := v a l 2 ) ] initiates an event of the specif ied type at the interface I; while [from I:EVENT.type] signals the occurrence of an event of the specif ied type at the interface I. Arguments passed by the in i t iator may be accessed by the acceptor . e g . c a 1 1 e d _ a d d r e s s := [ f r o m U : C a 1 1 e d _ a d d r e s s ] ; Program segments may contain any of the " b r a c k e f e d constructs intermixed with pascal assignments, repetit ion statements, conditionals and procedure and function cal ls . Since the transitions are defined separately, the speci f icat ion serves as a useful document for quick look-ups s imi lar 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 wel l as the NBS (basic and extended) transport layer protocols have been specif ied using this scheme [NBS83a,NBS83b,NBS81a,NBS81b]. (The authors c la im that approximately 40 percent of the entire implementation may be automatical ly produced.) This specif icat ion technique and its application to a session protocol is discussed further in the fol lowing chapter. {Transitions - module acts as both sender and receiver} <ACK_WAIT> <-- <ESTAB> [from U:SEND.request] begin p.msgdata : - [from U:UData] ; p.msgseq := send_seq; store(send_buffer,p); [to N:DATA.request (NData : = net_data(DATA, 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^ := net_data(DATA, p.msgseq, p.msgdata)]; [to S:TIMER.request(Name := retran_data, - 3 2 -Time := retran_time)]; end; <ESTAB> <-- <ACK_WAIT> [from N:DATA. ind icat ion] ([from N:NData. id] = A C K and [from N:NData.seq = 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 NrDATA. ind icat ion] ([from N:NData. id] = D A T A ) begin {always A C K data; store if expected sequence number} q.msgdata := [from N:NData.data] ; q.msgseq := [from N:NData.seq]; [to N:DATA.request (NData := net_data(ACK, 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:DATA.request (NData := net_data(AC.K> q.msgseq, null)]; [to S:TIMER.request(Name := retran_ack, _Time := retran_time)] ; end; <same_state> <— <either> [from U:RECEIVE.request] (not buffer_empty(recv_buffer)) begin q := retrieve(recv_buffer) ; [to U :RECEIVE. indicat ion(UData := q.msgdata)]; remove(rec.v_buffer, q.msgseq); end; Figure 10. ABP State Transitions - Blumer and Tenney Method - 3 3 -C. FDT and PDIL The Formal Descript ion Technique (FDT) is an extended state transition model f i rst 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 Pascal , in some aspects s imi lar to the method proposed by Blumer and Tenney. However, FDT appears to produce a more integrated program-l ike spec i f icat ion . In FDT , there is a concept of "channels" signifying interactions between modules within an environment. A specif icat ion of a module's channel lists all the feasible interact ion primit ives which may occur over the channel. Pr imit ives are classif ied 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 fol lowed by possible primitives in i t iated by the provider. The channel definitions in F D T is analogous to the " inter face" declarations in the method by Blumer and Tenney above. Service specif ications in FDT are defined using these channel or access point pr imit ive enumerations. The (internal) protocol specif icat ion contains further channel definitions for interactions with the lower layer as wel l as with the system environment. The actions taken by an entity module is according to transitions of an F S A . Transitions are specif ied by transit ion types which have the fol lowing fo rm: 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 > B E G I N « • * E N D ; The F R O M (present state), W H E N (input) and PROVIDED (enabling predicate) clauses make up the enabling condition portion of a transit ion type. The TO (destination state) clause and BEGIN . . .END (action) program segment define the operation of the - 3 4 -t rans i t ion—Each F R O M clause may have more than one W H E N , .PROVIDED, TO and BEGIN . . .END clauses associated with it„ For example, one may have the fol lowing hypothetical transition type def init ion: FROM s t a t e O WHEN e v e n t l TO s t a t e l ; WHEN e v e n t 2 PROVIDED p r e d 2 TO s t a t e 2 ; WHEN e v e n t 3 TO s t a t e 3 B E G I N ac t i on 3 ; E N D ; WHEN e v e n t 4 PROVIDED p r e d 4 TO s t a t e 4 B E G I N ac t i o n 4 ; E N D ; One advantage of this particular syntax is that " re lated" transitions may be grouped together. This allows specif ications 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 speci f icat ion technique based on (and very s imilar to) FDT is the Protocol Descript ion and Implementation Language (PDIL) f rom the RHIN project in France. It has provisions for protocol descriptions, service descriptions, implementation and simulat ion. A subset of the ISO session protocol has been 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 *) f rom ESTAB when PAR.SEND_request(UData) to A C K _ W A I T . begin send_msg.data:=UData; send_msg.seq:=send seq; SAP.BUFFER_storersend_buf , send_msg); NAP.DATA_request(net_data(DAT.A, sendjnsg .seq , send_msg.data)); SAP.TIMER_request(retran_data, retran_time); end; - 3 5 -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); NAP.DATA_request (net_data(DATA, send_msg.seq, send_msg.data)); SAP.TIMER_request(retran_data, retran_time); end; when NAP.DATA_ ind icat ion (NData) provided NData . id=ACK and NData.seq=send_seq to ESTAB begin . SAP.BUFFER_remove(send_buf, NData.seq) ; incr_send_seq; SAP.TIMER_cancel(retran_data) ; end; f rom ESTAB , A C K _ W A I T when NAP.DATA_ind icat ion(NData) provided NData . id=DATA to same begin recv_msg.data:=NData.data; recv_msg.seq:=NData.seq; NAP.DATA_request (net_data (ACK, recv jnsg . seq , null)); SAP.TIMER_request(retran_ack, retran_time); if NData.seq=recv_seq then begin SAP.BUFFER_store( recv_buf , rec.v_msg); incr_recv_seq; end end; when. SAP.TIMER_indicat ion(Name) provided Name=retran_ack to same begin recv_msg:=SAP.BUFFER^retr ieve(recv_buf) ; - NAP.DATA_request (net_data(ACK, recv_msg.seq, null)); SAP.TIMER_request(retran_ack, retran__time); end; when PAP.RECV_request ( ) provided not SAP.BUFFER_empty( recv_buf ) to same begin recv_msg:=SAP.BUFFER_retr ieve(recv_buf) ; PAP.RECV_ihdicat ion(recv_msg.data) ; SAP.BUFFER_remove(reev_buf , recv_msg.seq); end; Figure 11. F D T transitions of the ABP - 3 6 -D. A F F I R M A F F I R M is a system developed at USC-ISI for the speci f icat ion of abstract data types and ver i f icat ion of their properties [STEG82]. Since the system is based on transitions of abstract machines, it is suitable for defining communication protocols as we l l . Abstract data types and programs in A F F I R M are wri t ten in an extended variant of Pascal . A data type is specif ied 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 N E W S T A C K 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 which are "pr imit ive , unspecif ied" operations. The extenders and selectors are defined axiomatical ly with equations involving constructors. These equations are le f t - to - r ight rewrite rules which specify the ef fect of each function on each of the constructors. Service and protocol descriptions may be specif ied formal ly 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. Def in i t ion 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 some declarations fol lowed by axioms descriptions. A protocol speci f icat ion generally consists of several "type" definit ions. For example, the A F F I R M Alternat ing B i t Protocol representation consists of the type ABProtoco l plus auxi l iary types Message, Packet , Medium, Bit and QueueofPackets. Only the axioms of the ABProtoco l type is given in the fol lowing f igure. The complete representation is given in [STEG821 - 3 7 -Once a protocol has been speci f ied, the next step is to verify certain properties which it possesses. One aim is to show that the protocol speci f icat ion implements the services required (semantic properties). Correspondence between the two specif ications may be made by mapping the constructors and selectors of one onto the other. A protocol speci f icat ion is "accurate" if the axioms of the service speci f icat ion are "theorems" provable f rom axioms of the protocol spec i f icat ion . Properties (either semantic or syntact ic) to be shown are specif ied as theorems in A F F I R M and are proved by induction based on the constructors - structural induction. A "schema" outlining the appropriate induction approach accompanies each data type spec i f icat ion . A F F I R M does not search for or generate proofs of theorems by i tself . Instead, fac i l i t ies are available to a i d users in developing proofs interact ively : employ induction, spl it into subgoals, substitute equalit ies, and apply lemmas. Users direct their own proof strategies with A F F I R M carrying out the mechanics of the proofs. A favourable aspect of AFF IRM's abstract data type speci f icat ion is its high level of abstraction. For instance, actual implementation and size l imitat ions of queues and stacks are of no concern. A lso , the rewrit ing rule representation of axioms allow specif ications to be "walked through" to determine their accuracies. The main drawback with A F F I R M is that it is d i f f icu 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, Packet , QueueOfMessage, QueueOfPacket , Med ium, B i t ; • axioms Sent(ProtocolSend(p,m)) == if Pending(p) = NewQueueOfPacket then Sent(p). Add m else Sent(p), Sent( lnit ial izeProtocol) . == NewQueueOfMessage; axioms Received(Deliver(p)) == if ReceiverBuffer(p) = NewQueueOfPacket - 3 8 -then Received(p) else Received(p) Add Text(Frqnt(ReceiverBuffer(p))), Received(Init ial izeProtocol) == NewQueueOfMessage; axioms SenderToReceiver(ProtocolSend(p,m)) == if Pending(p) = NewQueueOfPacket 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(Init ial izeProtocol) == In i t ia l izeMedium; axioms SSN(ReceiveAck(p)) == if Seq(Front(ReceiverToSender(p))) = SSN(p) and ReceiverToSender(p) ~= Init ial izeMedium then ~SSN(p) else SSN(p), SSN(InitializeProtocol) == InitialSequenceNumber; axioms ReceiverToSender(ReceivePacket(p)) == if SenderToReceiver(p) ~= Ini t ia l izeMedium 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(Init ial izeProtocol) == In i t ia l izeMedium; axioms RSN(ReceivePacket(p)) == if Seq(Front(SenderToReceiver(p))) = RSN(p) and SenderToReceiver(p) ~= Init ial izeMedium then ~RSN(p) else RSN(p), RSN(Init ial izeProtocol) == Init ial izeSequenceNumber; axioms Receive Buff er(ReceivePacket(p)) == if Seq(Front(SenderToReceiver(p))) = RSN(p) and SenderToReceiver(p) ~= Init ial izeMedium then NewQueueOfPacket Add Front(SenderToReceiver(p)) else ReceiverBuffer(p) , ReceiveBuffer(Deliver(p)) == NewQueueOfPacket , ReceiveBuffer( Init ial izeProtocol) == NewQueueOfPacket ; - 3 9 -axioms Pending(ProtocolSend(p,m)) == if Pending(p) = NewQueueOfPacket then NewQueueOfPacket Add MakePacket (m, SSN(p)) else Pending(p), Pending(ReceiveAck(p)) == if Seq(Front(RecieverToSender(p))) = SSN(p) and ReceiverToSender(p) ~= Init ial izeMedium then NewQueueOfPacket else Pending(p), Pending(Init ial izeProtocol) == NewQueueOfPacket ; end {ABProtocol}; Figure 12. A F F I R M Axioms of the A B P (from [STEG82]) E. UNISPEX As we have seen, hybrid models are either directed towards automatic implementation or ver i f icat ion . It is desirable, however, to have an integrated system suitable for achieving both goals. One such system is UN ISPEX proposed by Vuong and Cowan. [VuCo82]. UNISPEX is an extended FSA model combining features of F D T (described earlier) and S P E X , a protocol speci f icat ion language aimed at fac i l i ta t ing verif ications [Schw81]. Protocol specif icat ion in UNISPEX 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 speci f icat ion include declarations and definitions - 4 0 -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 ia these external variables that the protocol machines exchange data and coordinate their act iv i t ies (see below). (State variables carry only local information). Interfaces to the upper and lower layers are defined by service primitives and mapping events (plus primitives), respectively . User service requests (network interactions) cause changes in interface (channel) variables and at the same t ime triggers occurrences of events. Event definitions capture the behaviour of the protocol machine in response to interact ion 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 fo rm: <name> / <code> / < o r i g i n > -> < d e s t > : when ( <pred> ) [ e f f e c t ] When an event, either message transmission/reception or t imeout , denoted by <code> c occurs, and the precondition <pred> holds, a state transit ion f rom <origin> to <dest> takes place. In addit ion, the program segment [effect] 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 using the V A R construct in Pascal . (The protocol machine part is analogous to Pascal T Y P E definitions). Interconnection of instances, either across layer or protocol machine boundaries, are specif ied using relations involving external variables. The properties part allows properties concerning the instances of protocol machines to be described. Both local (concerning a single protocol machine) and global (concerning the entire layer) invariants may be asserted. - 4 1 -Validation of the syntact ic properties of a protocol defined in UN ISPEX is achieved via reachabil i ty analysis and decomposition of its underlying F S A . This is., achieved by, f i rs t , translating a UNISPEX specif icat ion into FSA's and subsequently applying existing FSA 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 speci f icat ion is transformed into an "algebraic" data type speci f icat ion which can then be fed to a ver i f icat ion system such as A F F I R M . The rules for carry ing out such a transformation is yet to be defined. Events [ SendData / -DATA/ ESTAB — > 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 ; ] ReceiveData /+DATA/ ESTAB — > ESTAB1 or A C K _ W A I T — > A C K _ W A I T 1 when (InReq=DATA and SR=VR) [ Received:=Add(Received, MsgReceived) ; InChannel:=Remove(InChannel); RecvBuf:=Add(RecvBuf, MsgReceived) ; VR:=Increment(VR); ] ReceiveDupl icate /+DATA/ ESTAB — > ESTAB1 or A C K _ W A I T — > A C K _ W A I T 1 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 / ESTAB1 — > ESTAB or A C K WAIT ! — > A C K WAIT - 4 2 -When (OutReq=null and InReq=DATA) [ SS:=SR; MsgToSend:=empty; OutReq :=ACK; InReq:=null; ] ReceiveAck /+ACK/ A C K _ W A I T — > ESTAB When (InReq=ACK and SR=VS) [ VS:=Increment(VS); Pending :=false; SendBuf:=Remove(SendBuf); InReq:=null; ] Del iverData /null/ A N Y — > S A M E When (Cmd=receive and RecvBuf!=empty) [ MsgToDeliver:=Remove(RecvBuf) ; Cmd:=null ; ] ] T O P O L O G Y [ Instances Station : Array(Side) of ABStat ion Connections Station(i).OutReq <—> Station(OppSideG)). InReq Station(i).OutChannel <—>Station(Oppside(i)),InChannel; ] Figure 13. Events and Topology of the ABP U N I S P E X i f i c a t i o n - 4 3 -Chapter VI Formal Specification of the ISO Session Protocol This chapter reports on a formal specif icat ion of the ISO session level protocol . The session protocol standard is a set of procedures designed to fac i l i ta te dialogue management, document transfer and data f low synchronization and resynchronization between user entities [IS083s]. In the context of the ISO Reference Model [IS082], the session layer provides these services to presentation layer entit ies by interact ing with transport layer entit ies. 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 rel iable bulk data transfer service, respectively . • The speci f icat ion technique employed to define the ISO session protocol formal ly 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 f irst give an overview of the services provided by the session protocol . Next , we describe the formal ism to be used to define i t . F inal ly , - .we discuss experiences with specif icat ion of the session protocol . We present the formal specif icat ion of the session protocol using the technique described as the appendix to this thesis. - 4 4 -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 wi 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 and funct ional i t ies . Transport addresses are obtained from the session addresses supplied by the users. Cooperating users may identify " log ica l " session connections which may span one or more "physical" session connections. Users may also exchange a l imi ted 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 fa i r ly straightforward concepts such as segmentation and reassembly of user data units, concatenation of certa in protocol data units and expedited data transfer for conveying "out of band" data. Other concepts require more detailed explanations. Tokens are a means of control l ing rights of the users to invoke certain 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 token) and major synchronization and - 4 5 -act iv i ty management (major synchronization/activity token), (see below) Except for the data token, presence of a token implies avai labi l i ty of the associated serv ice. 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 imi ted amount of data is possible without the data token via the " typed-data" pr imit ive . For duplex connections, either side may transmit data at any t ime. During a session, a token may be dynamically reassigned to either users (at the discretion of the owner of the token). However, avai labi l i ty of a token is stat ic (determined at session connection t ime). Communicat ion between session users may be synchronized by expl ic i t definit ion of synchronization points. Each synchronization point is identi f ied by an automatical ly incremented synchronization ser ia 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 rom al l communication before and after i t " — whereas minor synchronization points are used to mark the data s t ream. Major synchronzati ion 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 ent i t ies. Pr imit ives 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 act iv i t ies — " log ica l " units of work which may span one or more session connections. There may only be one current act iv i ty on a session connection. Avai labi l i ty (and use) of act iv i ty management is determined by the major synchronize/activity token. If act iv i ty management is available, normal data must be exchanged within an act iv i t y . A l imited - 4 6 -amount of data may be passed outside an act iv i ty using the capabi l i ty data feature. There are mechanisms for start ing, ending, interrupting, resuming and cancel l ing an act iv i t y . The synchronization ser ial number is reset to 1 at the start of an act iv i ty and is automatical ly incremented at the end of the an act iv i ty . Other major synchronization points may be established between the start and end of an act iv i t y . The serial number is set to the user supplied value at resumption of an act iv i t y . As mentioned above, the service provider does not associate any semantics with the ser ia l numbers. Connection Release Phase If the release token is available, its owner has the authority to init iate 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, i rrespective of the placement of the release and data tokens, destructively terminate a session connection by means of the abort pr imit ive . The connection may also be aborted by the provider upon encountering irrecoverable protocol errors or loss of the transport connection. Protocol Subsets The definit ion of different subsets within the protocol standard is designed to "achieve s impl i f i cat ion , yet to provide a variety of capabi l i t ies, for different applications" [IS083s]. There are thre service subsets in the session standard: Basic Combined ...Subset (BCS), Basic -Synchronized, Subset (BS) and Basic Ac 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 rel iable transport service from the lower layer . - 4 7 -The BCS provides the minimal session services. Connections may be either half duplex 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 for structuring and resynchronizing the data s t ream. Half duplex and optionally duplex connections are supported. Mandatory functional i t ies include typed data, negotiated release, minor and major synchronization, resynchronization and token management. The synchronize minor, synchronize major/activ ity , release and possibly data tokens are avai lable. The underlying transport service must support expedited data transfer which the session provider uses to achieve reliable resynchronization with the peer session machine. The BAS provides a rel iable bulk data transfer serv ice . As for BS, half duplex and optionally duplex connections are supported. Ac t i v i t y management, capabi l i ty data exchange, major and minor synchronization, token management and exception reports are mandatory functional i t ies of this subset. Optional features include typed data transfer and resynchronization. The underlying transport 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 f inite state machine (FSM) augmented with program segments. An FSM is assumed to have three passive . - 4 8 -interfaces: the upper layer (users), lower layer and local system environment. These interfaces are passive in the sense that the means of associating in i t iat ion of an event with its reception by another entity as well as the delay between the instance a protocol entity init iates an event and when it is noticed are unspecif ied. There is a set of well defined events at each interface corresponding to service primit ives provided at the inter face. Output parameter(s) specif ied by the in i t iator of an event become the input parameter(s) available to the receipient . It is this abstract model of a protocol machine on which the speci f icat ion language is based. A formal speci f icat ion consists of several parts: data declarat ion, state def ini t ion, declaration of procedures and pr imit ives, in i t ia l i zat ion of variables, definit ion of procedures, description of pr imit ives, state transitions and description of header formats . Except for descriptions of the pr imit ive operations and header formats which are expressed in natural language, the other sections of the definit ion are formulated using an extended speci f icat ion language based on Pascal . Data declarations include definit ion (using Pascal constructs) of constants, types, structure of data objects, and declaration of variables. Each speci f icat ion contains definit ion of a record type whose fields are the " local variables" of the F S M and declaration of a variable to be of this type (eg. ca l l this variable Ecs). Statements in the program segments have impl ic i t "with Ecs do" prepended to them. Also, as part of the data declarations, there are expl ic i t definitions of the interface events. Each such event is described by the name of its associated service pr imit ive , parameter(s) and default value(s) (if any) for the parameter(s). (Parameters with default values are optional parameters). e g . i n t e r f a c e [ t o T : T _ D I S O O N N E C T . i n d i c a t i o n ( R e a s o n : r e a s o n ^ t y p e ; U s e r d a t a : d a t a t y p e d e f a u l t NULL State abbreviations are s imilar to declaration of sets or constants. They merely -49-provide pseudonyms for groups of states. There must be declarations of initial and final states. An FSM starts off at the in i t ia l state and ceases to exist when it reaches the f inal state. Any intermediate feasible state must appear in one or more abbreviations. The special abbreviation "same_state" need not be declared and may be used in state transitions to indicate that the F S M remains in the same s tate . A l l procedures (and functions) appearing in the specif icat ion must be declared. These are normal Pascal procedure and function declarations except that in addition to "forward", they may be designated "pr imi t ive" to denote that they wi l l only be described functionally and not defined expl ic i t ly within the spec i f icat ion . It should be noted here that the data and procedure declarations serve only to make the specif icat ion complete. 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 init ial izes the variables of a new F S M . Other procedures (and functions) defined are those which do not introduce implementation dependencies or restr ict ions. Procedures not sat isfy ing this cr i ter ion are termed "pr imit ives" and are defined descriptively to preserve the abstract nature of the speci f icat ion approach. The bulk of the specif icat ion is the state transit ions. Each state transit ion is character ized by a current state, a resultant state, an enabling condition (event and possibly predicates), program segment and transit ion prior ity : < d e s t > < - - ( p ) < o r i g i n > [ f r o m I : E V E N T . t y p e ] ( p r e d ) b e g i n t r a n s i t i o n _ a c t i o n _ r o u t i n e ; e n d ; As evident here, a transition statement resembles a regular (type 3) grammar production rule. Interpretation of such a rule is straightforward: the FSM at state origin (either a single state or a state abbreviation), upon occurrence of an event at - 5 0 -interface I, if the enabling predicate pred holds, wi l l execute the transit ion_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 pr ior i ty . Note that enabling predicates are not to have side effects on the machine variables for obvious reasons. Throughout the spec i f icat ion , square brackets ([]) enclose interactions (not necessarily events) with the interfaces. Each interface is identif ied by a single capita l let ter (eg. U for User , S for_ System and T for Transport service). EVENT 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, indicat ion, response or conf i rm. Thus, [ t o I : E V E N T . t y p e ( a r g l := v a i l , a r g 2 := v a l 2 ) ] initiates an event of the specif ied type at the interface I; while [from I :EVENT.type] signals the occurrence of an event of the specif ied type at the interface I. Arguments passed by the in i t iator may be accessed by the acceptor. e g . c a 1 1 e d _ a d d r e s s := [ f r o m U : C a 1 1 e d _ a d d r e s s ] ; Program segments may contain any of the " b r a c k e f e d constructs intermixed with pascal assignments, repetit ion statements, conditionals and procedure and function cal ls . . C. Specification of the Session Protocol The accompanying speci f icat ion is that of the BCS and BAS subsets. A l l definit ion sections mentioned above except for description of header formats (see [IS083p] for details) are included. In a general sense, the speci f icat ion is a translation of the state tables provided in the annex of [IS083p] enhanced with details extracted f rom the - 5 1 -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 direct ly from the descriptions (eg. those concerning interrupting or discarding act iv i t ies) . In addition to the "kernel" functions (connection establishment, normal data transfer, connection release, and abort) the fol lowing function groups are supported: negotiated release (for BCS), major and minor synchronization, typed data, capabi l i ty data, exception report, act iv i ty management and token management. The functions omitted are resynchronization and expedited data transfer. In addit ion, 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 spec i f icat ion . Moreover, "category 2" commands (synchronization, act iv i ty , capabil i ty data and typed data commands) are depicted as if they were "category 1" commands; that is, an SPDU containing a category 2 command is identif ied by the imbedded category 2 command; that is , the category 1 command which precedes it in the SPDU is ignored. The routines handling the reception and transmission of SPDU's are assumed to hide the distinction from the speci f icat ion . Most of the above omitted functions could have been included and assumptions deemed unnecessary; however the specif icat ion stands as it is due to a number of factors . The decision to make al l 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 speci f icat ion choices. Concatenation and fragmentation are really local implementation decisions. Including provisions for these would complicate the reception and transmission of - 5 2 -SPDU's. Furthermore, the routines associated with handling these options would have been specif ied as primit ives 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 definit ion 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 speci f icat ion is the " inef f ic ient" manner which the speci f icat ion technique allows it to be defined. Reuse of transport connection applies to not only abort but also normal release as wel l as refusal of a session connection. For each transit ion going to an unconnected session state, there would have to be three state transitions (to tc_unconnected, tc_reuse_init iator or tc_reuse_acceptor states), each dif fer ing only in the resultant state and some details such as issuing disconnect requests to the transport server or start ing t imers, etc . This is a consequence of the restr ict ion 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 state . 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 BAS . This appears contradictory with respect to the act iv i ty management description. In the ISO document, arr ival of expedited data is queued when there is no act iv i ty in progress and dequeued once an act iv i ty is started (or resumed). It is not clear why this detail is included when one cannot even use the expedited data option with BAS and no other subset has act iv i ty management capabi l i t ies . Other contradictions and ambiguities exist between the verbal descriptions and state table definitions in the document (especially pertaining to the avai labi l i ty of minor synchronization and data tokens and status of an act iv i ty ) . The reason for these inconsistencies, as mentioned, - 5 3 -could be due to the fact that the document is only an early draft proposal. - 5 4 -Chapter VII Conclusions As we have seen, many diversed techniques are available for formal ly defining communication protocols. The technique chosen to specify a particular protocol depends on the complexity of the protocol and the intended use(s) of the speci f icat ion (whether for implementation or ver i f icat ion purposes). FSA and petri nets are useful for representing simple protocols. Such representations are easily understood and fac i l i ta te analysis of the protocols. Automated analysis techniques based on transition models have been developed [ACDi82] , These models, however, are quite l imited in their abi l i ty to handle more complex protocols. The number of states (or places) and transitions become unmanageably large very quickly. High level programming languages and f lowcharts , on the other hand, are quite adequate in ful ly capturing the details of complex protocols. Furthermore, depending on the target implementation language, such a speci f icat ion may also serve as a natural implementation model . The major drawbacks of these techniques are the lack of abstraction and d i f f icu l ty in ver i f i cat ion . The buffer history approach attempt to ease the latter by allowing invariants to be stated on the input/output behaviour of communicating processes. However, the only ver i f icat ion methods available for other program models are assertion and temporal logic techniques developed for proving correctness of programs. . Extensions to transition and program definit ion techniques attempt to increase - 5 5 -their appl icabi l i ty of " rea l " protocols. Usually these extensions result in hybrid models which have means to express both the control and data f low aspects of protocols. Several specif icat ion languages based on the hybrid approach have emerged. Some are oriented towards automatic implementation (FDT, PDIL , F A P L ) while others are aimed at mechanical ver i f icat ion (AFFIRM) and s t i l l others sought to provide integrated implementation and ver i f icat ion fac i l i t ies for protocols (UNISPEX). Although analysing hybrid models is not as straightforward as analysing transit ion models (due to the additional program elements), the expl ic i t states in both allow one to fol low the logic of a protocol's control structure quite easi ly . This is an advantage over pure program models. Of course the program elements of hybrid models provide the expressive power lacking in basic transit ion techniques. Due to the complexity of most protocols, it appears that hybrid approaches are the most suitable (of the three) in formal ly specifying communication protocols. The hybrid speci f icat ion technique by Blumer and Tenney offers a straightforward method of representing the actions and transitions of high level protocols. Both control and data f low aspects are captured. Its major advantages over state transit ion diagrams and tables are its expressibil ity and c la r i t y . Although the other two approaches offer "graphical" representation, they become cluttered and d i f f icu l t to fol low when protocols of the complexity of most high level protocols are to be modelled entirely . Designers would no doubt be able to define a protocol more concisely and completely using a tool such as this than to rely on ad hoc methods. Moreover, the speci f icat ion produced is in machine-readable form (and in fac t , may be used as input to automated implementation generators or path finding programs [BlBu82,BlTe82]). There are, nevertheless, some awkwardness in specify ing 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 - 5 6 -ISO FDT description technique [BoRa82]). - 5 7 -BIBL IOGRAPHY [ A C N R 8 3 ] J . P . Ansart , V. C h a r i , M . Neyer , O. R a f i q , D. Simon, "Descr ipt ion, Simulation and Implementation of Communicat ion Protocols using PDIL" , Proceedings of the A C M S IGCOMM Conference, p l l 2 - 1 2 0 , Mar 1983. [ARCh82] J . P . Ansart , O. R a f i q , V. C h a r i , "Protocol Description and Implementation Language", Protocol Specif icat ion, Testing, and Ver i f icat ion , C.Sunshine (ed.), North-Hol land Pub. C o . , p l O l - 1 1 2 , .IFIP, 1982. [ACDi82] J . M . Ayache, J . P . Cour t ia t , M . D i a z , "The Design and Validation by Petr i Nets of a Rel iable Bus A l locat ion Protoco l " , IEEE C H , p221-228, 1982. [Bil l82] J . Bi l l ington, "Specif icat ion of the Transport Service using Numer ica l Pet r i Nets" , Protocol . Specif icat ion, Testing, and Ver i f i cat ion , C.Sunshine (ed.), North-Hol land Pub. C o . , p77-100, IFIP, 1982. [BlBu82] T .P . Blumer, J . C . Burrus, "Generating a Service Specif ication of a Connection Management Protoco l " , Protocol Specif icat ion, Testing, and Ver i f icat ion , C.Sunshine (ed.), North-Hol land . Pub Co . , p l 6 1 - 1 7 0 . IFIP, 1982. [BlTe82] T .P . Blumer, R . L . Tenney, " A Formal Specif ication Technique and Implementation Method for Protocols" , Computer Networks, VOL 6, p201-217, 1982. [Boch78] G.V. Bochmann, "F in i te State Descript ion of Communicat ion Protocols" , Computer Networks, V O L . 2 , p361-372, 1978. [Boch80] G.V. Bochmann, " A General Transition Model for Protocols and Communicat ion Services", IEEE Transactions on Communicat ions, VOL C O M - 2 8 , NO 4, p643-650, Apr 1980. [BoRa82] G.V. Bochmann, K.S. Raghunathan, "Example Descript ion of the Transport Service", Contr ibution to the meeting (July 1982) of the Subgroup B of the ISO TC97/SC16/WG1 ad hoc group on FDT , Jun 1982. [BoSu80] G.V. Bochmann, C . A . Sunshine, "Formal Methods in Communicat ion Protocol Design", IEEE Transactions on Communicat ions, VOL C O M - 2 8 , NO 4, p624-631, Apr 1980. [BCGJ82] G.V. Bochmann, E. Cerny , M . Gagne, C . Jard, A . Leve i l le , C . Laca i l le , M . Maksud, K .S . Raghunathan, B. Sarikaya, "Some Experience with the Use of Formal Specif ications", Protocol Speci f icat ion, Testing, and Ver i f i cat ion , C.Sunshine (ed.), North-Hol land Pub. C o . , p l 7 1 - 1 8 5 , IFIP, 1982. - 5 8 -[Dant80] A . Danthine, "Protocol Representation with F in i te -State Models" , IEEE Transactions on Communicat ions, VOL C O M - 2 8 , NO 4, Apr 1980. [DaBr78] A . Danthine, J . Bremer, "Model l ing and Ver i f icat ion of End- to -End Transport Protocols" , Computer Networks, VOL 2, p381-395, 1978. [Diaz82] M . D i a z , "Modeling and Analysis of Communicat ion and Cooperation Protocols Using Pet r i Net Based Models", Computer Networks, VOL 6, p419-441, 1982. [Divi82] B.L. D iV i to , "Integrated Methods for Protocol Specif icat ion and Ver i f icat ion" , Protocol Specif icat ion, Testing, and Ver i f i cat ion , C.Sunshine (ed.), North -Hol land. Pub. C o . , p411-433, IFIP, 1982. [Good77] D. Good, "Construct ing Verif ied and Rel iable Communications Procesing Systems", A C M Software Engineering Notes, VOL- 2(5), Oct 1977. [GoCo78] D. G o o d , - R . M . Cohen, "Ver i f iable Communicat ion Processing in Gypsy", Proceedings of the 17th IEEE Computer Society International Conference ( C O M P C O N ) , p28-35, Sep 1978. [GoMa78] M . G . Gouda, .E . Manning, "How to Describe Protocols" , Universi ty of Waterloo C C N G E-Report E -76, Mar 1978. [IS081] International Organization for Standardization? " A FDT based on an Extended State Transition Model" Working D r a f t , Boston, Dec 1981. [IS082] International Organization for Standardization, "Reference Model of Open System Interconnection", ISO/TC97/SC16, Dra f t ISO/DIS 7498, 1982. [IS083p] International Organization for Standardization, "Basic Connection Oriented Session Protocol Speci f icat ion" , ISO/TC97/SC16/WG6, D r a f t , Mar 1983. [IS083s] International Organization for Standardization, "Basic Connection Oriented Session Service Def in i t ion" , ISO/TC97/SC16/WG6, Dra f t , Mar 1983. [JuVu84] W. Jurgensen, S.T. Vuong, " C S P and C S P Nets: A Dual Model for Protoco l - Specif ication and Ver i f icat ion" , to be published in Proceedings of the Fourth International Workshop on Protocol Speci f icat ion, Testing and Ver i f i cat ion , Jun 1984. [NBS81a] "Specif icat ion of the Transport Protoco l , Volume 2: Basic Class Protoco l " , Report No ICST/HLNP81-12, Nat ional Bureau of Standards, 1981. [NBS81b] "Specif icat ion of the Transport Protoco l , Volume 3: Extended Class Protoco l " , Report No ICST/HLNP81-13, Nat ional Bureau of Standards, 1981. - 5 9 -[NBS83a] "Specif icat ion of a Transport Protocol for Computer Communicat ions, Volume 2: Class 2 Protocol" , Report No ICST/HLNP81-12, National Bureau of Standards, 1983. [NBS83b] "Specif icat ion of a Transport Protocol for Computer Communicat ions, Volume 3: Class 4 Protoco l " , Report No ICST/HLNP81-12, Nat ional Bureau of Standards, 1983. [RWZa78] H. Rudin, C . H . West, P. Zafiropulo, "Automated Protocol Val idat ion: One Chain of Development", Computer Networks, V O L 2 , p373-380, 1978. [Schi80] S.. Schindler, "Algebraic and Model Specif ication Techniques", Proceedings of the 13th Hawai i International Conference o n . System Sciences, Jan 1980. [Schw81] D . . Schwabe, "Formal Specif icat ion and Ver i f icat ion of a Connection Establishment Protoco l " , Proceedings of the Seventh Data Communications Symposium, Mexico C i t y , Oct 1981. [Sidh81] D.P. . Sidhu, "Toward Construct ing Verifiable^ Communicat ion Protocols" , Protocol Testing - Towards Proof? , INWG/NPL Workshop Proceedings, National Physical Laboratory, Teddington, U .K . , VOL 1, p75-141, May 1981. [SiKa82] G . A . Simon, D . J . . Kaufman, "An Extended Finite State Machine Approach to Protocol . .Specif ication", Protocol .Spec i f icat ion , Testing, and Ver i f icat ion , C.Sunshine (ed.), North-Hol land Pub. C o . , p l l 3 - 1 3 3 , IFIP, 1982. [Suns78] C A . - Sunshine, "Survey of Protocol Def ini t ion and Techniques", Computer Networks, VOL 2, p346-350, 1978. Ver i f icat ion [Suns79] C A . Sunshine, "Formal Techniques for Ver i f icat ion" , IEEE Computer , Aug 1979. Protocol Specif icat ion and [Suns81] C A . . Sunshine, "Formal Modeling of Communicat ion Protocols" , University of Southern Ca l i fo rn ia ISI R R - 8 1 - 8 9 , Mar 1981. [SRWG80] G .D . Schultz, D .B. Rose, C . H . West, J . P . Gray , "Executable Descript ion and Validation of SNA" , IEEE Transactions on Communicat ions, VOL C O M - 2 8 , NO 4, p661-676, Apr 1980. [STEG82] C A . Sunshine, D .H . Thompson, R.W. Er ickson, S.L . Gerhart , D. Schwabe, ' 'Specif ication and Ver i f icat ion of Communicat ion Protocols in A F F I R M using .State Transition Models" , IEEE Transactions on Software Engineering, VOL SE-8 , NO 5, p460-489, Sep 1982. [TeB181] R. Tenney , T. Blumer, "An automated Formal Specif icat ion Technique for Protocols" , Report No ICST/HLNP-81 -15 , Nat ional Bureau of Standards, 1981. - 6 0 -. . [VuCo82]. S.T. Vuong, D.D. Cowan, "UNISPEX - A Unif ied Model for Protocol Specif icat ion and Ver i f icat ion" , University of Waterloo Technical Report C S - 8 2 - 5 2 , Nov 1982. . - [Wats82] R.W. Watson, "An Experience in Transport Protocol Specif icat ion using an Algor i thmic Programming Language", Protocol Specif icat ion, Test ing; and Ver i f icat ion , C.Sunshine (ed.), North-Hol land Pub. Co . , p237-247, IFIP, 1982. - 6 1 -APPENDIX - Specification of the ISO Session Protocol { constant declarations } const VERSION = 1; { protocol version number } M A X _ C N _ D A T A _ S I Z E = 64; M A X _ A C _ D A T A _ S I Z E = 64; M A X _ R F_D A T A_SI ZE = 64; M A X _ F N _ D A T A _ S I Z E = 32; M A X D N DATA_SIZE = 32; max size of user data f ie ld in C N max size of user data f ie ld in A C max size of user data f ie ld in R F max size of user data f ie ld in F N __ .__ . . . . , max size of user data f ie ld in D N } M A X J \ I F _ D A T A _ S I Z E =. 32; f max size of user data f ie ld in N F } M A X . AB D A T A SIZE = 3; { max size of user data f ie ld in A B } T R _ T O K E N = $01; { release token mask } M A _ T O K E N = $04; { major sync/activity token mask } SY T O K E N = $10; { minor sync token mask } D K _ T O K E N = $40; { data token mask } C L E A R _ T C = $00; { clear tc 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 act iv i ty f lag } E O A C T = $00; { end of act iv i ty f lag } EOSSDU. = $01; { mark end of SSDU f lag } C O N F I R M . = $01; { conf i rm required on minor sync fig} N O T _ C O N C A T = $00; { no concatenation of SPDU's f lag } C O N C A T = $01; { concatenation of SPDU's f lag }.. { session requirement masks } H D U P L E X = $0001;{ half duplex } D U P L E X = $0002;{ fu 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;{ act iv i ty management } N E G _ R E L E A S E = $0080;{ negotiated release } C A P = $0100;{ capabi l i ty 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 } INIT_SYNC_SERIAL"= D E F A U L T 2 ; { in i t ia l synchronize ser ial no (1) } T A B I N T E R V A L = D E F A U L T 3 ; { abort t imer interval } - 6 2 -{ 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 o f t y p e s } type subset_type - ( { subset of protocol } B A S I C _ C O M B I N E D , B A S I C _ S Y N C H R O N I Z E D , BASIC_ACTIVITY ); boolean = ( { boolean values } F A L S E , T R U E 0; result_type = ( { connect result reply codes } REASON_NOT_SPECIF IED , P R O T O C O L _ V E R S I O N _ U N K N O W N , S U B S E T _ N O T _ S U P P O R T E D , U N A C C E P T A B L E _ S E S S _ C O N _ P A R A M , A C C E P T O R _ A D D R _ I N V A L I D , U S E R _ R E J E C T , U S E R _ N O T _ C O N N E C T E D , A F F I R M A T I V E ); reason type = ( { reason for release of connection } N O _ S P E C I F I C _ R E A S O N , M E M O R Y _ O V E R F L O W , L O C A L J J S E R ^ E R R O R , S E Q U E N C E _ E R R O R , D E M A N D D A T A _ T O K E N , P R O T O C O L _ E R R O R , U N D E F I N E D , T C _ G O N E , T Y P E D D A T A ); timer_.type = ( { t imer types } TIN, T A B ); inact iv i ty } abort } token_type = ( { values taken by tokens } NOT_AV AIL A B L E , INITIATOR_SIDE, A C C E P T O R _ S I D E , C H O I C E ); - 6 3 -pdu_type = ( { types of SPDU's } C N , A C , R F , { connection } F N , D N , NF , A B , A A , {release/abort } PT , GT, 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 } RS, R A , { resync } AS, A R , A D , A D A , AI, ,AIA, { act iv i ty } C D , C D A, { capabil i ty } ER , ED { exceptions } ); act_type = ( { act iv i ty switch } N O T _ A V A I L A B L E , O N , O F F ); resync_type. = ( { resynchronization switch } N O T _ A V A I L A B L E , R E S T A R T , A B A N D O N , I N T E R R U P T , D I S C A R D ); act_begin type = ( { type of act iv i ty begin request } START , ~\ begin } C O N T I N U E ( resume } ); { implementation dependent types } addr_type { session addr: host + tc addr's } h_addr_type { host address type } tc_addr_type { tc address type } int_type { integer type - 16 bits} octet_type { byte - 8 bits } data_type { ptr to str ing } - 6 4 -sync_serial_type { synchronization ser ial number - 6 octets} 5 act_id_type { act iv i ty identif ier - 3 octets } 5 sess_id_type { session identif ier type - max 64 octets} 5 qos_type { quality of service } 5 Pdu = { possible fields in a SPDU } record pversion : octet_type; ptype : pdu_type; pinit iator_addr, pacceptor_addr : h_addr_type; ptoken : token_type; preason : reason_type; pno_reason_field : boolean; presult : result_type; p_options : octet_type; psess_req : int_type; pCN_ref : 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 CN_ref : int_type; { ref to local F S M structure } CN_or ig in : boolean; { in i t iator of connection } max _SPDU_in, { max sizes of SPDU's. } max_SPDU_out : int type; sess_req : int_type; •f session requirements } laddr, { local and foreign session } faddr : addr_type; { addresses } lhost, { l oca l and foreign host name} fhost : h_addr_type; l t c , { l oca l and foreign tc 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? } - 6 5 -ec_report, { exception report avai l? } ec_data, { exception data avai l ? } tc_expedited, { expedited transport service} session_expedited : boolean; { expedited session serv ice? } dk_token, { data token } t r_token, { release token } sy_token, { minor sync.token } ma_token : token_type; { major sync/activity token } protocol_opts : octet_type; { protocol options } sync_serial_confirmed, { last confirmed sync ser ia l } sync_serial : sync_serial_type; { current sync ser ial no } qos : qos_type; { quality of service } act iv i ty : act_type; { status of act iv i ty } resync : resync_type; { resynchronization type } sess_id : sess_id_type { session identif ier } end; declaration of interface events and associated parameters } — parameters with default value given are optional } { *********** System interface ************** } i n t e r f a c e [ t o S : T I M E R . r e q u e s t ( Name : t i m e r _ t y p e ; T i me : i n t _ t y p e ) ] ; i n t e r f a c e [ f r o m S : T I M E R . r e s p o n s e ( Name : t i m e r t y p e ) ] ; i n t e r f a c e [ t o S : T I M E R . c a n c e l ( Name : t i m e r _ t y p e ) ] ; | *********** T r a n s p o r t i n t e r f a c e * * * * * * * * * * * } i n t e r f a c e [ t o T : T _ C O N N E C T . r e q u e s t ( C a 1 1 e d _ a d d r es s , C a l 1 i n g _ a d d r e s s : t . c _ a d d r _ t y p e ; E x p _ d a t a _ o p t i o n : b o o l e a n d e f a u l t F A L S E ; Qua 1 _ o f _ s e r v i c e : q o s _ t y p e ; U s e r d a t a : 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 : T _ C O N N E C T . i n d i c a t i o n ( C a 1 1 e d _ a d d r e s s , C a 1 1 i n.g_addr es s : t c _ a d d r _ t y p e ; E x p _ d a t a _ o p t i o n : b o o l e a n ; Qua 1 _ o f _ s e r v i c e : q o s _ t y p e ; U s e r d a t a : d a t a _ t y p e d e f a u l t NULL ) ] ; - 6 6 -i n t e r f a c e [ t o T : T _ C O N \ I E C T . r e s p o n s e ( Qua 1 _ o f _ s e r v i c e : q o s _ t y p e ; Res pond i n g _ a d d r es s : t , c _ a d d r _ t y p e ; E x p _ d a t a _ o p t i o n : b o o l e a n ; U s e r _ d a t a : 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 : T _ C O N N E C T . c o n f i rm ( Q u a l _ 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 e s s : t c _ a d d r _ t y p e ; E x p _ d a t a _ o p t i o n : b o o l e a n ; U s e r d a t a : 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 [ t o T : T _ D A T A . r e q u e s t ( D a t a : d a t a t y p e ) ] ; i n t e r f a c e [ f r o m T : T _ D A T A . i n d i c a t i o n ( Spdu : Pdu ) ] ; i n t e r f a c e [ t o T : T _ E X P E D I T E D _ D A T A . r e q u e s t ( D a t a : d a t a _ t y p e ) ] ; i n t e r f a c e [ f r o m T : T _ E X P E D I T E D _ D A T A . i n d i c a t i o n ( . S p d u : Pdu ) ] ; i n t e r f a c e [ t o T : T _ D I S O O N N E C T . r e q u e s t ( U s e r _ d a t a : d a t a _ t y p e d e f a u l t N U L L ) ] ; i n t e r f a c e [ f r o m T : T _ D I S O O N N E C T . i h d i c a t i on ( R e a s o n : r e s u l t _ t y p e ; U s e r d a t a : 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 ********* } i n t e r f a c e [ f r om U : I d e n t i f i e r In i t i a t o r _ a d d r , A c c e p t o r _ a d d r Qua 1 _ o f _ s e r v Ses s i o n _ r e q , S y n c _ s e r i a 1 In i t _ d k _ t o k e n , I n i t _ t r _ t o k e h , I n i t _ s y _ t o k e n , I n i t _ m a _ t o k e n U s e r d a t a S _ C O N M E C T . r e q u e s t ( : s e s s _ i d _ t y p e ; a d d r _ t y p e ; q o s _ t y p e ; i n t _ t y p e ; s y n c _ s e r i a l _ t y p e d e f a u l t N U L L ; t o k e n _ t y p e d e f a u l t N O T _ A V A I L A B L E ; d a t a t y p e d e f a u l t N U L L - 6,7 -) ] ; i n t e r f a c e [ t o U : S C O N N E C T . i n d i c a t i o n ( I d e n t i f i e r I n i t i a t o r _ a d d r A c c e p t o r _ a d d r Q u a l _ o f _ s e r v S e s s i o n _ r e q S y n , c _ s e r i a 1 In i t _ d k _ t o k e n , I n i t _ t r _ t o k e n , In i t _ s y _ t o k e n , In i t _ m a _ t o k e n U s e r d a t a ) ] ; s es s _ i d _ t y p e ; a d d r _ t y p e ; q o s _ t y p e ; i n t _ t y p e ; s y n c _ s e r i a 1_t ype ; t o k e n _ t y p e ; 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 U : S _ C O N N E C T . r e s p o n s e ( I den t i f i A c c e p t o r R e s u l t Qua 1 _ o f _ S e s s i o n _ S y n , c _ s e r I n i t _ d k _ I n i t _ , t : r _ I n i t _ s y _ In i t _ m a _ U s e r d a t ) ] ; e r _ a d d r s e r v r e q i a l t o k e n , t o k e n , t o k e n , t o k e n a s es s _ i d_t y p e ; a d d r _ t y p e ; r e s u l t _ t y p e ; q o s _ t y p e ; i n t _ t y p e ; s y n , c _ s e r i a l _ t y p e ; t o k e n _ t y p e ; d a t a t y p e d e f a u l t N U L L i n t e r f a c e [ t o U : S C O N N E C T . c o n f i r m ( I d e n t i f i e r A c c e p t o r _ a d d r R e s u 1 t Q u a l _ o f _ s e r v S e s s i o n _ r e q S y n c _ s e r i a 1 In i t _ d k _ t o k e n , In i t _ t r _ t o k e n , I n i t _ s y _ t o k e n , In i t _ m a _ t o k e n U s e r d a t a ) ] ; " i n t e r f a c e [ f r o m U : U s e r d a t a ) ] ; " i n t e r f a c e [ t o U s e r d a t a ) ] ; U : S s es s _ i d_t y p e ; a d d r _ t y p e ; r e s u l t _ t y p e ; q o s _ t y p e ; i n t _ t y p e ; s y n c _ s e r i a l _ t y p e ; : t o k e n _ t y p e d e f a u l t N O T _ A V A I L A B L E ; : d a t a _ t y p e d e f a u l t NULL S _ R E L E A S E . r e q u e s t ( : d a t a t y p e d e f a u l t N U L L R E L E A S E . i n d i c a t i o n : d a t a _ t y p e i n t e r f a c e [ R e s u l t f r o m U : S _ R E L E A S E . r e s p o n s e ( : r e s u l t t y p e ; - 6 8 -U s e r _ d a t a : d a t a _ t y p e d e f a u l t N U L L ) ] ; i n t e r f a c e [ t o U : S _ R E L E A 5 E . c o n f i rm ( R e s u l t : r e s u l t _ t y p e ; U s e r _ d a t a : d a t a _ t y p e ) ] ; i n t e r f a c e [ f r o m U : S _ U _ A B O R T o r e q u e s t ( U s e r d a t a : d a t a t y p e ) ] ; " i n t e r f a c e [ t o U : S _ U _ A B O R T . i n d i c a t i o n ( U s e r d a t a : d a t a t y p e ) ] ; i n t e r f a c e [ t o U : S _ P _ A B O R T . i n d i c a t i o n ( R e a s o n : r e a s o n t y p e i n t e r f a c e [ f r o m U : S _ D A T A . r e q u e s t ( D a t a : d a t a _ t y p e ) ] ; i n t e r f a c e [ t o U : S _ D A T A . i n d i c a t i o n ( D a t a : d a t a t y p e ) ] ; i n t e r f a c e [ f r o m U : S _ E X P E D I T E D _ D A T A . r e q u e s t ( D a t a : d a t a t y p e ) ] ; i n t e r f a c e [ t o U : S _ E X P E D I T E D _ D A T A . i n d i c a t i o n ( D a t a : d a t a t y p e ) ] ; i n t e r f a c e [ t o U : S _ P _ E X P E C T I O N _ R E P O R T . i n d i c a t i o n R e a s o n : r e a s o n t y p e ) ] ; i n t e r f a c e [ f r o m U : S _ U _ E X P E C T I O N _ R E P O R T . r e q u e s t ( R e a s o n : r e a s o n _ t y p e ; U s e r d a t a : d a t a t y p e d e f a u l t N U L L ) ] ; i n t e r f a c e [ t o U : S _ U _ E X P E C T I O N _ R E P O R T . i n d i c a t i o n R e a s o n : r e a s o n _ t y p e ; U s e r d a t a : 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 U : S _ T Y P E D _ D A T A . r e q u e s t ( U s e r d a t a : d a t a _ t y p e ) ] ; ~ - 6 9 -i n t e r f a c e [ t o U : S _ T Y P E D _ D A T A . i n d i c a t i o n ( U s e r d a t a : d a t a t y p e ) ] ; i n t e r f a c e [ f r o m U : S_TOKEN_GI V E . r e q u e s t .( T o k e n : o c t e t _ t y p e ) ] ; i n t e r f a c e [ t o U : S _ T G K E N _ G I V E . i n d i c a t i o n ( T o k e n : o c t e t _ t y p e . ) ] ; i n t e r f a c e [ f r o m U : S _ T O K E N _ P L E A S E . r e q u e s t ( T o k e n . : o c t e t _ t y p e ; U s e r d a t a : 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 [ t o U : S _ T O K E N _ P L E A S E . i n d i c a t i o n ( T o k e n : o c t e t _ t y p e ; U s e r d a t a : 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 U : S _ S Y N C _ M I N O R . r e q u e s t ( . . C o n f i r m : o c t e t _ t y p e d e f a u l t N U L L ; S y n c _ p o i n t : s y n c _ s e r i a l _ t y p e ; U s e r _ d a t a : 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 [ t o U : S _ S Y N C _ M I N D R . i n d i c a t i o n ( C o n f i r m : o c t e t _ t y p e d e f a u l t N U L L ; S y n c _ p o i n t : s y n c _ s e r i a l _ t y p e ; U s e r d a t a : 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 U : S _ S Y N C _ M I N 3 R . r e s p o n s e ( „ S y n c _ p o i n t : s y n c _ s e r i a 1 __t y pe ; U s e r _ d a t a : 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 [ t o U : S _ S Y N C ^ M I N O R . c o n f i rm ( S y n c _ p o i n t : s y n c _ s e r i a 1 _ t y p e ; U s e r _ d a t a : 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 U : S _ S Y N C _ M A J O R . r e q u e s t ( , S y n c _ p o i n t : s y n c _ s e r i a l _ t y p e ; U s e r d a t a : 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 [ t o U : S _ S Y N C _ M A J O R . i n d i c a t i o n ( . S y n c _ p o i n t : s y n c _ s e r i a 1 _ t y p e ; U s e r d a t a : d a t a _ t y p e d e f a u l t NULL ) ] ; ~ - 7 0 -i n t e r f a c e [ f r o m U : S _ S Y N C _ M A J C R . r e s p o n s e ( U s e r d a t a : d a t a t y p e ) ] ; " i n t e r f a c e [ t o U : S _ S Y N C _ M A J C R . c o n f i rm ( U s e r d a t a : d a t a t y p e ) ] ; " i n t e r f a c e [ , f r o m U : S _ A C T I V I T Y _ B E G I N . r e q u e s t ( A c t i v i t y _ i d : a c t _ i d _ t y p e ; Type : a c t _ b e g i n _ t y p e ; 0 1 d _ a c t _ i d : a c t _ i d _ t y p e d e f a u l t N U L L ; S y n c _ p o i n t : s y n c _ s e r i a 1 _ t y p e d e f a u l t N U L L ; 0 1 d _ s e s s _ i d : i n t _ t y p e d e f a u l t N U L L ; U s e r d a t a : d a t a _ t y p e d e f a u l t N U L L ) ] ; i n t e r f a c e [ t o 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 ( A c t i v i t y _ i d : a c t _ i d _ t y p e ; Type : a c t _ b e g i n _ t y p e ; 0 1 d _ a c t _ i d : a c t _ i d _ t y p e d e f a u l t N U L L ; S y n c _ p o i n t : s y n . c _ s e r i a l _ t y p e d e f a u l t N U L L ; 0 1 d _ s e s s _ i d : i n t _ t y p e d e f a u l t N U L L ; U s e r d a t a : 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 U : S _ A C T I V I T Y _ E N D . r e q u e s t ( S y n . c _ p o i n t : s y n c _ s e r i a 1 _ t y pe ; U s e r d a t a : 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 [ t o U : S _ A C T I V I T Y _ E I \ D . i n d i c a t i o n ( S y n c _ p o i n t : s y n c _ s e r i a 1 _ t y p e ; U s e r d a t a : 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 U : S _ A C T I V I T Y _ E N D . r e s p o n s e ( U s e r d a t a : d a t a t y p e d e f a u l t N U L L ) ] ; " i n t e r f a c e [ t o U : S _ A C T I V I T Y _ E N D . c o n f i rm ( U s e r d a t a : 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 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 ( ) ] ; i n t e r f a c e [ t o U : S _ A C T I V I T Y _ I N T E R R U P T . i n d i c a t i o n ( ) ] ; i n t e r f a c e [ f r o m 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 ( ) ] ; i n t e r f a c e [ t o U : S A C T I V I T Y I N T E R R U P T . c o n f i r m ( - 7 1 -) ] ; i n t e r f a c e [ f r o m U : S A C T I V I T Y D I S C A R D . r e q u e s t ( ) ] ; i n t e r f a c e [ t o U : S A C T I V I T Y D I S C A R D . i n d i c a t i o n ( i n t e r f a c e [ f r o m U : S A C T I V I T Y D I S C A R D . r e s p o n s e ( i n t e r f a c e [ t o U : S A C T I V I T Y D I S C A R D . c o n f i r m ( ) ] ; i n t e r f a c e [ f r o m U : S _ C A P A B I L I T Y _ D A T A . r e q u e s t ( U s e r d a t a : d a t a t y p e ) ] ; " i n t e r f a c e [ t o 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 ( U s e r _ d a t a : d a t a _ t y p e ) 3 ; i n t e r f a c e [ f r o m U : S _ C A P A B I L I T Y _ D A T A . r e s p o n s e ( U s e r d a t a : d a t a t y p e ) ] ; " i n t e r f a c e [ f r o m U : S _ C A P A B I L I T Y _ D A T A . c o n f i r m ( U s e r _ d a t a : d a t a _ t y p e ) ] ; state abbreviations } FSM starts at in i t ia l state and ceases to exist at f inal state ; other abbreviations are used in current state f ie ld of a FSM transition } state any_state = ( U N C O N N E C T E D , C A L L I N G , C A L L E D , IDLE , W A I T _ F O R _ A C _ S P D U , W A I T _ F O R _ G T A _ S P D U , W A I T _ F O R _ A A _ S P D U , W A I T _ F O R _ D N _ S P D U , W A I T _ F O R _ M C D _ S P D U , W A I T _ F O R _ C D A _ S P D U , W A I T _ F O R _ A I A _ S P D U , W A I T _ F O R _ A D A _ S P D U , W AIT_FOR_reco ver y_SPDU, W A I T _ F O R _ S _ C O N N E C T _ R E S P , 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 _ S _ M C D _ R E S P . WAIT F O R S AI R E S P , - 7 2 -W A I T _ F O F T S _ A D _ R E S P , " ^  W A I T _ F O R _ C D A _ R E S P , WAIT_FOR_S_recover.y_REQ abort_allowed = ( { session may be aborted } G A L L I N G , C A L L E D , IDLE , W A I T _ F O R _ S _ C O N N E C T _ R E S P , W A I T _ F O R _ S _ R E L E A S E _ R E S P WAIT_FOR_S_MCD_RESP, WAIT_FOR_S_AI_RESP, WAIT_FOR_S_AD_RESP, WAIT_FOR_CDA_RESP, W A I T _ F O R _ A C _ S P D U , WAIT_FOR_DN_SPDU, WAIT_FOR_MCD_SPDU, WAIT_FOR_GTA_SPDU, W A I T _ F O R _ C D 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 } C A L L E D , IDLE, W A I T _ F O R_S_ C O N N E C T_RESP, W A I T _ F O R _ S _ R E L E A S E_RESP W A I T _ F O R_S_ M C D_RESP, WAIT_FOR_S_AI_RESP, WAIT_FOR_S_AD_RESP, W A I T _ F O R _ C D A _ R E S P , W AIT_FO R _ A C_SPDU, WAIT_FOR D N_SPDU, W AIT_FOR>1CD_SPDU, W A I T _ F O R _ G T A _ S P D U , W A I T _ F O R _ C D A_SPDU, W A I T _ F O R _ A I A _ S P D U , W A I T _ F O R _ A D A_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 , W A I T _ F O R _ D N_SPDU, WAIT_FOR_GTA_SPDU, W A I T _ F O R _ M C D_SPDU ); IDLE_or_DN-= ( { idle or awaiting an D N S P D U } -73-IDLE, WAIT_FOR_DN_SPDU ); IDLE_or_MCD =• ( { idle or awaiting an M C D SPDU } IDLE, W A I T _ F O R _ M C D 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 R E S P ); IDLE_or_MCDR = ( { idle or await ing a response for a sync ind } IDLE,. W A I T _ F O R _ S _ M C D _ R E S P ); 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 AIT_FO R_S_R E L E A SE_R ESP, WAIT F O R S M C D R E S P ); " " IDLE_or_DN_MCD = ( { idle or awaiting a D N or M C D SPDU } ' IDLE , W A I T _ F O R _ M C D _ S P D U W A I T _ F O R _ D N _ S P D U , ); I D L E _ o r _ G T A _ M C D R = ( { idle or awaiting a give token ack , SPDU or synchronization response } IDLE, W A I T _ F O R _ S _ M C D _ R E S P , WAIT_FOR G T A SPDU ); . IDLE_or_ree_REQ = ( { idle or await ing a recovery request } IDLE , WAIT_FOR_S_recovery_REQ ); IDLE_or_rec_SPDU = ( { idle or await ing a recovery SPDU } IDLE , WAIT_FOR_recovery_SPDU w a i t _ D N _ M C D _ S P D U = ( { wait ing for either a D N or M C D SPDU } W A I T _ F O R _ M C D _ S P D U , WAIT_FOR_DN_SPDU ); - 7 4 -in i t ia l = U N C O N N E C T E D ; { in i t ia l state } f inal = U N C O N N E C T E D ; { f i n a l state } • declaration of functions and procedures } 'pr imit ive' described verbally } 'forward' defined } function acceptable_CN( CN_pdu : Pdu ) : boolean; pr imit ive ; function acceptable_AC( AC_pdu : Pdu ) : boolean; pr imit ive ; function AC_reject_reason( AC_pdu : Pdu ) : result_type; pr imit ive ; function CN_reject_reason( CN_pdu : Pdu ) : result_type; pr imit ive ; function al loc_ref : int_type; pr imit ive ; function arith_and( a r g l , arg2: octet_type ): boolean; pr imit ive ; procedure assign_token_accept( token_item : octet_type ); forward; procedure assign_token_give( token_item : octet_type ); forward; procedure clear_session; pr imit ive ; function get_host( sess_addr : addr type ): h_addr_type; pr imit ive ; function get_tc_addr( sess_addr : addr_type ): tc_addr_type; pr imit ive ; procedure increment_sync( ss: sync_serial_type ); pr imit ive ; procedure in i t ia l i ze_machine; forward; function intersect( a r g l , arg2: octet_type ): octet_type; pr imit ive ; procedure intersect_sr( sess_requirements : int_type ); pr imi t i ve ; function isatokenin( token, token_item : octet_type ): boolean; pr imi t i ve ; function mapSaddr( haddr : h_addr_type; tc_addr : tc_addr_type ): addr_type; - 7 5 -pr imit ive ; function min( a, b: int_type ): int_type; pr imit ive ; function other_side( token : token_type ): boolean; forward; function set_qos( qos : qos_type ) : qos_type; pr imit ive ; procedure set_sr( session_requirements : int_type ); p r imi t ive ; procedure set_tokens( token_item : octet_type); pr imit ive ; function size( data unit : data_type ): int_type; pr imit ive ; function tc_disc_jeason( reason : reason_type ): result_type; pr imit ive ; function testSaddr( sess_addr : addr_type ): boolean; pr imit ive ; function this_side( token : token_type ): boolean; forward; function token_other_side( token_i tem: octet_type ): boolean; forward; function token_this_side( token_itenru: octet_type ): boolean; forward; function union( a r g l , arg2: octet_type ): octet_type; pr imit ive ; function valid_sp( sync : sync_serial_type ) : boolean; pr imit ive ; function pduCN( CN_reference : int_type; C N _ i d : sess_id_type; version : octet_type; lhost, fhost : h_addr_type; dk_token, r l_token, sm_token, ma_token : token_type; protocol_options: octet_type; in_max_SPDU, out_max_SPDU : int_type; i n i t j n a r k : sync_serial_type; session_req : int_type; user_data : data_type ): data_type; pr imit ive ; function pduAC( CN_reference : int_type; - 7 6 -C N _ i d : sess_id_type; version : octet_type; lhost, fhost : h_addr_type; dk_token, r l_tqken, smj token , ma_token : token_type; protocol_options: octet_type; in_max_SPDU, out_max_SPDU : int_type; init_mark : sync_serial_type; session_req : int_type; user_data : data_type ): data_type; pr imit ive ; function pduRF( CN_reference : int_type; tc_disconnect : octet_type; version : octet_type; result : result_type; session_req : int_type; user_data : data_type ): data_type; pr imit ive ; function pduCK 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 : octet_type; { tc_disc : F N , . A B , PT } token i tem : PT, GT { prepare type : PR } user_data : data_type { F N , D N , NF , A B , PT } ): data_type; pr imi t i ve ; function pduDT( pdu_code : pdu_type; { DT, E X , ER , C D A , C D , A D , AI } C N _ i d : int_type; data : data_type ): data_type; pr imit ive ; function pduC2s( pdu_code : pdu_type; { 'MKB, M C B , ; M K D , M C D , RS , R A , ED } CN_ id : int_type; serial_no : sync_serial_type; { M K B , M C B , M K D , M C D , RS, sync_item : octet_type: { M K B , M K D , RS , ED } user_data : data_type { M K B , M K D , RS, R A , ED } ): data_type; pr imit ive ; function pduC2a( pdu_code : pdu_type; { AS , A R } C N _ i d : int_type; serial_no : sync_serial_type; oact iv i ty_ id : act_id_type; AS } nact iv i ty_ id : act_id_type; { AS , A R } user_data : data_type { AS, A R } ): data_type; pr imit ive ; { definition of 'forward' functions and procedures } function other_side( token ): boolean; { T R U E if 'token' is on peer side } begin other side := ( CN_or ig in 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 := ( CN_or ig in 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( token_i tem: octet_type ): boolean; . { specif ied 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 ( isatokenin(DK_TOKEN, token_item)) then here := here and this_side( dk_token); if ( isatokenin(SY_TOKEN, token_item)) then here := here and this_side( sy_token); if ( isatokenin(MA_TOKEN, token_item ) then here : = here and this_side( ma_token); token_this_side := here end; function token_other side( token_item: octet_type ): boolean; { specif ied 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 satokenin(DK_TOKEN, token_item)) then there : - there and other_side( dk_token); if ( isatokenin(SY_TOKEN, token_item)) then there := there and other_side( sy_token); if ( isatokenin(MA_TOKEN, token_item)) then there := there and other_side( ma_token); token other side := there - 7 8 -end; procedure assign_token accept( token_item ); { assign tokens to this side } var token_value: token_type; begin if (CN_origin) then token_value := INITIATOR_SIDE 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 ( isatokenin(DK_TOKEN, token_item)) then dk token := token_value; if ( isatokeninTSY_TOKEN, token_item)) then sy_token := token_value; if ( isatokenin(MA_TOKEN, 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 := INITIATOR_SIDE; if ( isatokenin(TR_TOKEN,- token_item)) then tr token := token_value; if ( isatokeninTDK_TOKEN, token_item)) then dk token : - token_value; if ( isatokeninTSY_TOKEN, token_item)) then sy_token := token_value; if ( isatokenin(MA_TOKEN, token_item)) then ma_token := token_yalue end; { in i t ia l izat ion routine to set up F S M } procedure in i t ia l i ze_machine; begin CN_ref := 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 tc := T C J J N D E F I N E D ; f tc := T C J J N D E F I N E D ; CN_or ig in .:= F A L S E ; max_SPDU_in := 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 ; r l_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 := QOS; sync_serial := IN IT_SYNC_SERIAL ; sync_serial_confirmed := IN IT_SYNC_SERIAL ; Primitive Procedures This section gives verbal descriptions of the pr imit ive procedures and functions used in the speci f icat ion . The exact operation of these are determined by local implementation choices and restr ict ions. pr imit ive acceptable_CN( CN_pdu ) This pr imit ive returns a boolean value depending on whether the parameters of the C N SPDU is acceptable to the session machine. Some of the reasons for rejecting the C N SPDU may be unmatching protocol version numbers, protocol subset not supported, inval id acceptor address, insuff ic ient resources to support another connection, unacceptable protocol options or in i t ia l token assignments. Other local reasons for rejecting a C N may be also be considered. pr imit ive acceptable_AC( AC_pdu ) This pr imit ive returns a boolean value depending on whether the parameters of the accept (AC) SPDU is acceptable to the session machine. Some of the reasons for rejecting an A C SPDU may be unmatching protocol version numbers, protocol subset not supported, unsatisfactory max SPDU sizes/token assignments/protocol options, e tc . Other local reasons for rejecting an A C may be also be considered. pr imit ive AC_reject_reason( A C _ p d u ) This primit ive returns the reason the A C SPDU was rejected by the session machine, (see acceptable_AC pr imit ive) . pr imit ive CN_reject_reason( CN_pdu ) This pr imit ive returns the reason the C N SPDU was rejected by the session machine, (see acceptable C N primit ive) . - 8 0 -primit ive al loc_ref This primit ive returns a valid number to be used as the connection ident i f ier . pr imit ive arith_and( a r g l , arg2 ) This pr imit ive returns a boolean value depending on whether the ar i thmetic 'and' of its argument results in a non-zero value. pr imit ive clear_session This pr imit ive releases and resets buffer space and variables relevant to the connection. pr imit ive get_host( sess_addr ) This pr imit ive extracts and returns the host address(or name) specif ied in the given (session) address. pr imit ive get^tc_addr( sess_addr ) This pr imit ive extracts and returns the transport address specif ied in the given (session) address. pr imit ive increment_sync( sync_serial ) This pr imit ive increments the synchronize ser ia l number by one. (This is specif ied as a pr imit ive - due to the implementation dependent nature of the length .of the number). pr imit ive intersect( a r g l , arg2 ) This pr imit ive returns the arth imet ic 'and' of its two arguments. pr imit ive intersect_sr( sess_req ) This pr imit ive readjusts the session requirement flags by intersecting the current values with that given in sess_req. pr imit ive isatoken( token, token_item ) This pr imit ive returns a boolean value depending on whether token is one of the tokens specif ied in token_item (arithmetic 'and' yields non-zero value). pr imit ive mapSaddr( haddr, tc_addr ) - 8 1 -This primit ive returns the session address constructed by combining the given host and transport addresses. pr imit ive min( a r g l , arg2 ) This pr imit ive returns the minimum of its two arguments. pr imit ive set_qos( qos ) This pr imit ive returns the quality of service according to the given qos and local quality of service parameters. pr imit ive set_sr( sess_req ) This pr imit ive sets the session requirement flags according to the given sess_req and local requirements. pr imit ive set_tokens( tokens_values ) This pr imit ive 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 in i t ia l placement of tokens). pr imit ive size( buf ) This pr imit ive returns the length of the specif ied buffer (data_type entity) . pr imit ive tc_disc_reason( reason ) This pr imit ive returns a result_type value from the given reason for release of the transport connection. pr imit ive testSaddr( sess_addr ) This pr imit ive returns a boolean value depending on whether the given session address is val id . pr imit ive union( a r g l , arg2 ) This pr imit ive returns the arthmetic 'or' of its arguments. pr imit ive valid_sp( sync_point ) This pr imit ive returns a boolean value indicating if the given sync_point is greater than the last confirmed synchronization number but less than or equal to the - 8 2 -0 synchronization number of the last synchronization request, (see increment_sync pr imit ive) . pr imit ive pduXX( argl ist . . . ) These primitives are responsible for constructing and returning. SPDU's f rom given parameters. - 8 3 -State Transitions The operation of the session protocol is defined in the fol lowing state transitions. Each transition is accompanied by comments explaining its e f fects . The transitions are grouped into categories of connection establishment, connection release, abort, data transfer, exception data, capabil i ty data, token management, minor synchronization, major synchronization and act iv i ty management. - 8 4 -( c l ) < C A L L I N G > <-- < U N C O N N E C T E D > [from U: 5_CONNECT.request ] ( 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 CN_ref := a l loc_ref ; CN_or ig in := T R U E ; sess_id := [from U: Identif ier] ; 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 tc := 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_CONNECT.request ( Called_address := f t c , Calling_address := l t c , Exp_data_option := tc_expedited and session_expedited, Qual_of_service := qos )]; end; E N A B L I N G CONDITION A S_CONNECT.request event occurs at the User inter face; 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 SPDU is of acceptable length. C U R R E N T STATE The session machine is in the unconnected state . The session machine extracts the transport address with which it wi l l attempt to establish a transport connection. The machine saves parameters f rom the user request for constructing the connect (CN) SPDU later on. The session machine then attempts to establ ish, a transport connection to a peer transport entity by in i t iat ing a T_CONNECT. request event. } A C T I O N - 8 5 -R E S U L T A N T STATE The session machine awaits a T _ C O N N E C T . c o n f i r m event which wi l l conf i rm the establishment of the transport connection. - 8 6 -( c2 ) } < C A L L E D > <-- < U N C O N N E C T E D > [from T_CONNECT. ind icat ion] begin CN_ref := al loc_ref ; l t c := [from T:Called_address]; f tc := [from T:Call ing_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; { } E N A B L I N G CONDITION A T_CONNECT . ind icat ion event occurs at the Transport inter face; 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 tate . ACT ION The session machine accepts the request for the specif ied transport connection by in i t iat ing a T_CONNECT.response event. R E S U L T A N T STATE The session machine awaits the connect request (CN) S P D U . - 8 7 -( c3 ) } < U N C O N N E C T E D > <-- < C A L L I N G > [from T:T DISCONNECT. ind icat ion] [to U :S_CONNECT.conf i rm( 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; E N A B L I N G CONDITION A T_DISCONNECT. indicat ion event occurs at the Transport interface; this indicates that establishment of the transport connection is unsuccessful. C U R R E N T STATE The session machine awaits the establishment of a transport connection. The session machine init iates a S_CONNECT .conf i rm event to inform the user of the fai lure to establish a connection with the peer transport ent i ty . R E S U L T A N T STATE The session machine goes to the unconnected s tate . begin } ACT ION - 8 8 -( c4 ) } < W A I T _ F O R _ A C _ S P D U > <~ < C A L L I N G > [from T: T_CONNECT .con f i rm] begin [to T: T_DATA.request. ( Data := pduCN( CN_ref , sess_id, VERSION,-lhost, fhost, dk_token, t r_token, sy_token, . ma_token, P R O T O C O L J D P T I O N S , max_SPDU_in , max_SPDU_out , sync_ser ial , sess_req, user data E N A B L I N G CONDITION A T_CONNECT .con f i rm event occurs at the Transport inter face; this indicates a transport connection has been established. C U R R E N T STATE The session machine awaits establishment of a Transport connection. The session machine constructs and sends a connect (CN) SPDU. to the peer session entity to request the establishment of a session connection. R E S U L T A N T STATE The session machine awaits the arr ival of the accept (AC) S P D U . ))]; end; ACT ION - 8 9 -( c5 ). - — } < U N C O N N E C T E D > <-- < C A L L E D > [from T :T_DATA. ind icat ion] (( [from T:Spdu.ptype] = C N ) and not ( acceptable_CN( [from T:Spdu] ) )) begin [to T: T_DATA.request( Data := pduRF( CN_ref , T C _ D I S C O N N E C T , VERSION, . , CN_reject_reason( [from TrSpdu] ), [from T:Spdu.psess req], [from T:Spdu.pdata] ))]; clear_session; end; { } E N A B L I N G CONDITION A T_DATA. ind icat ion event occurs at the Transport inter face; this indicates the arr ival of a connect (CN) SPDU f rom the peer session entity . The connection requested is NOT acceptable to the session machine. C U R R E N T STATE The session machine may part icipate in incoming session connection requests. ACT ION The session machine determines the reason for rejecting the connection request and transmits a R F SPDU to signal to the peer session entity that the request has been ..refused. R E S U L T A N T STATE The session machines goes to the unconnected state . -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_DATA. indicat ion] ( ([from T:Spdu.ptype] = CN) and acceptable_CN( [from T:Spdu] ) ) begin CN_or ig in := 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] ); max_SPDU_in := min(MAX_SPDU_IN, [ f rom T:Spdu.pmax_SPDU_in]); max_SPDU_out := min(MAX_SPDU_OUT, [ f rom 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_CONNECT. indicat ion( Identifier := sess_id, Initiator_addr := faddr, Acceptor_addr := laddr, Qual_of_serv : - qos, Session_req := [from T:Spdu.psess_req], .Sync_ser ial := [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_DATA. ind icat ion event occurs at the Transport in ter face ; this indicates the arr ival of a connect request (CN) SPDU from the peer session ent i ty . The connection requested is acceptable to the session machine. C U R R E N T 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 init iates a S_CONNECT. ind icat ion event to inform the user of the arrived request. R E S U L T A N T STATE The session machine waits for the user to accept or reject the requested -91-connection. - 9 2 -( 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_CONNECT.response] not ( [from U:Result ] = A F F I R M A T I V E ) . ' ' " begin [to T: T_DATA.request( Data := pduRF( CN_ref , T C _ D I S C O N N E C T , VERSION, [from U:Result ] , [from U:Session_req], [from U:User_data] ))]; clear_session; end; { } E N A B L I N G CONDITION A S_CONNECT.response event occurs at the User inter face; the user has rejected the connection request. C U R R E N T STATE The session machine is wait ing for the user to accept or reject the requested connection. ACT ION The session machine sends a refuse (RF) SPDU to the peer session entity indicating the user's decision. R E S U L T A N T STATE The session machine is in the unconnected state . - 9 3 -( c8 ) { } < IDLE > < - < W A I T _ F O R _ S _ C O N N E C T _ R E S P > [from U: S CONNECT.response] ( ([from U:ResultI= AFF IRMAT IVE ) and -(size([from U:User_data]) <= M A X _ A C _ D A T A _ S I Z E ) ) begin laddr := [from U:Acceptor_addr] ; 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( dk_token = CHOICE - ) dk_token := [from U:Init_dk_token]; if( tr_token = C H O I C E ) tr_token := [from U:Init_tr_token]; . if( sy_token = C H O I C E ) sy_token := [from U:Init_sy_token]; if( ma_token = C H O I C E ) ma_token := [from U:Init_ma_token]; [to T: T_DATA.requ.est ( Data := pduAC( CN_ref , sess_id, VERSION, lhost, fhost, dk_token, t r_token, sy_token, ma_token, protocol_opts, max_SPDU_in , max_SPDU_out , sync_ser ial , sess_req, [from U:User_data] ))]; end; {_ } E N A B L I N G CONDITION A S_CONNECT.response event occurs at the User inter face; the user has accepted the session connection request. The data to be sent to the peer session entity is of acceptable s i ze . C U R R E N T S T A T E The session machine is waiting for the user to accept or reject the requested connection. A C T I O N - 9 4 -The session machine adjusts the connection parameters according to the user response. The session requirements for the connection are those specif ied in both the C N and A C SPDUs. If the user was given the choice for in i t ia l placement of the tokens, the new values of the tokens are set. An accept (AC) SPDU is .constructed and sent to the peer session ent i ty . R E S U L T A N T STATE The session machine is in the idle (data transfer) s tate . - 9 5 -( 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_DATA. indicat ion] ([from T:Spdu.ptype] = RF) begin [to U :S_CONNECT.conf i rm( Identifier := sess_id, Acceptor addr := laddr, Result :=~Lfrom TrSpdu.presult], Qual_of_serv := qos, Session_req := [from T:Spdu.psess_req], Sync_serial := sync_ser ial , User_data := [from T:Spdu.pdata] )]; . [to T: T_DISCONNECT.request] ; c l e a r s e s s i o n ; end; {. E N A B L I N G C O N D I T I O N A T_DATA. ind icat ion event occurs at the Transport inter face; this indicates the arr ival of a connection refuse (RF) SPDU from the peer session entity: the connection request was rejected. C U R R E N T S T A T E The session machine awaits arr ival of a connection accept (AC) S P D U . A C T I O N The session machine initiates a S _CO NNE CT . con f i rm event to notify the user that the connection request was refused by the peer session ent i ty . The session machine also issues a T_DISCONNECT.request at the transport interface to terminate the transport connection. R E S U L T A N T S T A T E The session machine goes to the unconnected s tate . - 9 6 -( 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_DATA. indicat ion] (([from T:Spdu.ptype] = AC) and not acceptable_AC( [from T:Spdu] )) begin set_tokens( [from T:Spdu.ptoken] ); result := AC_reject_reason( [from T:Spdu] ); [to U :S_CONNECT.conf i rm( 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 := tr_token, Init_sy_token := sy_token, Init_ma_token := ma_token, User_data := [from TtSpdu.pdata] )]; [to T: T_DATA.request( Data := pduCK 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 I N T E R V A L )]; end; E N A B L I N G CONDITION A T_DATA. ind icat ion event occurs at the Transport inter face; this indicates the arr ival of a connection accept (AC) SPDU from the peer session entity : the connection request was accepted. However, the negotiated parameters in the A C SPDU is NOT acceptable to the session machine. C U R R E N T STATE The session machine awaits arr ival of a connection accept (AC) S P D U . ACT ION - 9 7 -The session machine init iates a S_CONNECT .conf i rm event to notify the user that the connection negotiation has fa i led . The session machine issues an abort (AB) SPDU to abort the connection. The abort t imer is started to wait for the A A SPDU to arr ive. R E S U L T A N T S T A T E The session machine waits for the arr ival of an abort accept (AA) S P D U . -98-( e l l ) { } < IDLE > < - < W A I T _ F O R _ A C _ S P D U > [from T :T_DATA. indicat ion] (( [from T:Spdu.ptype] = A C ) and acceptable_AC( [from T:Spdu] )) begin set_tokens( [from T:Spdu.ptoken] ); max_SPDU_in := [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 tc ); [to U: S_CONNECT.conf i rm( 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 := sync_ser ial , 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; E N A B L I N G CONDITION A T_DATA. ind icat ion event occurs at the Transport inter face; this indicates the arr ival of a connection accept (AC) SPDU f rom the peer session entity : the connection request was accepted. The A C SPDU parameters are acceptable to the session machine. C U R R E N T STATE The session machine awaits the arr ival of an accept (AC) S P D U . ACT ION The session machine saves the negotiated parameters given by the A C SPDU and init iates an S_CONNECT .conf i rm event to notify the user of the establishment of the connection with the peer session ent i ty . The functional units available for the - 9 9 -connection are the intersection of the functional units specif ed in the C N and A C SPDU session requirements. R E S U L T A N T S T A T E The session machine is in the connected state (ready to transfer data with its peer session entity). - 1 0 0 -( r l ) { < WAIT_FOR_DN_SPDU > <-- < IDLE > [from U: S_RELEASE.request] ( ((dk_token = NOT_AV 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_DATA.request( Data := pduCl( F N , CN_ref , TC_DISCONNECT , [from U:User_data] ))3; end; {. E N A B L I N G CONDITION A S_RELEA5E.request event occurs at the User inter face; 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. C U R R E N T STATE The session machine is in the idle state (ready for data transfer) . ACT ION The session machine constructs and sends a f inish (FN) SPDU to its peer session entity . R E S U L T A N T STATE The session machine awaits arr ival of a disconnect (DN) SPDU to conf i rm termination of the connection. - 1 0 1 -( r2 ) _-___} < WAIT_FOR S _ R E L E A S E _ R E S P > <-- < IDLE > Tfrom T: T_DATA.indication] ( ([from T:Spdu.ptype] = FN") and ((dk_token = N O T _ A V A I L A B L E ) or other_side( dk_token )) and ((tr_tok.en = N O T _ A V A I L A B L E ) or other side( tr_token )) ) begin [to U: S_RELEASE.indication( User_data : - [from T:Spdu.pdata] )]; end; {_ } E N A B L I N G CONDITION A T_DATA. ind icat ion event occurs at the Transport inter face; this indicates the arr ival of a finish. (FN) SPDU f rom the peer session ent i ty . The data token is either not available or is on the peer session entity s ide. Similar ly with the release token. C U R R E N T STATE The session machine is in the idle state (ready for data transfer) . ACT ION The session machine init iates an S_RELEASE. ind icat ion event to notify the user of the arr ival of the finish S P D U . R E S U L T A N T 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 avai lable. - 1 0 2 -( r3 ) { } < W A I T _ F O R _ S _ R E L E A S E _ R E S P > <-- < WAIT_FOR_DN_SPDU > [from T :T_DATA. indicat ion] ( ([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_RELEASE. indicat ion( User_data := [from T:Spdu.pdata] )]; end; { } E N A B L I N G CONDITION A T_DATA. ind icat ion event occurs at the Transport inter face; this indicates arr ival of a finish (FN) SPDU f rom the peer session entity . The connection does not have the negotiated release option. C U R R E N T STATE The session machine awaits arr ival of a disconnect (DN) SPDU to conf i rm termination of the connection. ACT ION The session machine notifies the session user of the arr ival of the F N SPDU by in i t iat ing a S_RELEASE. ind icat ion event. R E S U L T A N T STATE The session machine awaits response from the user to either accept or reject the termination request. - 1 0 3 -( r 4 ) { } < 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_DATA. indicat ion] ( ([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_RELEASE. indicat ion( User_data := [from TrSpdu.pdata] )]; end; { , } E N A B L I N G CONDITION A T_DATA. ind icat ion event occurs at the Transport inter face; this indicates the arr ival of a finish (FN) SPDU from the peer session entity . Neither the data token nor the release token is avai lable. C U R R E N T STATE The session machine awaits the arr ival of a major mark conf irmation or act iv i ty end acknowledgement (MCD) SPDU. ACT ION The session machine init iates an S_RELEASE. ind icat ion event to notify the user of the arr ival of the F N S P D U . R E S U L T A N T STATE The session machine waits for the user to respond to the disconnect request. ( r5 ) } < IDLE > < - < W A I T _ F O R _ S _ R E L E A S E _ R E S P > [from U: S_RELEASE.response] ( not ([from UrResult] = AFF IRMATIVE ) and not (tr_token = N O T _ A V A I L A B L E ) ) begin [to T: T_DATA.request( Data := pduCl( N F , CN_ref , NULL,^ [from LhUser data] ))]; end; { } E N A B L I N G CONDITION A S_RELEASE.response event occurs at the User inter face; this indicates that the user has rejected the disconnect request.. The connection has the negotiated release option. C U R R E N T STATE The session machine is wait ing for the user to accept or reject the disconnect request. ACT ION The session machine constructs and sends a not f inish (NF) SPDU . to the peer session entity . R E S U L T A N T STATE The session machine goes back to the idle s tate . - 1 0 5 -( r6 ) { } < U N C O N N E C T E D > < - < W A I T _ F O R _ S _ R E L E A S E _ R E S P > [from U:S_RELEASE.response] ([from UrResult] = AFF IRMATIVE ) begin [to T :T_DATA.request( Data : = pduCK D N , CN_re f , N U L L , [from U:User_data] ))]; clear_session; end; { } E N A B L I N G CONDITION A S_RELEASE.response event occurs at the User inter face; this indicates that the user has accepted the disconnect request. C U R R E N T STATE The session machine is wait ing for the user to either accept or reject the disconnect request. ACT ION The session machine constructs and sends a disconnect conf irmation (DN) SPDU to the peer session entity . R E S U L T A N T STATE The session machine goes into the unconnected s tate . - 1 0 6 -( 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_DATA. indicat ion] ( ([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_RELEASE.conf i rm( Result := A F F I R M A T I V E , User_data := [from T:Spdu.pdata] )]; end; { } E N A B L I N G CONDITION A T_DATA. ind icat ion event occurs at the Transport interface; this indicates arr ival of a disconnect conf irmation (DN) SPDU. The connection does not have negotiated release. C U R R E N T STATE The session machine is wait ing for the user to either accept or reject a disconnect request f rom the peer session ent i ty . ACT ION The session machine notifies the session user of the arr ival of the D N SPDU by in i t iat ing a S_RELEASE .con f i rm event. R E S U L T A N T STATE The session machine remains in the same state . - 1 0 7 -( r8 ) { } < U N C O N N E C T E D > < - < WAIT_FOR_DN_SPDU > [from T :T_DATA. ind icat ion] ([from T:Spdu.ptype] = D N ) begin [to U: S _ R E L E ASE.conf i rm( Result := A F F I R M A T I V E , User_data : - [from TrSpdu.pdata] )]; [to T: TJDISCONNECT.request ] ; clear_session; end; {_ } E N A B L I N G CONDITION A T_DATA. ind icat ion event occurs on the Transport inter face; this indicates the arr ival of a disconnect (DN) SPDU: the peer session entity has accepted the disconnect request. C U R R E N T STATE The session machine is wait ing for the arr ival of the D N S P D U . ACT ION The session machine init iates 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_DISCONNECT.request event. R E S U L T A N T STATE The session machine is in the unconnected state . - 1 0 8 -( r9 ) { } < IDLE > < - < WAIT_FOR_DN_SPDU > [from T :T_DATA. ind icat ion] ( ([from T:Spdu.ptype] = N F ) and not (tr_token = N O T _ A V AIL A B L E ) ) begin [to U: S_RELEASE.conf i rm( Result := U S E R _ R E J E C T , . . User_data := [from T:Spdu.pdata] )]; end; {. } E N A B L I N G CONDITION A T_DATA. ind icat ion event occurs at the Transport inter face; this indicates the arr ival of a not finish (NF) SPDU f rom the peer session entity rejecting the disconnect request. The release token must be available (the connection has the negotiated release option). C U R R E N T STATE The session machine awaits arr ival of a disconnect (DN) SPDU to conf i rm termination of the connection. ACT ION The session machine notifies the user of the peer session entity's refusal of the disconnect request by in i t iat ing a S_RELEASE .conf i rm event. R E S U L T A N T STATE The session machine goes back to the idle s tate . -109-( a b l ) { __} < W A I T _ F O R _ A A _ S P D U > <-- < abort_allowed > [from U: S_U_ABORT.request] begin [to T: T_DATAorequest( Data := pduCK 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; { } E N A B L I N G CONDITION A S_U_ABORT.request occurs at the User inter face; 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 tate . ACT ION The session machine constructs and sends an abort (AB) SPDU to the peer session entity. The session machine also issues a request to the system to start an abort t imer . R E S U L T A N T STATE The session machine awaits arr ival of an abort accept (AA) S P D U . - 1 1 0 -( ab2 ) {. } < U N C O N N E C T E D > < abort_allowed > [from T: T_DATA. indicat ion] ( [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_ABORT. indicat ion( 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_ABORT. indicat ion( Reason := reason )] end; [to T: T_DISCONNECT.request] ; clear_session; end; { } E N A B L I N G CONDITION A T_DATA. ind icat ion event occurs at the Transport inter face; this indicates the arr ival of an abort (AB) SPDU. C U R R E N T STATE The session machine is in an abortable s tate . ACT ION The session machine notifies the user of the aborted state by in i t iat ing a S_U_ABORT. ind icat ion or S_P_ABORT. ind icat ion event depending on the reason specif ied 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_DISCONNECT.request event. R E S U L T A N T STATE The session machine goes into the unconnected s tate . - I l l -( ab3 ) { < same_state > < - < W A I T _ F O R _ A A _ S P D U > [from T: T_DATA. indicat ion] ( [from T:Spdu.ptype] = A B ) begin end; {-E N A B L I N G CONDITION A T_DATA. ind icat ion event occurs at the Transport inter face; this indicates arr ival of an abort (AB) SPDU. C U R R E N T STATE The session machine awaits arr ival of an abort accept (AA) SPDU from the peer session entity . ACT ION No action is taken. R E S U L T A N T STATE The session machine remains in the same state . - 1 1 2 -( 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: T_DATA. ind icat ion] ( [from T:Spdu.ptype] = A A ) begin [to T: T_DISCONNECT.request] ; [to S: Timer.cancel( Name := TAB )]; clear_session; end; {_ } E N A B L I N G CONDITION A T_DATA. ind icat ion event occurs at the Transport inter face; this indicates the arr ival of an abort accept (AA) SPDU f rom the peer session entity . C U R R E N T STATE The session machine awaits arr ival of an A A SPDU to confirm abortion of the connection. ACT ION The session machine init iates a T_DISCONNECT.request event to release the transport connection. It also stops the abort t imer by issuing a T imer.cancel request to the system. R E S U L T A N T STATE The session machine goes into the unconnected s tate . - 1 1 3 -( ab-5 ) { } < 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 S: Timer.response] ( [from S:Name] = T A B ) begin [to T: T_DISCONNECT.request] ; clear_session; end; { _} E N A B L I N G CONDITION A Timer.response event occurs at the System interface; this indicates that the abort t imer has t imed out. C U R R E N T STATE The session machine awaits arr ival of an abort accept ( A A ) SPDU from the peer session entity . ACT ION The session machine proceeds to terminate the connection by in i t iat ing a T_DISCONNECT.request event. R E S U L T A N T STATE The session machine goes into the unconnected state . - 1 1 4 -( ab6 ) { < 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: T jD ISCONNECT. ind icat ion] begin [to S: Timer .cancel( Name := TAB )]; clear_session; end; { E N A B L I N G CONDITION A T_DISCONNECT. ind icat ion event occurs at the Transport interface; this indicates that the peer transport entity wishes to terminate the connection. C U R R E N T STATE The session machine awaits arr ival of an abort accept (AA) SPDU from the peer session entity. ACT ION The session machine stops the abort t imer (Timer .cancel) and clears the connection. R E S U L T A N T STATE The session machines goes to the unconnected state . - 1 1 5 -( ab7 ) { } < U N C O N N E C T E D > <-- < pabort_allowed > [from T: T_DISCONNECT. indicat ion] begin [to U:S_P_ABORT. indicat ion( Reason := T C _ G O N E )]; clear_session; end; {- } E N A B L I N G C O N D I T I O N A T_DISCONNECT. indicat ion event occurs at the Transport interface; this indicates that the transport connection is no longer avai lable. C U R R E N T S T A T E The session machine is in a provider abortable state (any state except U N C O N N E C T E D , C A L L I N G or W A I T _ F O R _ A A _ S P D U ) . A C T I O N The session machine notifies the user of the loss of connection by in i t iat ing a S_P_ABORT. ind icat ion event. R E S U L T A N T S T A T E The session machine goes into the unconnected s tate . - 1 1 6 -(dl) .< same_state > <-- < IDLE > [ f rom 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_DATA.request( Data := pduDT( DT, CN_ref , [from U: Data] ))]; end; {-E N A B L I N G CONDITION A S_DATA.request event occurs at the. User inter face; this indicates the user wishes to send data to the peer session entity . Either there is no act iv i ty management or there is an act iv i ty in progress. A lso , either the data token is not available or the data token is on this side. C U R R E N T STATE The session machine is in the idle s tate . ACT ION The session machine constructs and sends a data (DT) SPDU to the peer session entity . R E S U L T A N T STATE The session machine remains in the same state . - 1 1 7 -( d2 ) } < same_state > <-- < W A I T _ F O R _ S _ M C D _ R E S P > [ f rom U: S p A T A . r e q u e s t ] (dk_token = NOT_AV AIL ABLE) . begin [to T: T_DATA.request( Data := pduDT( DT, CN_ref , [from U: Data] ))]; end; { } E N A B L I N G CONDITION A S_DATA.request event occurs at the User inter face; this indicates the user wishes to send data to the peer session entity . The data token is not avai lable. C U R R E N T STATE The session machine is wait ing for the user to respond to a act iv i ty end indication or a major mark indicat ion. ACT ION The session machine constructs and sends a data (DT) SPDU to the peer session entity . R E S U L T A N T STATE The session machine remains in the same state . - 1 1 8 -( d3 ) { } < WAIT_FOR_recover„y_SPDU > <-- < W A I T _ F O R _ S _ M C D _ R E S P > [ f rom T: T_DATA. ind icat ion ] ( ([from T:Spdu.ptype] = DT) and (dk_token = NOT_AV AIL A B L E ) ) begin [to U: S_P_EXCEPTION_REPORT. ind icat ion ( Reason := P R O T O C O L _ E R R O R ; )]; [to T: T_DATA.request( Data := pduDT( E R , CN_ref , [from T:.Spdu] ))]; end; { } E N A B L I N G CONDITION A T_DATA. ind icat ion event occurs at the Transport inter face; this indicates the arr ival of a data (DT) S P D U . The data token is not avai lable. C U R R E N T STATE The session machine is wait ing for the user to respond to a act iv i ty end indication or a major mark indicat ion. ACT ION A S_P_EXCEPT ION_REPORT . ind ica t ion event is in i t iated 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 ent i ty . R E S U L T A N T STATE The session machine awaits arr ival of a 'recovery' SPDU (it is in an error state). i - 1 1 9 -( d4 ) } < same_state > <~ < WAIT_FOR_recover,y_SPDU > [ f rom T: T_DATA. ind icat ion ] ( ([from T:Spdu.ptype] = DT) and . . not (dk_token = N O T _ A V A I L A B L E ) ) begin end; {_ } E N A B L I N G CONDITION A T_DATA. ind icat ion event occurs at the Transport inter face; this indicates the arr ival of a data (DT) SPDU= The data token is avai lable. C U R R E N T STATE The session machine is awaiting arr ival of a 'recovery' SPDU (it is in the error state). ACT ION No action is taken (the incoming data is ignored). R E S U L T A N T STATE The session machine remains in the same state . - 1 2 0 -( d5 ) { } < same_state > <-- < IDLE > [ f rom T: T_DATA. indicat ior i ] ( ([from T.:Spdu.ptype] = DT) and ((activity = NO T_A VAIL A B L E ) or (activity = ON)) and ((dk_token = NO T_A VAIL A B L E ) or other_side( dk_token )) ) begin [to U: S DATA. indicat ion( Data := [from T:Spdu.pdata] )]; end; { } E N A B L I N G CONDITION A T_DATA. ind icat ion event occurs at the Transport inter face; this indicates the arr ival of a data (DT) S P D U . Either there is no act iv i ty management or there is an act iv i ty in progress. Also, 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 tate . ACT ION The session machine notifies the user of the arr ival of the data. R E S U L T A N T STATE The session machine remains in the same state . - 1 2 1 -( d6 ) < same_state > <-- < WAIT_FOR_DN_SPDU > [ 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 = NOT AVAILABLE) ) ) ) begin [to U: S DATA. indicat ion( Data := [from T.:Spdu.pdata] )]; end; {-E N A B L I N G CONDIT ION A T_DATA. ind icat ion event occurs at the Transport inter face; this indicates the arr ival of a data (DT) SPDU. Either there is no act iv i ty management or there is an act iv i ty in progress. A lso , either the data token is not available or the data token is not on this side and the release token is not avai lable. C U R R E N T STATE The session machine awaits the arr ival of a disconnect acknowledgement (DN) SPDU. ACTION The session machine notifies the user of the arr ival of the data. R E S U L T A N T STATE The session machine remains in the same state . - 1 2 2 -( d7 ) } < same_state > < - < W A I T _ F O R _ M C D _ S P D U > [ f rom T: T_DATA. ind icat ion ] ( ([from TrSpdu.ptype] = DT) and (dk_token = N O T _ A V A I L A B L E ) ) begin [to U: S_DATA. indicat ion( Data : - [from T:Spdu.pdata] )]; end; {. } E N A B L I N G CONDITION A T_DATA. ind icat ion event occurs at the Transport inter face; this indicates arr ival of a data (DT) SPDU. The data token is not avai lable. C U R R E N T STATE The session machine is wait ing for the arr ival of a M C D S P D U . ACT ION The session machine notifies the user of the arr ival of the data. R E S U L T A N T STATE The session machine remains in the same state . - 1 2 3 -( e l ) _______ } < same_state >. <-- < IDLE > [ f rom U: S_TYPED_DATA. request ] ((activity = N O T _ A V A I L A B L E ) or (activity = ON)) begin [to T: T_DATA.request( Data := pduC2s( E D , CN_ref , N U L L , T Y P E D _ D A T A , [from U:User_data] ))]; end; { } E N A B L I N G CONDITION A S_TYPED_DATA. request event occurs at the User inter face; this indicates that the user wishes to send 'typed' data — not constrained by the presence of the data token. Either there is no act iv i ty management or there is an act iv i ty in progress. C U R R E N T STATE The session machine is in the idle s tate . ACT ION The session machine constructs and sends an exception data (ED) SPDU with no reason parameter. R E S U L T A N T STATE The session machine remains in the same state . - 1 2 4 -( e2 ) } < same_state > <~ < IDLE_or_MCD > [ from T: T_DATA. ind icat ion ] ( ([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)) ) E N A B L I N G CONDITION A T_DATA. ind icat ion event occurs at the Transport in ter face ; this indicates the arr ival of a typed data (ED) SPDU (it has no reason parameter). There is either no act iv i ty management or there is an act iv i ty in progress. C U R R E N T STATE The session machine is in the idle state or awaiting arr ival of a major synchronization/activity end acknowledgement (MCD) S P D U . ACT ION The session machine notifies the user of the arr ival of the typed data. R E S U L T A N T STATE The session machine remains in the same state . - 1 2 5 -( e3 ) } < same_state > <~ < WAIT_FOR_DN_SPDU > [ f rom T: T_DATA. ind icat ion ] ( ([from T:Spdu.ptype] = ED) and [from T:Spdu.pno_reason_field] and ((activity = ON) or (activity = NOT_AVAILABLE ) ) and (dk_token = NO T_A VAIL A B L E ) ) begin [to U: S_TYPED_DATA. ind icat ion( User data := [from T:Spdu.pdata] end; {_ } E N A B L I N G CONDITION A T_DATA. ind icat ion event occurs at the Transport in ter face ; this indicates the arr ival of a typed data (ED) SPDU (it has no reason parameter). The data token is not avai lable. C U R R E N T STATE The session machine is wait ing for a disconnect acknowledgement (DN) S P D U . ACT ION The session machine notifies the user of the arr ival of the typed data. R E S U L T A N T STATE The session machine remains in the same state . - 1 2 6 -( e4 ) { } < same_state > < - < WAIT_FOR_DN_SPDU > [ f rom T: X_DATA. i indicat ion ] ( ([from TrSpdu.ptype] = ED) and ((activity = ON) or (activity = NOT_AVAILABLE) ) and not (dk_token = N O T _ A V A I L A B L E ) and (tr_token = NOT_AV AIL A B L E ) ) begin if ( [from T:Spdu.pno_reason_field] ) then . . [to U: S_TYPED_DATA. ind icat ion( User_data := [from TrSpdu.pdata] )] else [to U: S_U_EXCEPTION_REPORT. ind icat ion ( Reason := [from TrSpdu.preason], User_data := [from TrSpdu.pdata] )]; end; {_ } E N A B L I N G CONDITION A T_DATA. ind icat ion event occurs at the Transport inter face; this indicates the arr ival of a ED SPDU- The data token is avai lable. The release token is not avai lable. C U R R E N T STATE o The session machine is wait ing for the arr ival of a disconnect (DN) S P D U . ACT ION The session machine notifies the user of the arr ival of the S P D U . If there is a reason on the SPDU, ' then it is exception data otherwise it is typed data. R E S U L T A N T STATE The session machine remains in the same s tate . - 1 2 7 -( e5 ) { } < WAIT_FOR_recovery_SPDU > <-- < IDLE > [ f rom U: S_U_EXCEPTION_REPORT. request ] ( ((activity = NOT_AV AIL A B L E ) or (activity = ON)) and other_side( dk_token ) ) begin [to T: T_DATA;request( Data := pduC2s( E D , CN_ref , N U L L , [from U:Reason], [from U:User_data] ))3; end; {. } E N A B L I N G CONDITION A S_U_EXCEPTION_REPORT. request event occurs at the User inter face; this indicates the user wishes to signal a user exception to the peer session ent i ty . Either there is no act iv i ty management or there is an act iv i ty 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 tate . ACT ION The session machine constructs and sends an exception data (ED) SPDU with reason parameter as specif ied on the user request. R E S U L T A N T STATE The session machine goes into an error s tate ; it awaits arr ival of a recovery. SPDU from the peer session entity . - 1 2 8 -( e6 ) - - } < same_state > <— < IDLE_or_MCD > [ f rom T: T_DATA. ind icat ion ] ( ([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 EXCEPT ION_REPORT . ind ica t ion ( Reason r= [from TrSpdu.preason], User_data r= [from TrSpdu.pdata] )];-end; {-E N A B L I N G CONDITION A T_DATA. ind icat ion event occurs at the Transport inter face; this indicates the arr ival of a exception report (ED) SPDU (it contains a reason parameter). Either there is no act iv i ty management or there is an act iv i ty in progress. A lso , the data token is on the other side. C U R R E N T STATE The session machine is in the idle state or is await ing arr ival of major synchronization/activity end acknowledgement (MCD) S P D U . ACT ION The session machine notifies the user of the arr ival of the exception report. R E S U L T A N T STATE The session machine remains in the same state . - 1 2 9 -( el ) { } < WAIT_FOR_recovery_REQ > < - < IDLE o r _ M C D > [ f rom T: T JDATA. ind icat ion J ( ([from T:Spdu.ptype] = ED) and ((activity = NOT_AV AIL ABLE ) or (activity = ON)) and not [from T.:Spdu.pno reason_field] and this_side( dk_token )7 begin [to U: S_U_EXCEPTION_REPORT. ind icat ion ( Reason := [from TrSpdu.preason], User_data := [from T:Spdu.pdata] )]; end; { } E N A B L I N G CONDITION A T_DATA. ind icat ion event occurs at the Transport inter face; this indicates the arr ival of a exception report (ED) SPDU (it contains a reason parameter). E i ther there is no act iv i ty management or there is an act iv i ty in progress. The data token is on the this side. C U R R E N T STATE The session machine is in the idle state or is awaiting a major synchronization/activity end acknowledgement (MCD) S P D U . ACT ION The session machine notifies the user of the arr ival of the exception report. R E S U L T A N T STATE The session machine awaits response f rom the user concerning the exception report. - 1 3 0 -( cdl ) < W A I T _ F O R _ C D A _ S P D U > < - < IDLE > [from, U:S CAPABILITY_DATA.request ] ( this_sideT ma_token ) and (this_side( sy_token ). or ( s y j o k e n = NOT_AVAILABLE) ) and (this_side( dk_token ) or (dk_token = NOT AVA ILABLE ) ) and (activity = O F F )T begin [to T :T_DATA.request( Data := pduDT( C D , CN_ref , [from U:User_data] ))]; end; {-E N A B L I N G CONDITION A S_CAPABIL ITY_DATA. request event occurs at the User inter face; this indicates that the user wishes to send capabil i ty data (a l imited amount of transparent data outside activit ies) to the peer session ent i ty . 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 act iv i ty in progress. That is, this session machine has the right to start the next act iv i ty . C U R R E N T STATE The session machine is in the idle s tate . ACT ION The session machine constructs and sends a capabi l i ty data (CD) SPDU to the peer session entity . R E S U L T A N T STATE The session machine awaits acknowledgement for the capabi l i ty data . - 1 3 1 -( cd2 ) { } < W A I T _ F O R _ C D A _ R E S P X - < IDLE > [from T: T_DATA. ind icat ion] ( ([from T:Spdu.ptype] - CD) and other_side( ma_token ) and (other_side( sy_token ) or (sy_token = NO T_A VAIL ABLE)) and (other_side( dk_token ) or (dk_token = NOT AVA ILABLE ) ) and (activity = O F F )T begin [to U :S_CAPABIL ITY_DATA. ind icat ion ( User_data := [from T:Spdu.pdata] )]; end; {-E N A B L I N G CONDITION A T_DATA. ind icat ion event occurs at the Transport inter face; this indicates the arr ival of a capabi l i ty data (CD) SPDU. 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 act iv i ty in progress. C U R R E N T STATE The session machine is in the idle s tate . ACT ION The session machine notifies the user of the arr ival of the C D SPDU by in i t iat ing a S_CAPABIL ITY_DATA . ind ica t ion event. R E S U L T A N T STATE The session machine awaits response from the user concerning the capabi l i ty data . - 1 3 2 -( cd3 ) { < IDLE > <-- < W A I T _ F O R _ C D A _ R E S P > [from U:S_CAPABIL ITY_DATA. response] begin [to T :T_DATA.request( Data := pduDT( C D A , CN_re f , [from U:User data] ' ))1; end; E N A B L I N G CONDITION A S_CAPABIL ITY_DATA. response event occurs at the User interface; this indicates that the user wishes to acknowledge previously received capabi l i ty data. C U R R E N T STATE The session machine is awaiting response from the user to acknowledge the capabi l i ty data. ACT ION The session machine constructs and sends a capabi l i ty data acknowledgement (CDA) SPDU to the peer session entity . R E S U L T A N T STATE The session machine goes to the idle s tate . - 1 3 3 -( cd4 ) { } < IDLE > <-- < W A I T _ F O R _ C D A _ S P D U > [from T: T JDATA. ind icat ion] ([from TrSpdu.ptype] = C D A ) begin [to U :S_CAPABIL ITY_DATA .conf i rm( User data := [from T:Spdu.pdata] )]; end; { } E N A B L I N G CONDITION A. T_DATA. ind icat ion event occurs at the Transport inter face; this indicates the arr ival of a capabi l i ty data acknowledgement (CDA) S P D U . C U R R E N T STATE The session machine is wait ing for the arr ival of a C D A S P D U . ACT ION The session machine confirms the user's capabil i ty data request by in i t iat ing a S _ C A P A B I L I T Y _ D A T A . c o n f i r m event. R E S U L T A N T STATE The session machine goes to the idle s tate . - 1 3 4 -( t l ) { } < same_state > <— < I D L E _ o r _ G T A _ M C D R > [from U: S_TOKEN_PLEASE, request ] begin [to T :DATA.request( Data := pduCK PT, . CN_re f , [from U:Token], [from U:User data] ))]; end; {...... } E N A B L I N G CONDITION A S_TOKEN_PLEASE. request event occurs at the User inter face; 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 SPDU or. await ing a response f rom the user concerning a major synchronization indication or act iv i ty end indicat ion. ACT ION The session machine constructs and sends a please token (PT) SPDU to the peer session entity . R E S U L T A N T STATE The session machine remains in the same state . - 1 3 5 -( t2 ) { < same_state > < - < I D L E _ o r _ D N _ G T A _ M C D > [from T: T_DATA. indicat ion] ([from TrSpdu.ptype] = PT) begin [to U :S_TOKEN_PLEASE. ind icat ion( Token := [from TrSpdu.ptoken], User_data : - [from TrSpdu.pdata] )]; end; { — E N A B L I N G CONDITION A T_DATA. ind icat ion event occurs at the Transport inter face; this indicates arr ival of a request for token (PT) S P D U . C U R R E N T 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). ACT ION The session machine notifies the session user of the (PT) request by in i t iat ing a S_TOKEN_PLEASE . ind ica t ion event. R E S U L T A N T STATE The session machine remains in the same state . - 1 3 6 -( t3 ) { } < same_state > < - < IDLE_or_MCDR > [from U: S_TOKEN_GIVE.request] ( token_this_side( [from UrToken] ) and ((activity = ON) or (activity = NOT_AVAILABLE) ) ) begin [to T :DATA.request( Data := pduCK GT, CN_re f , [from UrToken], N U L L ))]; assign_token_give( [from UrToken] ); end; E N A B L I N G CONDITION A S_TOKEN_GIVE.request event occurs at the User inter face; this indicates that the user wishes to give one (or more) token(s) to the peer session ent i ty . The token(s) is on this side and either there is no act iv i ty management available or an act iv i ty is in progress. 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 major synchronize/activity end indicat ion. ACT ION The session machine constructs and sends a give token (GT) SPDU to the peer session entity- The'token(s) is now on the other side. R E S U L T A N T STATE The session machine remains in the same state . - 1 3 7 -( t4 ) {. < W A I T _ F O R _ G T A _ S P D U > <-- < IDLE > [from U: S_TOKEN_GIVE.request] ( token_this_side( [from U:Token] ) and (activity = OFF) ).. begin [to T :DATA.request( Data := pduCK GT, CN_ref , [from UrToken], N U L L ))]; assign_token_give( [from U:Token] ); end; E N A B L I N G CONDITION A S_TOKEN_GIVE.request event occurs at the User inter face; 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 act iv i ty in progress. C U R R E N T STATE The session machine is in the idle state . ACT ION The session machine constructs and sends a give token (GT) SPDU to the peer session entity . The token(s) is now on the other side. R E S U L T A N T S T A T E . The session machine awaits arr ival of an acknowledgement for the GT S P D U . - 1 3 8 -( t5 ) { } < same_state > <~ < IDLE_or_DN_MCD > [from T: T_DATA. ind icat ion] ( ([from TrSpdu.ptype] = GT) and token_other_side( [from T:Spdu.ptoken] ) ) begin [to U:S_TOKEN_GIVE. indicat ion( Token := [from T:Spdu.ptoken] )]; if ( act iv i ty = O F F ) then [to T: T_DATA.request( Data := pduCl ( G T A , CN_re f , N U L L , N U L L ))]; assign_token_accept( [from T:Spdu.ptoken] )]; end; E N A B L I N G CONDITION A T_DATA. ind icat ion event occurs at the Transport inter face; this indicates arr ival of a give token (GT) SPDU f rom the peer session entity . The peer session entity has possession of the said token(s). C U R R E N T STATE The session machine is either in the idle state or is wait ing for the arr ival of a disconnect (DN) or major synchronize/activity end acknowledgement (MCD) S P D U . ACT ION The session machine notifies the session user of the (GT) SPDU by in i t iat ing a S_TOKEN_GIVE. indicat ion event. If no»_act iv i ty is in progress, a give token acknowledgement (GTA) SPDU is sent to the peer session ent i ty . The specif ied token(s) is now on this side. R E S U L T A N T STATE The session machine remains in the same state . - 1 3 9 -( t6 ) } < IDLE > <-- < W A I T _ F O R _ G T A _ S P D U > [from T: T_DATA. indicat ion] ( [from T:Spdu.ptype] = G T A ) begin end; { } E N A B L I N G CONDITION A T_DATA. ind icat ion event occurs at the Transport inter face; this indicates the arr ival of a give token acknowledgement (GTA) S P D U . C U R R E N T STATE The session machine is awaiting arr ival of a give token acknowledgement (GTA) SPDU. ACT ION No action is taken. R E S U L T A N T STATE The session machine goes to the idle s tate . - 1 4 0 -( t7 ) { _ . _ _ } < IDLE > <-- < WAIT_FOR_S_reco.very_REQ > [from U: S_TOKENLGIVE.request] ( i satokenin (DK_TOKEN, [from UrToken]) and token_this_side( [from UrToken] ) ) begin [to TrDATA.request( Data r= pduCK GT, CN_re f , [from UrToken], N U L L ))]; assign_token_give( [from UrToken] ); end; E N A B L I N G CONDITION A S_TOKEN_GIVE.request event occurs at the User inter face; this indicates that the user wishes to give the data token (and possibly other tokens) to the peer session ent i ty . The token(s) is on this s ide. C U R R E N T STATE The session machine is wait ing for a 'recovery' request from the user to exit the error state. ACT ION The session machine constructs and sends a give token (GT) SPDU to the peer session entity . The token(s) is now on the other side. R E S U L T A N T STATE The session machine goes to the idle s tate . - 1 4 1 -( t8 ) { } < IDLE > <-- < WAIT_FOR_recovery_SPDU > [from T: T_DATA. ind icat ion] ( ([from T:Spdu.ptype] = GT) and isatokenin(DK_TOKEN, [from T:Spdu.ptoken]) and token_other_side( [from T:Spdu.ptoken] ) ) begin [to U:S_TOKEN_GIVE. indicat ion( Token := [from T:Spdu.ptoken] )]; assign_token_accept( [from TrSpdu.ptoken] ); end; { } E N A B L I N G CONDITION A T_DATA. ind icat ion event occurs at the Transport inter face; this indicates arr ival of a give token (GT) SPDU f rom the peer session ent i ty . 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 await ing a 'recovery' SPDU to exit the error s tate . ACT ION The session machine notifies the session user of the arr ival of the GT SPDU by in i t iat ing a S_TOKEN_GIVE. indicat ion event. The token(s) is reassigned to this side. R E S U L T A N T STATE The session machine goes to the idle s tate . - 1 4 2 -( s y l ) } < same_state > <-- < IDLE > [from U:S_SYNC_MINOR.request ] ( ((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( Data := pduC2s( M K B , CN_re f , sync_ser ial , [from U:Conf i rm] , [from U:User_data] ))]; increment_sync( sync_serial ); end; { } E N A B L I N G CONDITION A S_SYNC_MINOR.request event occurs at the User inter face; this indicates the user wishes to establish a minor synchronization point. Either there is no act iv i ty management or there is an act iv i ty in progress. The synchronize minor 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 s tate . ACT ION A synchronize-minor (MKB) SPDU is constructed and sent to the peer session ent i ty . The internal synchronization ser ial number is incremented. R E S U L T A N T STATE The session machine remains in the same state . - 1 4 3 -( sy2 ) ) < same_state > <— < IDLE > [from T :T_DATA. ind icat ion] ( ([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_SYNC_MINOR. indicat ion( Conf i rm := [from T: Spdu.pmisc], Sync_point := [from T: Spdu.psync_ serial] , User_data := [from TrSpdu.pdata] - ) ] ; increment_sync( sync_serial ); end; E N A B L I N G CONDITION A T_DATA. ind icat ion event occurs at the Transport inter face; this indicates the peer session entity wishes to establish a minor synchronization point. Either there is no act iv i ty management or there is an act iv i ty 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 tate . A synchronize-minor indication is given to the user. The internal synchronization serial number is incremented. R E S U L T A N T STATE The session machine remains in the same state . } ACT ION - 1 4 4 -( sy3 ) { < same_state > <-- < WAIT_FOR_DN_SPDU > [from T :T_DATA. indicat ion] ... ( ([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_SYNC_MINOR. indicat ion( Conf i rm := [from T :Spdu.pmisc] , Sync_point := [from T: Spdu.psync serial] , User_data := [from T:, Spdu.pdata] -)]; increment_sync( sync_serial ); end; {-E N A B L I N G CONDITION A T_DATA. ind icat ion event occurs at the Transport inter face; this indicates the peer session entity wishes to establish a minor synchronization point. Either there is no act iv i ty management or there is an act iv i ty in progress. The synchronize minor token is on the other side. The data token is not avai lable. C U R R E N T STATE The session machine is awaiting arr ival of a disconnect (DN) SPDU to complete the termination process. ACT ION A synchronize-minor indication is given to the user. The internal synchronization serial number is incremented. R E S U L T A N T STATE The session machine remains in the same state . - 1 4 5 -( 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_DATA. indicat ion] ( (([from T:Spdu.ptype] = M K B ) or ([from TrSpdu.ptype] = MCB)) and not (sy_token = NOT_AV AIL A B L E ) ) begin [to U: S_P_EXCEPTION_REPORT. ind icat ion ( Reason := P R O T O C O L _ E R R O R )]; [to T: T_DATA.request( Data := pduCK A B , CN_re f , 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; {_ } E N A B L I N G CONDITION A T_DATA. ind icat ion event occurs at the Transport inter face; this indicates the arr ival of a minor synchronization establishment or conf i rmation (MKB or MCB) S P D U . The synchronize minor token is avai lable. C U R R E N T STATE The session machine is awaiting response from the user for an act iv i ty end or major synchronization indicat ion. ACT ION A protocol exception report is indicated to the user. The session connection is aborted. R E S U L T A N T STATE The session machine awaits arr ival of an acknowledgement for the abort S P D U . - 1 4 6 -( sy5 ) } < same_state > <~ < WAIT_FOR_recovery_SPDU > [from T :T_DATA. indicat ion] ( (([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; { } E N A B L I N G CONDITION A T_DATA. ind icat ion event occurs at the Transport inter face; this indicates the arr ival of either a minor synchronization establishment or conf irmation (MKB or M C B ) S P D U . The synchronize minor token is avai lable. C U R R E N T STATE The session machine is awaiting arr ival of a recovery. SPDU from the peer session entity to exit the error state. ACT ION No action is taken. R E S U L T A N T STATE The session machine remains in the same state . - 1 4 7 -( sy6 ) { < same_state > <-- < I D L E _ o r _ R E L R _ M C D R > [from U:S_SYNC_MINOR.response] ( ((activity = NO T_A VAIL A B L E ) or (activity = ON)) and not ( sy token = NOT_AV AIL A B L E ) and valid_spT [from U:Sync_point] ) ) begin [to T :T_DATA.request( Data := pduC2s( M C B , CN_ref , ' [from U:SyncjDoint], N U L L , N U L L ))]; sync_serial_confirmed := [from U:Sync_point]; end; {_ E N A B L I N G CONDITION A S_SYNC_MINOR.response event occurs at the User inter face; this indicates the user wishes to respond to a peer in i t iated minor synchronization request. Either there is no act iv i ty management or there is an act iv i ty in progress. The synchronize minor token is available. The synchronization point the user wishes to conf i rm is val id . 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 rom the peer session entity . ACT ION A synchronize-minor confirmation (MCB) SPDU is constructed and sent to the peer session entity. The synchronize ser ial number in the response is recorded. R E S U L T A N T STATE The session machine remains in the same state . - 1 4 8 -( sy7 ) { < same_state > <-- < IDLE_or_DN_MCD > [from T :T_DATA. ind icat ion] ( ([from TrSpdu.ptype] = M C B ) and ((activity = NOT_AVAILABI_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_SYNC_MINOR.conf i rm( . Sync_point : = [from T: Spdu.psync_serial], User_data := [from T: Spdu.pdata] )]; sync_serial_confirmed := [from T:Spdu.psync_serial]; end; {-E N A B L I N G CONDITION A T_DATA. ind icat ion occurs at the Transport inter face; this indicates arr ival of a minor synchronization conf irmation (MCB) S P D U . Either there is no act iv i ty management or there is an act iv i ty in progress. The synchronize minor token is avai lable. The synchronization point the peer session entity wishes to conf i rm is va l id . C U R R E N T STATE The session machine is in the idle state or awaiting arr ival of a disconnect (DN) or major synchronize/activity end acknowledgement (MCD)SPDU. ACT ION A synchronize minor conf irmation is given to the user. The confirmed synchronization ser ial number is recorded. R E S U L T A N T STATE The session machine remains in the same state . - 1 4 9 -( m a l ) { } < W A I T _ F O R _ M C D _ S P D U > < - < IDLE > [from U :S_SYNC_MAJOR. request ] ( ((activity = N O T _ A V A I L A B L E ) or (activity = ON)) and this_side( ma^token ) and ((dk_token = , NO T_A VAIL A B L E ) or this side( dk_token )) and ((sy_token = NOT_AV AIL A B L E ) or this_side( sy_token )) ) begin [to T: T_DATA.request( Data := pduC2s( M K D , CN_ref , sync_ser ial , N O T _ E O A C T , [from UrUser data] ))]; increment_sync( sync_serial ); act_end_conf_pending : - F A L S E ; end; {_ } E N A B L I N G C O N D I T I O N A S_SYNC_MAJOR. request event occurs at the User inter face; this indicates the user wishes to establish a major synchronization point. Either there is no act iv i ty management or there is an act iv i ty 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 s ide. C U R R E N T S T A T E The session machine is in the idle s tate . A C T I O N A synchronize-major (MKD) SPDU is constructed and sent to the peer session entity . The internal synchronization serial number is incremented. R E S U L T A N T S T A T E The session machine awaits arr ival of an acknowledgement for the major synchronization S P D U . - 1 5 0 -( ma2 ) { _ _ _ _ _ _ } < IDLE > <-- < W A I T _ F O R _ S _ M C D _ R E S P > [from U:S_SYNC_MAJOR. response] ( not act_end_conf_pending ) begin [to T:T DATA.r.equest( Data := pduC2s( M C D , CN_re f , sync_ser ial , N U L L , [from U:User_data] ))]; sync_serial_confirmed := sync_serial ; end; E N A B L I N G C O N D l f ION A S_SYNC_MAJOR.response event occurs at the User inter face; this indicates that the user wishes to respond to a peer in i t iated major synchronization request. The session machine is awaiting response for a major synchronization point (and not an act iv i ty end) indicat ion. C U R R E N T STATE The session machine is awaiting response from the user concerning a major synchronization request or an act iv i ty end signal f rom the peer session entity . ACT ION A synchronize-major confirmation (MCD) SPDU is constructed and sent to the peer session entity . The synchronization response confirms al l previous minor synchroniation points. R E S U L T A N T STATE The session machine goes to the idle s tate . - 1 5 1 -( ma3 ) _..} < same_state > <-- < WAIT_FOR_DN_SPDU > [from T :T_DATA. ind icat ion] ( ([from TrSpdu.ptype] - M K D ) and ((activity = NOT_AV AIL ABLE ) 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_SYNC_MAJOR. ind icat ion ( ,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_ACTIVITY END.indication( ,Sync_point := [from T: Spdu.psync serial],. User_data := [from T: Spdu.pdata]")]; act_end_conf_pending := T R U E ; ' act iv i ty := OFF ; . end; increment_sync( sync_serial ); end; {. } E N A B L I N G CONDITION A T_DATA. ind icat ion event occurs at the Transport inter face; this indicates that the peer session entity wishes to establish a major synchronization point or end an act iv i t y . Either there is no act iv i ty management or there is an act iv i ty in progress. The synchronize major/activity token is on the other side. The data token is not avai lable. 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 arr ival of a disconnect (DN) SPDU to complete the termination process. A C T I O N A synchronize-major or end of act iv i ty indication is given to the user. The internal synchronization serial number is incremented. If the peer session entity request is to end the current act iv i ty , set the act iv i ty switch to O F F . A flag.-is set denoting whether the incoming SPDU is an act iv i ty end indication or not. - 1 5 2 -R E S U L T A N T S T A T E The session machine remains in the same state . - 1 5 3 -( ma4 ) { } < W A I T _ F O R _ S _ M C D _ R E S P > <-- < IDLE > [from T :T_DATA. ind icat ion] ( ([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 = NOT_AV AIL ABLE ) 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_SYNC_MAJOR. ind icat ion ( -Sync_point := [from T: Spdu.psync serial ] , User_data := [from T: Spdu.pdata] -)] else [to U:S_ACTIVITY_END.indicat ion( ,Sync_point := [from TY Spdu.psync_serial]j" User_data := [from T: Spdu.pdata] )]; increment_sync( sync_serial ); end; {_ } E N A B L I N G CONDITION A T_DATA. ind icat ion event occurs at the Transport inter face; this indicates the peer session entity wishes to establish a major synchronization point or end an act iv i ty . Either there is no act iv i ty management or there is an act iv i ty 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 state . ACT ION A synchronize-major or end of act iv i ty indication is given to the user. The internal synchronization ser ial number is incremented. R E S U L T A N T STATE The session machine awaits response from the user concerning the major synchronization or act iv i ty end indicat ion. - 1 5 4 -( 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_DATA. ind icat ion] ( (([from TrSpdu.ptype] = M K D ) or ([from TrSpdu.ptype] = MCD)) ) begin [to U: S_P_EXCEPTION_REPORT. ind icat ion ( Reason := PROTOCOL_ERROR.•)] ; [to T: T_DATA.request( Data := pduCK A B , CN_re f , 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; {_ „_____} E N A B L I N G CONDITION A T _ D A T A b d i c a t i o n event occurs at the Transport inter face; this indicates the arr ival of a major synchronization/activity end establishment or conf irmation (MKD or M C D ) S P D U . C U R R E N T STATE The session machine is awaiting response from the user on an act iv i ty end/major synchronization indicat ion. ACT ION A protocol exception report is indicated to the user. The session connection is aborted. R E S U L T A N T STATE The session machine awaits the arr ival of an acknowledgement for the abort S P D U . - 1 5 5 -( ma6 ) { , } < IDLE > <-- < WAIT_FOR M C D _ S P D U > [from T :T_DATA. ind icat ion] ([from T:Spdu.ptype] = M C D ) begin if act_end_conf_pending then begin [to U: S^ACTIVITY_END.conf i rm( User_data := [from T:. Spdu.pdata] )]; act iv i ty := 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 := sync_ser ial ; end; {-E N A B L I N G CONDITION A T_DATA. ind icat ion occurs at the Transport inter face; this indicates arr ival of a major synchronization/activity end conf irmation (MCD) S P D U . C U R R E N T STATE The session machine is awaiting arr ival of the M C D S P D U . ACT ION A synchronize major/activity end conf i rmation is given to the user. The ser ia l number of the synchronization point confirms al l previous minor synchronization points. If the acknowledment SPDU is for the end of an act iv i ty , set the act iv i ty switch to O F F . -R E S U L T A N T STATE The session machine goes to the idle s tate . - 1 5 6 -( ma7 ) { } < WAIT_FQR recovery_SPDU > <-- < WAIT_FORJ-ecovery_SPDU > Tfrom T:T_DATA.indication] 0 ( ([from TrSpdu.ptype] = M K D ) and not (ma_token = N O T _ A V A I L A B L E ) ) begin end; {. } E N A B L I N G CONDITION A T_DATA. ind icat ion event occurs at the Transport inter face; this indicates the arr ival of a major synchronization/activity end (MKD) S P D U . The synchronize major/activity token is avai lable. C U R R E N T STATE The session machine is awaiting arr ival of a 'recovery' SPDU from the peer session entity to exit the error state. ACT ION No action is taken. R E S U L T A N T STATE The session machine remains in the same state . - 1 5 7 -( a l ) < same_state > <-- < IDLE > [ from U: S_ACTIVITY_BEGIN.request ] ((activity = OFF) and this_side( ma_token ) and (this_side( sy_token ) or (s,y_token = NOT_AVAILABLE) ) and ((dk_token = N O T _ A V A I L A B L E ) or this_side( dk_token )) ) begin act iv i ty = O N ; if( [from U:Type] - START ) then begin sync_serial := IN IT_SYNC_SERIAL ; user_data := pduC2a(AS, CN_re f , N U L L , N U L L , [from U:Act iv i ty_ id ] , [from U:User_data] ); end; else begin ,„ . ^ sync_serial := [from U:Sync_point]; user_data := pduC2a(AR, CN_ref , _ sync_ser ial , [from U:01d_act_id], [from U:Act iv i ty_ id ] , [from U:User data] ); end; [to T :T_DATA.request( Data : = user data; )]; end; {_ } E N A B L I N G CONDITION A S_ACTIVITY_BEGIN.request event occurs „at the User in ter face ; this indicates the user wishes to begin or resume an act iv i ty . There is currently no act iv i ty in progress. The synchronization major/activity token is on this s ide. The data token (synchronization minor token) is either not available or is on this s ide. C U R R E N T STATE The session machine is in the idle s tate . - 1 5 8 -ACT ION The session machine constructs and sends either an act iv i ty start (AS) or an act iv i ty resume (AR) SPDU to the peer session entity depending on the type specif ied in the user request. If it is a START request, then reset the internal synchronization ser ial number; otherwise set it to the user supplied value. The act iv i ty switch is set to O N . R E S U L T A N T STATE The session machine remains in the same state . - 1 5 9 -( a2 ) { } < same_state > <~ < IDLE_or_DN > [ from T: T_DATA. ind icat ion ] ( ([from T:Spdu.ptype] = AS) and (activity = OFF) 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 = NOT_AV AIL A B L E ) or other_side( dk_token )) ) begin sync_serial : = IN IT_SYNC_SERIAL ; [to U:S_ACTIVITY_BEGIN. indication( Act i v i t y_ id := [from T:Spdu.pnew_act_id], Type := START , User_data := [from T:Spdu.pdata] )]; act iv i ty = O N ; end; { } ENABLING CONDITION A T_DATA. ind icat ion event occurs at the Transport inter face; this indicates the arr ival of an act iv i ty start (AS) S P D U . There is currently no act iv i ty 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. C U R R E N T STATE The session machine is in the idle state or is await ing a disconnect acknowledgement (DN) S P D U . ACTION The internal synchronization serial number is reset. The session, machine notif ies the user by in i t iat ing an S_ACTIVITY_BEGIN. indicat ion event. The act iv i ty switch is set to O N . RESULTANT STATE The session machine remains in the same state . - 1 6 0 -( a3 ) { } < same_state > <-- < IDI_E_or_DN > [ f rom T: T_DATA. ind icat ion ] ( ([from TrSpdu.ptype] = AR) and (activity = OFF) and other_side( ma_token) and ((sy_token = NDT_AV AIL A B L E ) or other_side( sy token )) and ((dk_token = NOT_AV AIL A B L E ) or other_side( dt_token )) ) begin sync_serial := [from T:Spdu.psync_serial]; [to U:S_ACTIVITY_BEGIN. indication( 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 := sync_ser ial , User_data := [from TrSpdu.pdata] )]; act iv i ty = O N ; end; {-E N A B L I N G CONDITION A T_DATA. ind icat ion event occurs at the Transport inter face; this indicates the arr ival of an act iv i ty resume (AR) S P D U . There is currently no act iv i ty in progress. The major synchronization/activity token is on the peer entity s ide. The data token (minor synchronization token) is not available or is on the other side. C U R R E N T STATE The session machine is in the idle state or is wait ing for arr ival of a disconnect acknowledgement (DN) S P D U . ACT ION The internal synchronization ser ial number is set to the received ser ial number. The session machine notifies the user by in i t iat ing an S_ACTIVITY_BEGIN. indicat ion event. The act iv i ty switch is set to O N . R E S U L T A N T STATE The session machine remains in the same state . - 1 6 1 -( a4 ) {. } < W A I T _ F O R _ M C D _ S P D U > <-- < IDLE > [from U:S_ACTIVITY_END.request] ( (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( Data := pduC2s( M K D , CN_ref , , sync_serial , E O A C T , [from UiUser data] . ))]; increment_sync( sync_serial ); act_end_conf_pending := T R U E ; end; { } E N A B L I N G C O N D I T I O N A S_ACTIVITY_END.request event occurs at the User inter face; this indicates the user wishes to terminate an act iv ty . There is an act iv i ty 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. C U R R E N T S T A T E The session machine is in the idle s tate . A C T I O N A synchronize-major (MKD) SPDU is constructed and sent to the peer session entity. The internal synchronization serial number is incremented. R E S U L T A N T S T A T E The session machine awaits arr ival of an acknowledgement for the act iv i ty end (MKD) SPDU. - 1 6 2 -( a5 ) } < IDLE > <-- < 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_DATA.request( Data := pduC2s( M C D , CN_re f , sync_ser ial , N U L L , [from U:User data] ))]; sync_serial_confirmed := sync_ser ial ; act iv i ty := O F F ; end; { } E N A B L I N G CONDITION A S_ACTIVITY_END.response event occurs at the User inter face; this indicates the user wishes to respond to a peer in i t iated act iv i ty end request. The session machine is awaiting a response for an end of act iv i ty (and not a major synchronization) indicat ion. C U R R E N T STATE The session machine is awaiting response from the user concerning an act iv i ty end signal f rom the peer session entity . ACT ION A synchronize major (MCD) SPDU is constructed and sent to the peer session entity . The act iv i ty end response confirms al l previous minor synchroniation points. The act iv i ty switch is set to O F F . R E S U L T A N T STATE The session machine goes to the idle s tate . - 1 6 3 -( a6 ) { } < WAIT_FOR_AIA_SPDU > <-- < IDLE_or_rec_REQ > [from U:S_ACTIVITY_INTERRUPT.request ] ( (activity = ON) and this_side( ma_token ) and ((dk_token = NO TRAVAIL A B L E ) or this_side( dk_token )) ) begin [to T: T_DATA.request( Data := pduDT( AI , -CN_ref , N U L L ))]; end; E N A B L I N G CONDITION A S_ACTIVTTY_INTERRUPT.re quest event occurs at the User inter face; this indicates the user wishes to interrupt the current act iv i ty . There is an act iv i ty 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 tate . ACT ION A act iv i ty interrupt (AI) SPDU is constructed and sent to the peer session ent i ty . R E S U L T A N T STATE The session machine awaits arr ival of an acknowledgement for the act iv i ty interrupt S P D U . - 1 6 4 -( a7 ) { } < WAIT_FOR_S_AI_RESP > <-- < IDLE_or rec_SPDU > [ f rom T: T_DATA. ind icat ion T ( ([from TrSpdu.ptype] = Al) and other_side( ma_token ) and (activity = ON) and ((dk_token = NOT_AV AIL A B L E ) or other_side( dk_token )) ) begin [to U :S_ACTIVITY_INTERRUPT. ind icat ion] ; end; { } E N A B L I N G CONDITION A T_DATA. ind icat ion event occurs at the Transport inter face; this indicates that the peer session entity wishes to interrupt the current act iv i ty . The synchronize major/activity token is not on this s ide. There is an act iv i ty 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 tate . ACT ION The session machine notifies the user by ini t iat ing an S_ACTIV ITY_INTERRUPX. ind icat ion event. R E S U L T A N T STATE The session machine awaits response from the user concerning the act iv i ty interrupt request. - 1 6 5 -( a8 ) } < IDLE > <-- < WAIT_FOR_S_AI R E S P > [from U:S_ACTIVITY_INTERRUPT.response] begin ~ [to T:T_DATA.request( Data := pduDT( A IA , CN_re f , N U L L . ))]; act iv i ty := O F F ; end; {_ } E N A B L I N G CONDITION A S_ACTIVITY_INTERRUPT.response event occurs at the User interface; this indicates the user wishes to respond to a peer in i t iated act iv i ty interrupt. C U R R E N T STATE The session machine is awaiting response from the user concerning an act iv i ty interrupt f rom the peer session entity . ACT ION An act iv i ty interrupt acknowledgement (AIA) SPDU is constructed and sent to the peer session ent i ty . The act iv i ty switch is set to OFF... R E S U L T A N T STATE The session machine goes to the idle s tate . - 1 6 6 -( a9 ) { } < IDLE > <-- < W A I T _ F O R _ A l A _ S P D U > [ f rom T: T_DATA. ind icat ion ] ([from TrSpdu.ptype] - AIA) begin [to U :S_ACTIV ITY_INTERRUPT.conf i rm] ; act iv i ty := O F F ; end; {. „ } E N A B L I N G CONDITION A T_DATA. ind icat ion event occurs at the Transport inter face; this indicates that the peer session entity wishes to acknowledge the act iv i ty interrupt. C U R R E N T STATE The session machine is awaiting the arr ival of an act iv i ty interrupt acknowledgement (AIA) SPDU. ACT ION The session machine notifies the user by in i t iat ing an S_ACTIV ITY_ INTERRUPX.conf i rm event. The act iv i ty switch is set to O F F . R E S U L T A N T STATE The session machine goes to the idle state . - 1 6 7 -( alO ) } < W A I T _ F O R _ A D A _ S P D U > <-- < IDLE_or_rec_REQ > [from U: S_ACTIVITY_DISCARD.request] ( (act iv i ty = ON) and this_side( ma_token ) and ((dk_token = NOT_A VAIL A B L E ) or this_side( dk_tokeh )) ) begin [to T: T_DATA.request( Data := pduDT( A D , CN_re f , N U L L . ))]; end; {_ ..} E N A B L I N G CONDITION A S_ACTIVITY_DISCARD.request event occurs at the User interface; this indicates the user wishes to cancel the current act iv i ty . There is an act iv i ty in progress. The synchronize major/activity token is on this s ide. 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 tate . ACT ION A act iv i ty discard (AD) SPDU is constructed and sent to the peer session ent i ty . R E S U L T A N T STATE The session machine awaits arr ival of an acknowledgement for the act iv i ty discard S P D U . - 1 6 8 -( a l l ) { } < WAIT_FOR_S_AD_RESP > <-- < IDLE_or_rec_SPDU > [ from T: T_DATA. ind icat ion ] ( ([from TrSpdu.ptype] = AD) and other_side( ma_token ) and (activity = ON) and ((dk_token = NO T_A VAIL ABLE ) or other_side( dk_token )) ) begin [to U :S_ACTIVITY_DISCARD. indicat ion] ; end; { } E N A B L I N G CONDITION A T_DATA. ind icat ion event occurs at the Transport inter face; this indicates that the peer session entity wishes to cancel the current act iv i ty . The synchronize major/activity token is on the peer entity side. There is an act iv i ty 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 tate . ACT ION The session machine notifies the user by ini t iat ing an S_ACTIVITY_DISCARD. indicat ion event. R E S U L T A N T STATE The session machine awaits response from the user concerning the act iv i ty discard request. -169-( al2 ) } < IDLE > <-- < WAIT_FOR_S_AD_RESP > [from U:S_ACTIVITY_DISCARD.response] begin [to T:T_DATA.request( Data := pduDT( A D A , CN_ref , N U L L act iv i ty end; := O F F ; {-E N A B L I N G CONDITION A S_ACTIVITY_DISCARD.response event occurs at the User interface; this indicates the user wishes to respond to a peer in i t iated act iv i ty cancel lat ion. C U R R E N T STATE The session machine is awaiting response from the user concerning an act iv i ty cancel lat ion from the peer session entity . ACT ION An act iv i ty discard acknowledgement (ADA) SPDU is constructed and sent to the peer session entity . The act iv i ty switch is set to O F F . . R E S U L T A N T STATE The session machine goes to the idle state . - 1 7 0 -

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