Abstract Estelle is a Formal Description Technique (FDT) developed by ISO for specifying distributed systems. The aims of developing FDTs are to enable unambiguous specifications and to provide a basis for analysis and verification of communication protocols. We have developed a technique of verifying Estelle specifications. This paper describes how the ISO RTSE protocol can be modelled using Estelle and the process of analysing such specifications. The analysis is done by first transforming the Estelle specifications into NPNs, and then the NPN specifications are analysed by a proven automated verification tool, PROTEAN. It is found that translating the English specifications into Estelle to give a formal specification is not a difficult task and Estelle enables the specification to be analysed. Thus, the main objectives of ISO in developing FDTs are satisfied. Keywords: Estelle, Numerical Petri Nets, PROTEAN, RTSE, Application layer protocol, Formal specification, Protocol verification, Reachability analysis 1.Introduction Traditionally, specifications of communication protocols are written in a natural language (e.g. English). However, when written in a natural language, the specifications can be ambiguous and open to misinterpretation. This is an especially serious problem in developing telecommunication software and protocols, because the services provided often have complex interactions with other services. In addition, the process of translating requirements into a finished product is time consuming and labour intensive, because a specification written in a natural language does not lend itself to analysis or consistency checking. In view of these issues, formal languages called Formal Description Techniques (FDTs) have been developed by ISO. The objectives of ISO in developing FDTs were [1]: to enable unambiguous, clear and precise descriptions of OSI standards to be written; to allow such descriptions to be verified for consistency and correctness; to provide clear guidance to designers and implementors of OSI systems as to what they should implement, but not how; and to provide a sound basis for conformance testing. To increase design quality, communication protocols should be specified in an FDT, which enables unambiguous specifications to be written and to be verified by a computer-aided tool. Estelle [7, 8] is one of the FDTs developed by ISO for specifying distributed and concurrent systems. It is particularly suited for describing communication protocols and services. Estelle is based on an extended finite state machine model described in a Pascal-like language. Each component of communication protocols is specified by a module whose functional behavior is described as a finite state machine. In Estelle, a protocol system is specified as a hierarchically structured system of modules which interchange messages (called interactions) through bidirectional links between their ports (called interaction points). Both the hierarchy of modules and the structure of links may change over time, thereby making the system a dynamic one. Existing methods of verifying Estelle specifications involve translating the specifications into another form, such as finite state machines or Petri nets, for which tools of verification have already been implemented. Their limitations are that they have to be based on a variant of Estelle, they impose some restrictions on the specifications to be verified, and they do not handle dynamic behaviour and exported variables [10, 15, 16]. We have developed a technique [18, 19, 23] of translating a standard Estelle specification, including all dynamic behaviour, exported variables and Estelle statements, into a Numerical Petri Net specification. Using this technique, each Estelle module, consisting of a module header definition and a module body definition, is modelled independently as an indivisible NPN net which is very compact. Nearly all single elements of an Estelle module can be kept in NPN. Both data flow and control flow of a protocol system are combined in this NPN-based model, and the data flow in particular is completely expressed in this model. This paper describes how the ISO RTSE protocol [5, 6] can be modelled using Estelle and the process of analysing such specifications. The analysis is done by first transforming the Estelle specifications into NPNs using the techniques we have developed, and then the NPN specifications are analysed by a proven automated verification tool, PROTEAN. 2.Estelle To avoid the ambiguities inherent in specifications written in natural language and to verify and test the specifications formally for correctness and completeness, ISO developed two Formal Description Techniques (FDTs), namely Estelle [7, 8, 13] and LOTOS [2], for the description of ISO services and protocols. Both FDTs achieved international standard (IS) status in 1989. Estelle is chosen as the FDT to formally specify communication protocols and services for the following reasons: Estelle is very easy to learn, even for the beginner. This is mainly due to the well-known concept of extended finite state machines (EFSMs). We consider it much more difficult to learn LOTOS [21]. Traditionally, English text and state tables have been used for the informal description of standard protocols. State tables and Estelle description are strongly related, since both are based on EFSM. This provides us with a high degree of similarity between the informal and the formal descriptions [9]. Semi-automatic generation of implementations from formal descriptions is one of the most interesting applications of FDTs. Such a technique makes the implementation process more efficient and reduces the risk of errors and incompatibilities. Estelle is well suited for this purpose due to its language concept which is closer to implementation [17]. Estelle is supported by various tools for syntax and static semantics checking, simulation and implementation [14]. Modelling power of Estelle The framework of an Estelle specification is a set of cooperating entities called modules, communicating with each other by exchanging information through channels and by restricted sharing of variables (exported variables). The behaviour of a module and its internal structure are specified respectively by the set of transitions (of an extended finite state machine model) that the module may perform and by the definition of submodules (child modules) of the module together with their interconnections. Each module has a number of input/output access points called interaction points. There are two types of interaction points: external and internal. A channel, which is associated with each interaction point, defines two sets of interactions that can be sent over the channel. These two sets consist respectively of a list of interactions which can go out and a list of those which can come in through a particular interaction point. Interactions are abstract messages exchanged with the module environment (through external interaction points) and with child modules (through internal interaction points). Informally a module is represented graphically as a rectangle, with points indicating interaction points, and arrows indicating the names and directions of interactions through those points. Figure 1 gives an example of the representation of a module in a graphical manner and in Estelle syntax with the module name (Entity) and its class attribute (Process), the name of the interaction points (P1 and P2), and their associated interactions (Request, Indication, Response, Confirm, Data, P_ack, N_ack). The operation of each module is determined by a number of transition statements which describe an extended finite state machine (EFSM). Figure 2 gives an example of translation from an EFSM transition to an Estelle transition. The transition enables a change of state from IDLE to WAIT under the conditions that there is the interaction "ConnectRequest" at the interaction point "P1" as specified in the WHEN clause, and the predicate "Free" is true as specified in the PROVIDED clause. The result of the transition execution as specified in the transition block (between BEGIN and END) is that the interaction "ConnectIndication" is created and sent through the interaction point "P2". Figure 1: Representation of a module in (a) a graphical manner and (b) Estelle syntax Figure 2: An example of transition from an EFSM transition to an Estelle transition 3.RTSE The RTSE (Reliable Transfer Service Elements) protocol [5, 6] is an application layer protocol which ensures that each application-protocol-data-unit (APDU) is completely transferred between application-entities (AEs) exactly once, or that the sending AE is warned of an exception. RTSE attempts to recover from communication and end-system failure and minimizes the amount of retransmission needed for recovery. The standard mapping of RTSE on to the underlying protocol stack is via ACSE and the presentation service. RTSE is organised into various services such as open, close, transfer, turn-please, turn-give, abort-by-provider and abort-by-user. The RTSE user (e.g. ROSE) must first use the open service, which uses ACSE to establish an application association. At the end, only the association-initiating user invokes the close service to terminate the association. As well as graceful termination of the association, RTSE includes the usual abort services. Once the association is set up, RTSE operates by means of sending some messages via the transfer service. Each transferred message is confirmed, the response variant indicating success or failure. In case of failure, the transfer can be repeated. The other main feature of RTSE is the concept of the turn. The turn gives permission to transfer a APDU to one RTSE entity at a time, and to terminate the association. In this paper, however, it is not possible to present all services of the RTSE protocol. Instead, the turn-please and turn-give services are given to demonstrate how to specify them in Estelle, and how to translate them into NPNs for verification. Turn-please The turn-please service is used by an RTSE user to request the turn, if it does not already possess the turn. This service is a non-confirmed service. The service is driven by the following events: The requesting RTPM, after receiving an RT-TURN-PLEASE request from the RTSE user (requestor), issues a P-TOKEN-PLEASE request primitive. If the priority parameter is present in the RT-TURN-PLEASE request primitive, an RT-TURN-PLEASE (RTTP) APDU is formed from the priority parameter value and transferred as User-data of the P-TOKEN-PLEASE request primitive. The accepting RTPM, after receiving a P-TOKEN-PLEASE indication primitive, issues an RT-TURN-PLEASE indication primitive to the RTSE user (acceptor). If an RTTP APDU is transferred as User-data of the P-TOKEN-PLEASE indication primitive, the RT-TURN-PLEASE indication primitive parameter is present and derived from the RTTP APDU. Note that priority zero is the highest priority and is reserved for the action of releasing an application-association. If the priority parameter is absent, priority zero is assumed. Turn-give The turn-give service enables an RTSE-user to relinquish the turn to its peer. It may do so only if it possesses the turn and there is no outstanding RT-TRANSFER confirm primitive. This service is a non-confirmed service. The service is driven by the following events: The requesting RTPM, which possesses the turn and receives an RT-TURN-GIVE request primitive from the RTSE user (requestor), issues a P-CONTROL-GIVE request primitive and becomes the receiving RTPM. The accepting RTPM, after receiving a P-CONTROL-GIVE indication primitive, issues an RT-TURN-GIVE indication primitive to the RTSE user (acceptor). Note that the turn-give service has no parameters. 4.Modelling RTSE in Estelle The formal specification in Estelle of RTSE was derived from the ISO documents [5, 6] and comprises two major parts. The first part describes data types and structures used by RTSE, i.e., Protocol Data Units (PDUs) and Abstract Service Primitives parameters (ASPs). The PDUs' part is the information exchange between peer protocols; and the ASPs' part is concerned with the structure and content of service primitives. The second part defines the module representing the behaviour of the RTSE ASE (Application Service Element). Specification model Figure 3 shows the environment and the module structure in which the Estelle specification of RTSE protocol has been considered. There are two sides: one is the requestor and the other the acceptor. Each side consists of four modules: USER, RTPM, ACPM and PS. The USER module represents an application above RTSE. The ACPM module represents the association control protocol machine which provides services for the establishment and release of associations. The PS module represents the presentation service provider which provides transfer services to the RTPM and ACPM modules. The RTPM module represents the RTSE protocol machine. In Figure 3, there are four RTSE service primitives: RT_TPreq stands for RT-TURN-PLEASE request RT_TPind stands for RT-TURN-PLEASE indication RT_TGreq stands for RT-TURN-GIVE request RT_TGind stands for RT-TURN-GIVE indication. And there are four Presentation service primitives: P_TPreq stands for P-TOKEN-PLEASE request P_TPind stands for P-TOKEN-PLEASE indication P_CGreq stands for P-CONTROL-GIVE request P_CGind stands for P-CONTROL-GIVE indication. The main body of the Estelle specification in Appendix A represents the specification model in Figure 3. Estelle description of PDUs and ASPs Estelle adopts from Pascal the notation for data type and structure definitions, whereas the ISO specification of the RTSE protocol uses ASN.1 [3] to define its PDUs. ASN.1 is used to specify the structure and contents of PDUs, independent of how they are to be represented for the purpose of transmission. ASN.1 is coupled with Basic Encoding Rules (BER) [4]. When a PDU is to be transmitted, it is converted into its transfer syntax form using BER. Given the need to express the RTSE protocol in Estelle, it is necessary to translate ASN.1 definitions of PDUs and service primitives into Estelle. For some data types, translation between ASN.1 and Estelle can be achieved simply by direct mappings. However, there are some ASN.1 types which require the design of special Estelle/Pascal structures for the translations. Table 1 gives the translation from RTSE APDUs specified in ASN.1 for the turn-please and turn-give services to those in Estelle. Table 2 summarizes thee basic translation between ASN.1 types and Estelle types. Some further explanation can be found in [24]. Figure 3: Specification model Estelle description of RTSE behaviour In the ISO document [5, 6], the behaviour of the RTSE protocol is described in state tables and in English text. The EFSM and state table of RTPM for the turn-please and turn-give services are given in Figure 4. The transition part of the Estelle module body is derived from the state table and the Estelle description of PDUs and ASPs. Appendix A gives the Estelle specification of the module body RTPM, which is derived from the EFSM and state table in Figure 4. Figure 4: An EFSM and a state table of RTPM for the turn-please and turn-give services

ASN.1 Type	Estelle Type
INTEGER / BITSTRING Atype ::= [[TAG]](INTEGER|BITSTRING) { t1(value1), . . . tn(valuen) }	CONST BitStrLen = any INTEGER; t1 = value1; . . . tn = valuen; TYPE BIT = 0 .. 1; BitsType = ARRAY[0 .. BitStrLen] Of BIT; BITSTRING = RECORD bits : BitsType; length : 0 .. BitStrLen; END; AType_Type = INTEGER | BITSTRING;
ENUMERATED AType ::= [[TAG]] ENUMERATED {t1(value1), ..., tn(valuen)}	TYPE AType_Type = (t1, ..., tn);
SEQUENCE / SET Structure AType ::= [[TAG]] (SEQUENCE | SET) { id1[t1]T1, id2[t2]T2 OPTIONAL, . . . idn[tn] IMPLICIT Tn }	TYPE AType_Type = RECORD id1 : T1 id2 : RECORD CASE present : BOOLEAN OF TRUE : (T1Opt : T2); FALSE : (); END; . . . idn : Tn END;
CHOICE Structure AType ::= [[TAG]] CHOICE { id1[t1]T1, id2[t2]T2, . . . idn[tn]Tn }	TYPE AType_TAG_TYPE = (id1_TAG, id2_TAG, ..., idn_TAG); AType_Type = RECORD CASE tag : AType_TAG_TYPE OF id1_TAG : (id1 : T1); id2_TAG : (id2 : T2); . . . idn_TAG : (idn : Tn); END;
SET OF / SEQUENCE OF Structure AType ::= [[TAG]] (SEQUENCE | SET) OF T	CONST SEQ_MAX = any INTEGER; SET_MAX = any INTEGER; TYPE AType_Type = RECORD val : array[1 .. (SEQ_MAX | SET_MAX)] OF T; len : 0 .. (SEQ_MAX | SET_MAX); END;

Table 2: Data Type Translation between ASN.1 and Estelle

The specification in Appendix A, however, assumes that the priority parameter is present in the RT-TURN-PLEASE request primitive. 5. Numerical Petri Nets (NPNs) Numerical Petri Nets (NPNs), developed originally by Symons [25], are one of the many extensions of Petri nets. It has been found possible with NPNs to retain the basic principles, symbols and modes of operation of Petri nets, while adding a considerable amount of modelling convenience. We were motivated to choose NPNs for modeling Estelle by the following characteristics: their appealing presentation in a more compact form of diagram; their strong theoretical foundation; their expressive power in concurrency and nondeterminism; the number of analytic techniques available for examining properties of protocol specification; and the number of automated tools available for verification purposes. NPNs have been successfully used in modelling some ISO protocols [11, 22]. They contain the following extensions to Petri Nets: Tokens can have any finite number of attributes, each of which may be of one of several different types; Global variables can be associated with the net; The transition enabling conditions refer not only to the tokens in the input places but also to the global variables; The firing of a transition not only removes tokens from the input places and inserts new tokens into the output places, but may change the values of the global variables. 6. A Verification Process As shown in Figure 5, starting from protocol specifications written in natural language, the verification process comprises the following steps: Step 1 : Formal specification Protocol specifications written in natural language plus state tables are formally specified in Estelle. The objective of this step is to obtain an unambiguous description that can serve as input to the next step. Syntax and static semantic checking of the specifications is performed in this step. The Portable Estelle Translator (PET) from NIST is used for such checking. Step 2 : Translating into Numerical Petri Nets In order to enable communication protocols specified in Estelle to be verified, our approach is to use an NPN-based model as a core formalism to complete the verification process. The details of translating an Estelle specification into a Numerical Petri Net specification can be found in [18, 19, 23]. Here we give an outline of how this is done. All module bodies, all the external interaction points, the exported variable declaration part in the module header of any corresponding module body, and all the internal interaction points of the module body become places in an NPN, while transitions in the module body become transitions in an NPN. Tokens are used to model the dynamic behaviour of Estelle, to model interactions exchanged with the module environment (through external interaction points) and with child modules (through internal interaction points), and to model exported variables shared between a parent module and its child module. Each token is a collection of attributes. The first attribute is used to identify the type of token. There are six types of token: control, state, in-message, out-message, link and exported. With respect to Estelle dynamic operations, the control tokens can also be further divided into 7 subtypes: init, connect, attach, release, terminate, disconnect and detach. Tokens in NPN places indicate that the message and state belonging to the module instance will be processed by one of the enabling transitions in the module body. Transitions are fired to represent transitions being executed in the module body. The net result is the exchange of tokens or interactions from place to place, and a new marking is obtained. There are a number of merits of this approach over existing ones. It is based on standard Estelle, rather than a variant or a subset of Estelle. Almost all single elements of Estelle can be kept in a transformed NPN. All dynamic behaviours, exported variables and Estelle statements can be modelled by NPNs. Both data flow and control flow of protocol systems are contained in this NPN-based model. An NPN net, as a result of translating an Estelle module, is indivisible and very compact. However, the Estelle priority and delay clauses, dynamic loops in a transition block, and the systemprocess attribute are not supported using this approach. Table 3 gives a brief mapping of Estelle components onto NPNs. Step 3 : Analysis and result interpretation After translating an Estelle specification into NPNs, the behaviour of the protocol is analyzed using the automated verification tool, PROTEAN (PROTocol Emulation and Analysis) [12], developed by Telecom Australia. The verification technique employed by PROTEAN is reachability analysis. After obtaining the verification results, if there is any error we return to Step 1; otherwise we move to the implementation phase. Translating RTSE into NPNs In our approach, each Estelle module is translated independently into an indivisible NPN net and later all of these nets are integrated. In the NPN net representing the module RTPM, there are four NPN places: RTPM_body representing the module body identifier; and RTPM_USAP, RTPM_PSAPD and RTPM_ASAP representing the associated interaction point identifiers USAP, PSAPD and ASAP respectively. Eight Estelle transitions for the turn-please and turn-give services in Appendix A are translated to be eight NPN transitions; and there are two additional NPN transitions, InitRTPM1 and InitRTPM2, because there are two different initialization parts: one for id equal to 1 and the other for id equal to 2. Figure 6 gives the NPN net of the RTSE turn-please and turn-give services. Finally, this NPN net is integrated with the NPN net representing the module USER, the NPN net representing the module ACPM, and the NPN net representing the module PS. The details of integration can be found in [18, 19, 23]. Figure 5: A verification process for Estelle Figure 6: An NPN graph for the RTSE turn-please and turn-give services

Estelle	NPN
a module body identifier	a place
an external interaction point	a place
an internal interaction point	a place
a transition	a transition
a from-clause	an enabling condition
a provided-clause	an enabling condition
a transition block	transition operations
a when-clause	an input arc with an in-message token
an output-statement	an output arc with an out-message token
an exported-variable-declaration part	a place
the module-initialization part	a transition
a module instance and its state	a state token
a connection status	a link token
an attachment status	a link token
a set of exported variables	an exported token
an init-statement	an output arc with an init token
a release-statement	an output arc with a release token
a terminate-statement	an output arc with a terminate token
a connect-statement	an output arc with a connect token
an attach-statement	an output arc with an attach token
a disconnect-statement	an output arc with a disconnect token
a detach-statement	an output arc with a detach token

Table 3: Mapping of Estelle components onto NPNs

NET: RTSE TURN-PLEASE AND TURN-GIVE SERVICES 22 Sep 94 15:19:54 SIMULATION OF THE NET - RTSE TURN-PLEASE AND TURN-GIVE SERVICES PART ONE - THE REACHABILITY GRAPH
Markings	Transition	Module-instance
1 --> 2	RT_TPreqSTA22	UB
2 --> 3	P_TPreqSTA22	RTPMB
3 --> 4	P_TPind1	PPM
4 --> 5	RT_TPindSTA11	RTPMA
5 --> 6	RT_TGreqSTA11	UA
6 --> 7	P_CGreqSTA11	RTPMA
7 --> 8	P_CGind2	PPM
8 --> 9	RT_TGindSTA22	RTPMB
9 --> 10	URT_TGindSTA22	UB
10 --> 11	RT_TPreqSTA12	UA
11 --> 12	P_TPreqSTA12	RTPMA
12 --> 13	P_TPind2	PPM
13 --> 14	RT_TPindSTA21	RTPMB
14 --> 15	RT_TGreqSTA21	UB
15 --> 16	P_CGreqSTA21	RTPMB
16 --> 17	P_CGind1	PPM
17 --> 18	RT_TGindSTA12	RTPMA
18 --> 1	URT_TGindSTA12	UA

Figure 7: A reachability graph generated by PROTEAN

Verification of RTSE After having obtained the global NPN net of the RTSE protocol by translating from the Estelle specification, the behaviour of the protocol is verified and simulated using the automated verification tool, PROTEAN (PROTocol Emulation and Analysis) [12]. With PROTEAN, NPN specifications may be created, edited, stored, combined with other NPNs, structured, listed, displayed, and analyzed. PROTEAN provides a variety of analysis modules. It includes interactive simulation, exhaustive reachability analysis, and several directed graph analysis facilities. Reachability graphs can be automatically generated and displayed. Based on the reachability graph, there are facilities that could determine deadlocks and livelocks. Language analysis is used to reduce the reachability graph to a language graph which can be used to study sequences of key system events and allows a protocol to be compared with its service specification. Cycle graphs can also be generated , allowing users to highlight interesting cycles on reachability graphs and language graphs. Other facilities are provided to debug the specification. If a problem of the protocol is found, sequences of events which lead to undesired behaviour can be traced. Figure 7 gives the reachability graph file generated by PROTEAN. 7. Conclusions In this paper, we have described how to model the ISO RTSE protocol using Estelle. Based on an extended finite state machine, Estelle is very easy to learn. The nature of Estelle also makes it easy to translate state tables combined with English specifications into formal specifications. It is concluded that Estelle is an FDT which can be very conveniently used for the formal specification of communication protocols. We have also presented the process of verifying the RTSE Estelle specifications. The process is based on translating the Estelle specifications into NPNs which can then be verified by the proven automated verification tool, PROTEAN. In this analysis exercise, there was no deadlock and no actual livelock uncovered. Estelle enables the specifications to be analysed. Thus, it satisfies two of the main objectives of ISO in developing FDTs : to enable unambiguous, clear and precise descriptions of OSI standards to be written; and to allow such descriptions to be verified for consistency and correctness. The translation from the RTSE Estelle specification to the NPN specification is done automatically using the Estelle-to-NPN translator, which is a part of EVEN (Estelle Verification Environment using NPNs) [20] developed at La Trobe University, Australia. The translator will generate intermediate codes that allow verification to be performed by PROTEAN. Any error detected during the verification process is reported by EVEN in Estelle format. By using EVEN, the user does not need to know anything about the translation; and the user is also able to understand the errors detected more readily as they are described in Estelle format. To conclude, our method described here provides a viable approach to verifying real ISO protocols specified in standard Estelle. References ISO/TC97/SC21/N1534, Information Processing Systems - Open Systems Interconnection - Guidelines for the Application of FDTs to OSI, Geneva, September (1986). ISO8807, Information Processing Systems - Open Systems Interconnection - LOTOS (Formal Description Technique based on the Temporal Ordering of Observational Behaviour), (1989). ISO8824, Information Processing Systems - Open Systems Interconnection - Specification of Abstract Syntax Notation One (ASN.1), IS 8824, (1990). ISO8825, Information Processing Systems - Open Systems Interconnection - Specification of Basic Encoding Rules for ASN.1, IS 8825, (1990). ISO/IEC 9066-1, Information processing systems - Text communication - Reliable Transfer Part 1: Model and service definition, (1989). ISO/IEC 9066-2, Information processing systems - Text communication - Reliable Transfer Part 2: Protocol specification, (1989). ISO9074, Information Processing Systems - Open Systems Interconnection - ESTELLE (Formal Description Technique based on an Extended State Transition Model), (1989). ISO/IEC JTC 1/SC 21, Information Processing Systems - Open Systems Interconnection - ESTELLE - A FDT Based on an Extended State Transition Model - Proposed Draft Amendment 1: Estelle Tutorial, (1991). C. Andrae, R. Gotzhein and S. Sedillot, An Evolutionary Approach to the Development of Complex Protocol Standards, in: Protocol Specification, Testing and Verification, XIII, eds. A. Danthine, G. Leduc and P. Wolper (North-Holland, Amsterdam, 1993). P. Azema, J.C. Lloret, G. Papapanagiotakis and F. Vernadat, ESTELLE Validation and PROLOG Interpreted Petri Nets, in: The Formal Description Technique Estelle, eds. M. Diaz, J.-P. Ansart, J.-P. Courtiat, P. Azema and V. Chari (North-Holland, Amsterdam, 1989, 273-302). J. Billington, Specification of the Transport Service using Numerical Petri Nets, in: Protocol Specification, Testing and Verification, II, ed. C. Sunshine (North-Holland, Amsterdam, 1983). J. Billington, G.R. Wheeler and M.C. Wilburham, PROTEAN: A High-level Petri Net Tool for the Specification and Verification of Communication Protocols, IEEE Transactions on Software Engineering 14(3) (1988), 301-316. S. Budkowski and P. Dembinski, An Introduction to Estelle: A Specification Language for Distributed Systems, Computer Networks and ISDN Systems 24 (1987), 3-23. S.T. Chanson, A.A.F. Loureiro and S.T. Vuong, On tools supporting the use of formal description techniques in protocol development, Computer Networks and ISDN Systems 25 (1993), 723-739. J.P. Courtiat and P. de Saqui-Sannes, ESTIM: an integrated environment for the simulation and verification of OSI protocols specified in Estelle*, Computer Networks and ISDN Systems 25 (1992), 83-98. V. Dimitrov and A. Petkov, Verification Oriented Estelle Specification of Communication Protocols, in: Research into Networks and Distributed Applications, ed. R. Speth ( North-Holland, Amsterdam, 1988, 953-960). R. Foedisch, T. Held and H. Koenig, A PROTOCOL DEVELOPMENT ENVIRONMENT BASED ON ESTELLE, in: Information Network and Data Communication, IV, eds. M. Tienari and D. Khakhar (North-Holland, 1992, 121-141). A. Jirachiefpattana, Numerical Petri Nets Approach to Estelle Specification Verification, Ph.D. Thesis, School of Computer Science and Computer Engineering, La Trobe University, Melbourne, Australia (September 1995). A. Jirachiefpattana and R. Lai, Verification Results for the ISO ROSE Protocol Specified in Estelle, in: Protocol Specification, Testing and Verification, XIV, eds. S.T. Vuong and S.T. Chanson (Chapman & Hall, 1995). A. Jirachiefpattana and R. Lai, EVEN : A Software Environment for Estelle Specification Verification, to appear in The Journal of Systems and Software, Elsevier Science B.V. North-Holland (1997). R. Keller, S. Fischer and W. Effelsberg, Implementing Movie Control, Access and Management - from a Formal Description to a Working Multimedia System, in: Proceedings of the 14th International Conference on Distributed Computing Systems (IEEE Computer Press, 1994). R. Lai, T.S. Dillon and K.R. Parker, Application of Numerical Petri Nets to Specify ISO FTAM Protocol, in: Proceedings of the 1989 Singapore International Conference on Networks (1989). R. Lai and A. Jirachiefpattana, Verification of ISO ACSE Protocol Specified in Estelle, Computer Communications 17(3) (1994) 172-188. A. Lo and R. Lai, Integrating Estelle and ASN.1 for Automatic Implementation, in: Formal Description Techniques, FORTE'93 (Elsevier Science Publishers B.V., North-Holland, 1994). F.J.W. Symons, Modelling and analysis of communication protocols using Numerical Petri Nets, PhD thesis, Dep. Elec. Eng. Sci., Univ. Essex, Telecommun. Syst. Group Rep. 152 (1978). Appendix A Estelle Specifications of RTSE turn-please and turn-give services Specification RTSE_Spec; default individual queue; timescale seconds; { Constant and Type Declarations } #include 'type.e' { Channel Definition } #include 'channel.e' { USER Module Definition } #include 'user.e' { ACPM Module Definition } #include 'acse.e' { PS Module Definition } #include 'ps.e' {*RTPM Module Header Definition*} module RTPM_mod systemactivity (id : integer); ip USAP : RTSE_Channel_type (provider); ASAP : ACSE_Channel_type (user); SAPD : Pres_Data_Channel_type (user); end; {* RTPM Module Body Definition *} body RTPM_body for RTPM_mod; var RTapdu : RTSE_apdus_Type; USapdu : USER_apdus_Type; state STA11, (*associated; Initiator holding TURN*) STA12, (*associated; Initiator not holding TURN*) STA21, (*associated; Responder holding TURN*) STA22; (*associated; Responder not holding TURN*) initialize to STA11 PROVIDED id=1 begin end; to STA22 PROVIDED id=2 begin end; trans FROM STA12 TO STA12 WHEN USAP.RT_TPreq NAME P_TPreqSTA12: begin RTapdu.tag := rttp_apdu_TAG; RTapdu.rttp_apdu :=Event.priority; Output PSAPD.P_TPreq (RTapdu); end; trans FROM STA22 TO STA22 WHEN USAP.RT_TPreq NAME P_TPreqSTA22: begin RTapdu.tag := rttp_apdu_TAG; RTapdu.rttp_apdu := Event.priority; Output PSAPD.P_TPreq (RTapdu); end; trans FROM STA11 TO STA11 WHEN PSAPD.P_TPind NAME RT_TPindSTA11: begin USapdu.priority := Event.rttp_apdu; Output USAP.RT_TPind (USapdu); end; trans FROM STA21 TO STA21 WHEN PSAPD.P_TPind NAME RT_TPindSTA21: begin USapdu.priority := Event.rttp_apdu; Output USAP.RT_TPind (USapdu); end; trans FROM STA11 TO STA12 WHEN USAP.RT_TGreq NAME P_CGreqSTA11: begin Output PSAPD.P_CGreq; end; trans FROM STA21 TO STA22 WHEN USAP.RT_TGreq NAME P_CGreqSTA21: begin Output PSAPD.P_CGreq; end; trans FROM STA12 TO STA11 WHEN PSAPD.P_CGind NAME RT_TGindSTA12: begin Output USAP.RT_TGind; end; trans FROM STA22 TO STA21 WHEN PSAPD.P_CGind NAME RT_TGindSTA22: begin Output USAP.RT_TGind; end; end; (* End of RTPM_body *) {* Main body of RTSE_Spec Specification* } (* Module Variable Declaration Part *) modvar UA, UB : USER_mod; RTPMA, RTPMB : RTPM_mod; ACPMA, ACPMB : ACPM_mod; PPM : PS_mod; (* Main Initialization Part *) initialize begin init UA with USER_body(1); init UB with USER_body(2); init RTPMA with RTPM_body(1); init RTPMB with RTPM_body(2); init ACPMA with ACPM_body(1); init ACPMB with ACPM_body(2); init PPM with PS_body; connect UA.USAP to RTPMA.USAP; connect UB.USAP to RTPMB.USAP; connect RTPMA.ASAP to ACPMA.ASAP; connect RTPMB.ASAP to ACPMB.ASAP; connect RTPMA.PSAPD toPPM.PSAPD[1]; connect RTPMB.PSAPD to PPM.PSAPD[2]; connect ACPMA.PSAPA to PPM.PSAPA[1]; connect ACPMB.PSAPA to PPM.PSAPA[2]; end; end. (* End of RTSE_Spec *)