(Jürgen M. Schneider (Auth.) ) Protocol Engineeri PDF
(Jürgen M. Schneider (Auth.) ) Protocol Engineeri PDF
(Jürgen M. Schneider (Auth.) ) Protocol Engineeri PDF
Schneider
Protocol Engineering
Informatics
J. M. Schneider
Protocol Engineering
A Rule-based Approach
W. Bibel
Automated Theorem Proving
E. Eder
Relative Complexities of First Order Calculi
F. KurfeB
Parallelism in Logic
Vieweg - - - - - - - - - - - - - -
JOrgen M. Schneider
Protocol Engineering
A Rule-based Approach
II
vleweg
Die Deutsche Bibliothek - CIP-Einheitsaufualune
Foreword
It is now over twenty years since the first efforts were made to interconnect
computers for the exchange of data. In the 1970s proprietary networking
architectures, such as IBM's SNA, were developed and installed at many
customer sites worldwide. At the same time the ARPANET in the United States
became a research vehicle providing many new insights, in particular into
packet switching technology and routing algorithms.
Preface
Not long ago, the interconnection of computer systems was a highly
complex task requiring considerable effort. Today, computer networks have
become part of our daily life and are of vital importance for many organ-
izations. Although the speed of this remarkable evolution has always been
high, the future prospects of computer communication encompass an
increasing number of new applications that are even more breathtaking
than those developed in the past, including, for example, multimedia docu-
ment exchange, video conferences, or cooperative work over large
geographical distances. However, despite the enormous advances in phys-
ical interconnection and transmission technology, the complexity of real-
izing these applications is still high due to the growing demands for
extensive cooperation between heterogeneous distributed systems based
on increasingly powerful communication services.
Acknowledgements
This book is the published version of my doctoral dissertation. which I com-
pleted at the University of Kaiserslautern. in Germany. in 1991. The thesis
was written while I was a PhD student at the IBM European Networking
Center (ENC) at Heidelberg. Germany. between 1988 and 1991. During this
time. I enjoyed an extremely stimulating atmosphere and was able to
extend my personal knowledge considerably in a number of different ways.
I am grateful to Dr. Lothar Mackert for enabling this opportunity for me. for
all the inspiring conversations we had and. in particular. for his trust and
friendship over the years. I am also indebted to my advisor Prof. Dr. Jurgen
Nehmer. By attending his classes I learned most of what I know of distrib-
uted systems and his continuous support and guidance has always been a
source of encouragement. Many thanks also go to Prof. Dr. Wolfgang
Effelsberg for the help and constructive comments I received during and
after his time at the ENC.
My thanks and recognition are also richly deserved by Dr. Georg Zorntlein.
who went through this text several times. His accuracy. patience and tech-
nical contributions enormously improved the quality of the thesis. My ideas
probably never could have been formulated in an understandable way
without the generous help of Dr. Mark Mattingley-Scott. who tried hard to
correct my English wording. The fact that he is already aware of my grati-
tude because he also had to read this acknowledgement section is a
typical case of how far generosity can be exploited. Among the many
other people who contributed to the successful completion of this work I
would particularly like to thank my fellow PhD students at the ENC. I appre-
Preface ix
ciated learning about the Dutch way of life from Rolf Velthuys during our
conference visits and by sharing the same room for three years, which was
a unique experience that I look forward to telling my grandchildren during
cold evenings by the fire. It was also a pleasure for me to recognize that I
was never observed more closely and imitated more amusingly than by
Udo Bar at the celebration of my PhD. Finally, Dr. Stefan Pappe showed us
all how to manage PhDs the easy way.
It was the character of the daily work at the ENC, in an international envi-
ronment with students coming from a number of different countries that
made the time spent there particularly rewarding. Many thanks for their
contribution to my work go to B. Bar, F. Clarius, W. Eschebach, H. Janssen, 1.
Mangold, D. Miller, J. Monnery, S. Roorda, U. Scheere, E. Spriet and 1.
Stullich. Acting as their supervisor was valuable for my personal education,
which was also permanently supported by Prof. Dr. Gunter Muller, who
headed the ENC at that time, and kept me under constant pressure to
develop my abilities beyond those of an acceptable football player. I also
acknowledge the help of my colleagues at the University of Kaiserslautern
and the good relationship we maintained. I would particularly like to
mention Ralf Reske, who organized social events very well. My thanks also
go to Dr. Reinhard Gotzhein and Prof. Dr. Horst Muller for their assistance in
the formal semantics part of the thesis.
My family has always been the backbone of my life. At times, they contrib-
uted more than I did to the success of this work. My parents always sup-
ported me and made my studies possible. My constant preoccupation with
the problems of my thesis and the many hours I spent writing at my desk
required a lot of love and patience from my wife, Rosemarie. I gratefully
acknowledge her tolerance regarding my sometimes frantic behavior, as
well as all the highest priority interrupts generated by our son Jens.
I dedicate this book to the memory of my cousin, Dr. Gerhard Wagner, who
has been a model for me all my life and without whose encouragement I
would probably have never started this work. It was God's will to call him
before he could see its completion.
Contents
--------------------_.
1 Introduction 1
1.1 Overview 2
1.2 Communication Systems 5
1.2.1 Structuring Principles 6
1.2.2 Architectural Concepts 12
1.3 Protocol Engineering 14
1.3.1 Life-cycle 15
1.3.2 Tool Support 17
Figures
1. Communication system interconnecting open systems 6
2. Communication system as a collection of subsystems 7
3. Decomposition of communication services . . . . . . . . . . . . .. 8
4. Layered communication system as defined by the OSI Basic
Reference Model 9
5. An (N)-Iayer in a layered communication system 9
6. Mapping between data units in adjacent layers . . . . . . . . . .. 11
7. Formal development process 16
8. X.25 protocols ............. 23
9. Use of X.25 to provide the OSI connection-oriented network service 24
10. Network service primitives 24
11. X.25 packets 24
12. X.25 PLP CALL REQUEST and DATA packet formats 26
13. X.25 PLP call setup state diagram 28
14. Time sequence diagram for call setup in the X.25 PLP 28
15. X.25 DTE in Estelle 35
16. Estelle module header and channel definitions for X.25 PLP 35
17. Creating an X_25_DTE in Estelle ......... 36
18. Estelle ("PASCAl") type definitions for network SPs and X.25 PlP
packets ........ 36
19. Estelle module body for X_25_DTE (in part) ............... 37
20. X.25 DTE in SOL 40
21. SOL process for X_25_DTE ....... 41
22. SOL type definitions for network SPs and X.25 PlP packets ... 42
23. High-level Petri net graphical representation .......... 45
24. Modelling different communication modes with Petri nets 47
25. X.25 DTE as Numerical Petri Net 48
26. Representation of agents in a process algebra 50
27. Syntax of behavior expressions in Basic LOTOS ............... 52
28. X.25 DTE in LOTOS 54
29. LOTOS process for X_25_DTE ............................... 54
30. LOTOS (ACT ONE) type definitions for network SPs and X.25 PLP
packets ......... 55
31. X.25 DTE in Z 59
32. Z operation schema for X_25_DTE 59
xiv
33. Z type definitions for network SPs and X.25 PLP packets 61
34. Abstract, local and transfer syntax in communication systems 67
35. ASN.1 module definition frame example ....... 69
36. Simple type examples ... . . . . . . . . . . . . . . . . . . . . . .. 72
37. Type examples constructed with SEQUENCE ..................... 75
38. Type examples constructed with SET .... . ....... 76
39. Type example constructed with SEQUENCE OF ................... 77
40. Type example constructed with SET OF " ..... 78
41. Type examples constructed with CHOICE ... 80
42. Subtype examples 81
43. Basic encoding rules .... . ......................... 84
44. Encoding of the identifier field 85
45. CRS network service configuration ............ 87
46. CRS specification of the network service configuration . . . . . . . .. 87
47. Syntax of rule system specifications . . . . . . . . . . . . . . . . . . . .. 89
48. CRS specification of X.25 DTE .......................... 89
49. Syntax of rules ............... . . . . . . . . . . . . . . . .. 91
50. CRS specification of X.25 PLP call setup initiation ....... . 91
51. CRS specification of X.25 PLP duplex and expedited data transfer 93
52. Syntax of event expressions 94
53. Syntax of gate specifications 94
54. CRS specification of X.25 PLP gates ... 95
55. CRS specification of X.25 window mechanism 97
56. Syntax of contexts ... . . . . . .. 98
57. Syntax of views ....... . ............... 98
58. Context and view structure of the X.25 PLP specification in CRS .... 99
59. Contexts and views example for X.25 PLP data transfer specified
with CRS .................... . . . . . .. 100
60. Syntax of ADT specifications '" 102
61. Syntax of abstract operations .. 102
62. CRS specification of ADT DataQueue 103
63. Example of LOTOS semantics expressed as "PROLOG" rules ...... 131
64. Example control clause in a logic program . . . . . . . . . . . . . . . .. 135
65. Distributed test configuration " . . . . . . .. .......... 146
66. CRS implementation concepts 151
67. X-ASN.1 implementation concepts ............... 154
68. Structure blocks ..... . . ..... 155
Figures xv
69. structure tree for the X.25 CAll REQUEST packet type 156
70. Structure trees ............. . 157
71. Data blocks ........ . 157
72. Data tree for an X.25 CAll REQUEST packet 158
73. Data trees 159
74. Rule sets of the CRS inference machine 160
75. WES set of the CRS inference machine 163
76. Run set of the CRS inference machine 163
77. Protocol automaton of the synchronous CRS gate machine 165
78. Protocol automaton of the asynchronous CRS gate machine 168
79. Architecture of the local CRS runtime environment 171
80. Rule system control block 173
81. Rule control block 173
82. Gate control block 175
83. Event control block 175
84. Compiling CRS specifications into executable form 177
85. Example of X-ASN.1 extended "C++" code 178
86. "C++" classes for X-ASN.1 expressions and variables 179
87. Example gate header file 181
88. Example gate source file ..... . ..... 182
89. Example rule system header file 184
90. Example rule system source file 185
91. Dependency graph example for conjunctions 190
92. Dependency graph for disjunction 191
93. Example rule functions 192
94. Example ADT header file 194
95. Example ADT source file 195
96. Example configuration source file 196
97. Integrated tools environment . . .. 199
98. CRS and X-ASN.1 based kernel . . .. 201
99. Rule-based shell .. 205
100. State-based shell 207
101. Event-based shell ...... . . ........... 209
102. Behavior simulator ...... . 213
103. Test case development tool 216
104. Test case validation tool .. 220
Figures xvii
1.1 Overview
The complexity of the services expected from a communication system
have grown steadily over the last decade. Today's communication systems
not only have to provide access to various physical media and cater for
reliable data transfer, but also support remote operations, transaction proc-
essing, office document interchange, manufacturing messaging, and many
other new functions. In general, a clear trend towards powerful applicatlon-
oriented communication services can be observed.
The fact that standardized protocols are becoming more and more impor-
tant puts additional burdens on implementors, who are now concerned with
conformance and interoperability in heterogeneous environments. Commu-
nication hardware and software has to be developed carefully in order to
achieve and maintain high quality of products. New networks employing
optical fibers allow transmission speeds orders of magnitudes higher than
with copper technology. These networks will trigger new distributed applica-
tions requiring new communication services and new protocols.
Possible automation and tool support are considered to be the main bene-
fits that can be derived by employing formal approaches. In a formal
approach, different development activities and their interrelations are
defined by an underlying methodology. The fundamentals and results of
development steps are documented as formal descriptions. In this way,
input can be processed and output produced by tools supporting the devel-
opment activities. These tools may work automatically, or under the guid-
ance of a user.
1.1 Overview 3
This thesis describes the provision of tool support for protocol engineering
based on a formal methodology. The initial step In this methodology is to
get from an informal description to a formal specification of requirements.
Further steps consist of refining and implementing the specification and
finally testing the implementation. In order to facilitate these steps, suitable
formal description techniques (FDTs) and tools have to be employed. The
feasibility and efficiency of the initial step is crucial to the applicability of
the whole scenario and depends on the techniques used. A rule-based
formal description technique (Communicating Rule Systems (CRS» is
adopted in this thesis and used to illustrate basic ideas. Rules are consid-
ered to be excellent means for capturing protocol knowledge in a human-
understandable way. It is shown that they are also appropriate for realizing
tool support.
In chapter 2, the reasons why the work conducted in the framework of this
thesis was not done with one of the standardized FDTs are explained. An
evaluation is presented that also includes popular non-standard FOTs'. The
suitability of the FDTs for specifying communication services and protocols
was investigated, as well as assessing properties of their underlying models.
In particular, the following techniques are considered: Estelle and SOL (state
machines), NPNs (Petri nets), LOTOS (process algebras), Z (predicate logic).
The ferm "formal description technique (FDT)" is used in a broader scope in this thesis
(detailed in chapter 2) and is not confined to standardized techniques.
4 1 Introduction
Specification examples covering parts of the X.2S packet level protocol are
presented to illustrate basic language features. Before discussing FDTs,
informal specification aids and their shortcomings are summarized. The FDT
evaluation is concluded with a comparative assessment of the techniques.
Although many of the ideas presented in other chapters of this thesis are of
general nature, their realization would have been more difficult or even
impossible with the techniques evaluated in chapter 2. In chapter 3, the
adoption of CRS for specifying communication services and protocols is
described. Modifications made to the original approach presented in
[Neum88] are explained. One major modification is the replacement of CRS
data type constructs by the Abstract Syntax Notation One (ASN. i), as
standardized in [1508824]. ASN.1 typing mechanisms offer considerable
advantages because they are tailored to describe data structures frequently
used in communication systems. Since the Incorporation of ASN.1 into pro-
gramming languages or specification techniques was not foreseen by the
standard, several extensions to ASN.1 were necessary, resulting in an
Extended Abstract Syntax Notation One (X-ASN.1). The application of
both CRS and X-ASN.1 is illustrated with the X.25 packet level protocol.
Formal CRS semantics is given by using Jabel/ed transition systems at the
end of chapter 3.
that allows for use and mutual exchange of specification knowledge. The
realization of such an environment based on the CRS and X-ASN.1 execution
mechanisms is detailed.
The main results of the work presented in this thesis are summarized in
chapter 6 and some conclusions are drawn. Possible future directions for
the application of FDTs in distributed system design and realization are out-
lined.
OPEN
SYSTEM
OPEN
SYSTEM
OPEN
SYSTEM
I,,
.......... " ...... ~,... ..~ ...... ,., . '" ,- , ....... .. ...................................... ......
, , ~ -
OPEN
SYSTEM
local area networks (LANs) to metropolitan and wide area networks (MANs,
WANs) (see for example [Tane88]).
OPEN SYSTEM
OPEN SYSTEM
k
-_ .. --
..... -
.. ---- .. '
.. -
--~-
• In Figure 2, and in following figures, dotted lines are used to indicate logical rather
than physical interconnection.
8 1 Introduction
OPEN SYSTEM
OPEN SYSTEIol
k
each open system and underlying lower layers. The collection of all appli-
cation entities in an open system constitutes the application layer sub-
system. Application layer subsystems existing in each open system together
form the application layer.
OPEN SYSTEM
OPENSYST£M
k
Figure 4. Layered communication system as defined by the OSI Basic Reference Model
SPa
CN - 1)- SAP
SPa
Entities situated in the same layer, but located in different open systems,
are called peer entities. Peer entities communicate by exchanging protocol
data units (POUs) of well-defined format, according to the (N)-protocol. POUs
are not directly transmitted (except for the physical layer), but passed to
the next lower layer as an SP parameter. Entities situated in adjacent layers,
but located in the same open system, interact in terms of Interface data
units (IOUs). In an IOU, upper layer POUs are included in a service data
unit (SDU), together with some Interface control Information (ICI). The
lower layer entity interprets the ICI and adds some protocol control infor-
mation (PCI) to the SOU to form the lower layer POU. At the receiving side,
the PCI header is stripped off and interpreted by the peer entity. The SOU
information is passed to the higher layer. The mapping between these dif-
ferent kinds of data units in communication systems is visualized in
Figure 6.
There are many problems that may have to be overcome in each layer.
Flow control mechanisms are usually required for entities within the same
layer and between entities in adjacent layers. Sequencing mechanisms
have to be present if the underlying layer does not guarantee to deliver
data in the same order as submitted. In case of corruption, duplication, or
loss of data, error detection must be assured. Multiple connections in one
layer may be mapped onto one connection in a lower layer
(multip/exing/demultiplexing), or several connections in a lower layer may
be used to support one connection in a higher layer
1.2 Communication Systems 11
(N+1Ho)""
(NHa)'tf"
4. dependencies of SP parameters.
• Service access points (SAPs) symbolize the location where SPs are
exchanged between a service provider and a service user. The seman-
tics of communication at SAPs is not fixed. In principle, synchronous or
asynchronous communication mode is possible. Properties of SAPs may
comprise reliability, capacity, order preserving, context-dependency etc.
(compare [Gotz89J).
• The active elements in a layer are called entities. Entities are respon-
sible for realizing layer functions. They communicate with peer entities in
other systems by using a communication protocol. To achieve this com-
munication, each entity is connected to one or more SAPs of the lower
layer and uses the lower layer service. Enhanced services are provided
at SAPs of the next higher layer. The number of entities in a layer is not
fixed; entities may also execute in parallel. Protocol entities may be
realized as single processes, procedures, or as part of those.
As may have become apparent from this discussion, the definition and
understanding of architectural concepts for communication systems is a dif-
ficult subject due to the high degree of abstraction required in the frame-
work of open systems. The application and use of FDTs has stimulated and
influenced international agreement on semantics of architectural concepts.
The representation and meaning of architectural concepts in different FDTs
is an important issue.
1.3.1 Life-cycle
The general formal development life-cycle is presented In Figure 7 (see
also [BochS7a) [BrinSSa) [DrobS9) [Turn90) [Sidh90a). The initial task In this
life-cycle is the definition of system requirements. Clear understanding of
desired functionality has to be reached. Then an architecture may be
designed that satisfies the requirements. This is either done in a completely
informal way using natural language and pictures, or semi-formally by
applying graphic- and table-based techniques.
FORMALIZATION
o
~
ERlrICATION'
~ 0
STEPWISE
REFINEMENT
VALIDATION
l~~NTAT~
Figure 7. Formal development process
Finally, all or part of the development process has to be reassessed for the
purpose of maintenance, modification, performance improvement, or addi-
tion of system reqUirements.
At present, various means have been proposed for specifying services and
protocols for the different layers in a communication system. The specifica-
tions form the basis for design validation and serve as references for
implementors. For validating the correctness of implementations, tests can
be derived from specifications. According to [Lisk86], a specification can be
considered an abstraction from a set of implementations. The primary
purpose of the abstraction is to focus on the functional requirements of a
system that can be met in various ways by possible implementations
[Yiss86b]. To achieve this purpose, specifications need to be general
enough so that they do not exclude admissible implementations unneces-
sarily, but also have to be restrictive enough to rule out unacceptable ones.
Desirable properties of specifications include preciseness, consistency, com-
pleteness, and structured ness (compare [Brin88a]).
X.2S protocols
Packet-switched
Network
network' (see Figure 8). Together with the local and the remote DCE, the
network can be regarded as the underlying service provider passing pro-
tocol messages between DTEs. These messages are called packets in the
X.25 PLP. Two forms of connections are supported by the protocol. namely
switched virtual calls (SVCs) and permanent virtual circuits (PVCs). SVCs
are set up before data transfer and are cleared afterwards. PVCs are similar
to a leased line and require neither setup nor clearing. A so-called logIcal
channel is associated with each SVC and PVC by the protocol. The use of
the X.25 PLP to provide the OSI connection-oriented network service
(OSI-CONS) [IS08348] has been standardized in [IS08878].
The relationship between the OSI-CONS and the X.25 PLP is illustrated in
Figure 9 [IS08878]. Network service users (transport entities) interact with
network entities in the underlying layer (network service provider) in terms
\ ,
if \ .
if
I TL Entity I /f \\ I TL Entity
I
/f
I •
NS USER
~ .. \ \.\ I ..~
:' I
"~- ..! -----
~-.\ -- ----
--------- - - - I-- -
~- -,.,
NETWORK SERVICE ' - - 1--
NS PROVIDER
l "NL Entity I
"Nl Entity I
I:
ii
.... \ J
! ,.•
J
\ \. I
-\\ //
X2if¥R'CKET LEVEL PIUI'OCIl.. !lATA UNl'I'S
As an example consider the situation where the network service user issued
an N-GONNECT-request primitive and an INCOMING CALL packet arrives.
Depending on the actual sequence of events the network entity may have
passed the CAlL REQUEST packet to the DCE and a "call collision" occurs. In
[1508878]. paragraph 6.2.1. it is stated: "When an NL entity receives an
INCOMING CALL ... packet. it signals an N-CONNECT-indication ... primitive ...
to the NS user.". However. in the "call collision" case this violates the
network service. The text accompanying Figure 9 in [IS08878] is incom-
plete with respect to this situation.
Figure 10 summarizes the network SPs. In standards. such tables are also
used to list SP parameters and to indicate whether parameters are manda-
tory or optional (see [IS08348]). The types of SP parameters are described
informally by enumerating possible values or characterizing possible
ranges. The X.25 PLP packet types are given in Figure 11. In [1508208]. the
2.1 Informal Specification 25
connection N-CONNECT-request
establishment N-CONNECT-indication
N-CONNECT-response
N-CONNECT-confirm
data transfer N-DATA-request
N-DATA-indication
N-DATA-ACKNOWLEDGE-request
N-DATA-ACKNOWLEDGE-indication
N-EXPEDITED-DATA-request
N-EXPEDITED-DATA-indication
N-RESET-request
N-RESET-indication
N-RESET-response
N-RESET-confirm
connection N-DISCONNECT-request
release N-DISCONNECT-indication
Figure 10. Network service primitives
Figure 12 shows the format of the CALL REQUEST packet (left-hand side of
the figure). The parts drawn in bold lines represent the packet header con-
tained in all X.2S packets in the first three bytes. The first four bits constitute
the so-called "general format identifier". which is constant for all packets
except DATA packets. The number of the logical channel the packet
belongs to is contained in the second half of the first byte (group number).
and in the second byte of the packet header (channel number). The 12 bits
provided allow for 4096 logical channels. However. use of channel number
o is reserved. The third byte contains the packet type identifier. which is an
individual bit pattern for each packet. The "general format identifier" in DATA
packets contains important information for the DTEs executing the X.2S PLP
(see right-hand side of Figure 12). The "Q-biY' can be used to distinguish
between qualified and non-qualified data. the "D-biY' can be used for
requesting receipt confirmation of data packets. The numbering scheme
0 0 0 1 I group number
01 0 1 Madulo I group number
colling address
coiled address
facilities length
data
facilities
user data
...............................1
Figure 12. X.25 PlP CAll REQUEST and DATA packet formats
2.1 Informal Specification 27
During an execution of the X.25 PlP, DTEs are in different states. In each
state, several packets may be sent or received. In order to define the pos-
sible incoming and outgoing packets for all states of the protocol, state
diagrams are used. In Figure 13, the state diagram for the X.25 PlP call
setup phase is shown. From a service user's point of view, internal protocol
states are not of interest, but possible sequences of SPs are. An explicit
representation of sequence information is provided by time sequence dia-
grams. In Figure 14, the time sequence diagram for call setup in the X.25
PlP is shown. Vertical bars are used to illustrate the interfaces that data
units have to pass through and arrows indicate data flow. Time proceeds
from the top to the bottom of the diagram. The connection establishment is
initiated by a network service user with an N-CONNECT-request primitive. A
CALL REQUEST packet is sent by the network entity and delivered as an
INCOMING CAll packet to the receiving side. An N-CONNECT-indication
primitive is passed to the remote network service user, who responds with
an N-CONNECT-response primitive. A CAll ACCEPTED packet is sent and
delivered as a CAll CONNECTED packet. An N-CONNECT-confirm primitive is
28 2 Protocol Specification with Formal Description Techniques
passed to the network service user, signalling that the requested connection
has been established.
Figure 14 describes partially the mapping between network SPs and X.2S
packets according to [IS08878]. The CCITT X.2S PLP had been defined
NS NS OCE OCE
NS NS
User Pro'llider Pro'llider User
NSAP X.25 Interface NETWORK )(.25 I "tarof.c. NSAP
N-ClNf:cr request
V CALL RIIIIUIBT .....
V ----------- Il«XImG CALL ...
N-CINf:cr IlIdlcatllll
V
~
...1HDIfCT~
ClLL JCCIS"I'EIl ~
Figure 14. Time sequence diagram for call setup in the X.25 PLP
2.1 Informal Specification 29
before the ISO network service and, consequently, before the mapping
between the service and the protocol. This does not correspond to the
development cycle as presented in chapter 1, but has historical reasons.
The mapping of SP parameters to packet fields and vice versa is given in
several individual paragraphs and clauses of English text in [1508878]. The
meaning and intended use of packet fields has been described using
many sentences spread over different sections of the document [1508208].
In general, such natural language descriptions are easy to read, but as
already illustrated, readability does not necessarily induce intelligibility. In
fact, ambiguities cannot be avoided in natural language text and important
information may be missing. Besides these shortcomings, the fact that
informal specifications cannot be processed by tools supporting validation,
implementation, and testing of services and protocols is a major drawback.
Formal models and FDTs have been invented to overcome this problem.
1. a formal syntax, which is a set of rules prescribing all the symbols that
can be used and the expressions that can be constructed in the lan-
guage;
Another aspect which is particularly important for the ideas presented in this
thesis is
2.2 Formal Description Techniques (FDTs) 31
Besides these general criteria, the intended application area must be kept
in mind when evaluating the suitability of FDTs. For example, powerful con-
structs for the parallel composition of specification parts do not contribute to
the suitability of a technique for describing sequential systems, whereas for
specifying concurrent activities they are crucial. In general, the formal
semantics of an FDT should be unambiguously related to the architectural
concepts of the intended application area [Viss86b] [Turn87] [Gotz90b]. In
[Turn87], the link between FDT concepts and architectural concepts of the
application area is referred to as the architectural semantics of an FDT.
The evaluation of several existing FDTs with respect to the general criteria
and with respect to the application area of communication systems is pre-
sented in the following sections. The selected FDTs use different underlying
models and have been applied frequently to the specification of communi-
cation services and protocols. To illustrate the basic characteristics of the
selected FDTs, the underlying models are explained first. Setting up a virtual
call in the X.2S PLP is used as a common example and partially described
in all techniques.
" In [Brin88a], an FDT is called constructive if there exists an interpretation algorithm for
the symbolic execution of specifications.
32 2 Protocol Specification with Formal Description Techniques
In this definition, outputs are associated with transitions and depend on the
input and the current state (Mealy machine). Alternatively, the output func-
tion A. may also be defined as A: Q -+ 0, associating outputs with states
(outputs depend on states only, Moore machine). Mealy and Moore
machines are deterministic: subsequent states are uniquely determined by
the current state (and the input). If the transition function 0 is defined as a
relation 0: Q x I -+ P(Q) (P(Q) denoting the powerset of Q), the state
machine is called nondeterministic. FSMs are graphically represented as
state diagrams (see for example Figure 13) or as state tables.
Estelle
An Estelle specification describes a hierarchically ordered set of EFSMs,
called module Instances (or tasks), running in parallel and communicating
via message passing. Minor state variables, predicates, and actions of
EFSMs are represented as "PASCAL" variables, functions, statements and pro-
cedures. The "PASCAL" programming language is almost completely incor-
porated in Estelle and is also used for type definition. Communication
between tasks is achieved via bidirectional channels connecting two Inter-
action points of different module instances. An unbounded FIFO queue Is
associated with each interaction point, buffering messages (called Inter-
actions) at the receiving side.
NSAP
Figure 16. Estelle module header and channel definitions for X.25 PLP
36 2 Protocol Specification with Formal Description Techniques
initialize
begin
init dte_l with X_25_DTE_body;
TYPE
N_CONNECT_request = RECORD
called_address : ARRAY [1 .. MAX ADO] OF CHAR;
calling_address : ARRAY [1 •• MAX=ADD] OF CHAR;
receipt confirmation selection: BOOLEAN;
expedited data selection : BOOLEAN;
quality_ot_service Network_quality_of_service;
user_data : ARRAY [1. .MAX_UDAT] OF OCTET
END;
= RECORD
header : Packet header;
calling dte address length - : INTEGER;
called dte address length : INTEGER;
called-dte-address- BCD STRING;
calling dte address BCD-STRING;
facility length INTEGER;
faci 1ity-field Facil ities;
user_data ARRAY [1. .16] OF OCTET
END;
Packet_header = RECORD
q_bit BOOLEAN;
d bit BOOLEAN;
modulo ( modulo 8, modulo 128 );
lc number INTEGER;-
packet_type_id OCTET
END;
Logical_channel_number = (8 .. 4895);
Figure 18. Estelle (HPASCALH) type definitions for network SPs and X.25 PLP packets
2.2 Formal Description Techniques (FDTs) 37
Figure 19 illustrates how a module body for module header X_25 _OlE is
specified in Estelle. Main states are enumerated following the state-keyword.
Minor state variables, types, and procedures may be declared. The initial
transition executed after creation takes module instances into state pI. The
dynamic behavior of module instances is defined in the transition part of a
initialize to pI;
begin
LC_status := free;
end;
trans
froll pI
to p2
when NSAP.N CONNECT req
provided LC_status = free
begin
CR PDU.header.q bit := FALSE;
CR-PDU.header.d-bit := N CR SP.receipt confirmation selection;
CR)DU.header.lc_number := LC; - - -
SDL
SDL is similar to Estelle in many respects, but uses a graphical syntax
(SDL/GR). It is only recently that a textual syntax (SDL/PR) has been devel-
oped to ease the distribution and machine processing of SDl specifications.
An SDL system is composed of a number of blocks that are connected via
channels. Blocks can be further substructured into several smaller blocks,
leading to a hierarchical system structure. At the lowest level, a block is
defined by one or several processes, which are the parallel units. Whereas
blocks define the static system structure, processes are created dynam-
ically and are deleted after their termination. The channels connecting
blocks can be refined within block substructures; the messages being con-
veyed are called signals in SOL. On the process level, signalroufes are
attached to channels. The semantics of channels and signal routes are dif-
ferent. Whereas channels cause an unspecified but perceptible delay for
signals, signalroutes pass signals without any delay from source to destina-
40 2 Protocol Specification with Formal Description Techniques
tion. Each process has a FIFO queue attached to it that buffers the incoming
signals.
A small SOL system representing an X.2S DTE by one block and one process
is depicted in Figure 20. The SOL symbol for a block is a rectangle, proc-
esses are drawn as 8-cornered boxes. The block X_25_manager is con-
nected to the environment via the channels NSAP and Packets, representing
the communication links to the network service user and the X.2S network.
The signal lists in brackets specify what kind of signals can be sent and
received via these channels. All signals have to be declared using the text
symbols included in the diagram. The process X_25 _DIE is parameterized
by a logical channel number (l c) and has two signalroutes (SP, Pack)
attached to the corresponding channels (NSAP, Packets).
SYSTEM X_25_PLP
~Il- [SP2] SIGNAL ~
NSAP N....CONNECLreq
, [SP1]
...
N....CONNECT_ind
SIGNAL
CalLrequeat
Incomln9-call
...
SIGNALLIST
Pack1 - ColLrequeat ....
Pack2 - Incomin9-coll, ...
...
PROCESS X_25_DTE
FPAR lC Integer; DCl
LC_Btatua LC.JItatuB_tYPB - fro.;
N_CfU;P f<LCONNECT_requeat;
CILPOU CALLREQUEST;
I
CalLrequeat ( CILPOU )
( p2 )
I
NEWTYPE N_CONNECT_request
STRUCT
called address Charstring;
call ing address Charstring;
receipt=confirmation_selection Boolean;
expedited_data_selection Boolean;
quality of service Network_quality_of_service;
user_data - Octetstring;
ENDNEWTYPE
NEWTYPE CALL_REQUEST
STRUCT
header Packet header;
calling dte address length Integer;
called dte address length Integer;
called-dte-address- BCDString;
calling dte address BCDString;
facil ity length Integer;
facil ity-field Faci 1ities;
user data OctetString;
ENDNEwrYPE
NEWTYPE Packet_header
STRUCT
q bit : Boolean;
d-bit : Boolean;
modulo : Modulotype;
lc number Integer;
packet type id : Octet;
ENDNEWTYPE -
NEWTYPE Modulotype
LITERALS modulo_B, modulo_12B;
ENDNEWTYPE
Figure 22. SOl type definitions for network SPs and X.25 PLP packets
Most of the criticism for Estelle also applies to SDL: a low level of
abstraction, only asynchronous communication, limited structuring facilities
for state transitions etc. In contrast to Estelle, SDL allows ADTs to be defined
and makes no explicit use of a particular programming language. Other
SDL characteristics are considered drawbacks compared to Estelle: only one
common input queue for each process, no spontaneous transitions,
deterministic selection of inputs. These characteristics complicate
implementation-independent specification and appropriate extensions have
been proposed for SOL in [Hogr89b].
P is a set of places,
PLACE 1
~ron.ltlon condition]
lren.ltlon operation.
created token.
PLACE 2
NPNs
Numerical Petri Nets (NPNs) [Whee85] are a form of HLPNs being applied
for specifying services and protocols [BiII88] [Diaz86] [BiII86]. The graphical
representation illustrated in Figure 23 corresponds to the graphical syntax
of NPNs [BiII88].
In NPNs, tokens are tuples of variables. The arcs can be inscribed with func-
tions and expressions, leading to complex enabling and firing rules. In
addition, a set of global data variables can be associated with a net spec-
ification. Only a number of simple data types are provided (Integer,
Boolean, Enumerated, String). Two different capacity functions are given,
restricting the number of tokens for a specific color and the total number of
tokens at places, respectively.
To further illustrate the various net mechanisms that can be used for speci-
fying distributed systems, two small nets are shown in Figure 24, modelling
different communication modes between system parts. In net (a), a shared
place is used to connect the entities PI and P2 represented by two places
and one transition each. In order to communicate, one entity puts a token
on the shared place and the other may remove it from there (asynchronous
communication mode). In net (b), PI and P2 are coupled by a shared tran-
sition and tokens removed from one input place may be moved to either
2.2 Formal Description Techniques (FOTs) 47
P1 P2 P1 P2
(0) (b)
NConReq
l.CJtatuI· pendln;
• NSAP Packets
VARIABLE TYPE
cd,cg String
rC,ed Boolean
QO& Integer
- { <"N_CONNECT_req">} Ud String
q,d Boolean
- {<"InCOI1InQ...c"II">' mod El1I.I1IIIr.. tad
<"C1ear.lndlc..tlon">} Ie Integer
ptl String
mo(NSAP) - { }
cgl,cdl Integer
cd,cg String
mo (Packets) - { } fl Integer
f String
Ud String
First, basic concepts like entities or SAPs require several places and/or tran-
sitions to be represented, due to the very general mechanisms that nets
offer. Second, the variety of adequate possibilities for describing a system
can cause confusion. Each new net has to be understood from the begin-
ning by Its lOW-level primitives because abstraction mechanisms are
missing.
HlPNs (and NPNs) are formally well-defined and powerful methods exist for
analyzing nets. Compared to normal place/transition nets, the expressive-
ness of NPNs is better, but certain reqUirements can sometimes only be
described by larger nets with several transitions and places. Data typing
facilities are severely limited. On the other hand, nets are implementation-
independent specifications expressing concurrency and causality well.
Compositionality can be achieved in various ways: by identifying places
and/or transitions of individually developed nets or by introducing subnets
2.2 Formal Description Techniques (FDTs) 49
2.2.3 LOTOS
The formal description technique LOTOS (Language of Temporal Ordering
Specification) was developed within ISO between 1981 and 1988 [1508807]
(in parallel with Estelle). A process algebraic approach was taken and the
algebraic data type language ACT ONE was adopted for abstract data type
definition. A comprehensive tutorial on LOTOS is provided in [BoI087].
Process Algebras
The process algebraic approach to the specification of communicating
systems was Initiated by Milner with CCS (Calculus of Communicating
Systems) presented In [Miln80]. The basic idea Is to describe a system only
by the behavior that can be seen (or experienced) by an external observer.
Systems are composed of several communicating agents Interacting with
each other and with the external environment. Communication takes place
as an indivisible unit of synchronized interaction (called actions). The
behavior of agents is described by behavior expressions that are subject
to algebraic laws. Several related approaches (for example [Hoar85]) use
the notion of processes instead of agents.
Agents are often graphically represented as boxes, with the set of possible
actions drawn at the sides (see Figure 26 for an example). The observable
actions determine the alphabet A of an agent. The unobservable (internal)
actions of an agent (for example, internal communication between two
components) are represented with an internal action symbol. The behavior
of an agent is specified by an associated behavior expression (see
Figure 26) that is constructed from predefined simple behavior by applying
a fixed set of compositional operators. These operators can be used to
combine agents sequentially or concurrently and to specify alternative or
recursive behavior. The number and characteristics of predefined simple
behaviors and available operators distinguish different process algebras.
The syntax employed is also different in many cases.
50 2 Protocol Specification with Formal Description Techniques
a- I-C
A A
b-
A = {a, b, c, d}
actions =Au { i } A= ((a; b ; A) [] (j ; c ; d ; stop) )
LOTOS
In LOTOS, communicating agents forming a system are called processes. A
specification defines a hierarchy of processes, where process behavior is
expressed by combining subprocesses exhibiting simpler behavior until the
specification can be expressed directly (inaction, action prefix. choice,
successful termination). Composition operators are provided for sequential
composition (enabling, disabling) or parallel composition of processes
(pure interleaving, full synchronization, general case). Processes being
composed in parallel communicate by participating in a synchronous
event. The notion of a gate is used as a synonym for event labels and sym-
bolizes the abstract location where the interaction takes place. Interactions
performed at internal gates can be hidden from the outside world by using
the hiding-operator. The symbol I is used to denote an internal event.
Existing process definitions can be instantiated in other process definitions.
In this way, recursive behavior can be achieved.
B1 B2
Name Syntax
inaction stop
action prefix
- unobservable (internal) liB
- observable 9iB
choice BiD B2
parallel compasition
- general case B1 1[911 .... 9nJI B2
- pure interleaving B1II1 B2
- full synchronization Bill B2
hiding hide 91' ... , 9n in B
process instantiation p [911 ..., 9n]
successful termination exit
sequential composition (enabling) B1 »B2
disabling B1 [> B2
Figure 27. Syntax ot behavior expressions In Basic LOTOS
2.2 Formal Description Techniques (FDTs) 53
way that several processes acting in parallel impose their individual con-
straints on data values during synchronization with other processes. This is
called the constraint-oriented specification style. other specification styles
exist and should be used for more implementation-oriented specifications.
NSAP
eqns
forall cd, cg : CharString, re, ed : Bool, ud : OctetString
ofsort Bool
receipt_confirmation_selection NConReq ( cd, cg, re, ed, ud ) } = rc
endtype
eqns
forall bI, b2 : Bool, mod: Mod, no : Nat, id : Octet
ofsort Bool
q_bit ( make_header ( bI, b2, mod, no, id ) ) = bi ;
endtype
endtype
Figure 30. LOTOS (ACT ONE) type definitions for network SPs and X.25 PLP packets
56 2 Protocol Specification with Formal Description Techniques
Since LOTOS was conceived for specifying OSI services and protocols, the
architectural concepts of communication systems are represented well.
Processes model protocol entities and can be composed flexibly to form a
protocol layer and to provide a service. SPs and PDUs are exchanged with
interactions at gates representing SAPs. The functionality of a service or the
rules of a protocol are defined by temporal orderings of interactions and
multi-way synchronization constraints. A new process can be instantiated for
each new connection and processes can be parameterized by CEPs.
The application of ACT ONE for specifying data types requires a substantial
effort. Only limited support is provided by a predefined type library and all
other types have to be defined from scratch. The denotation of values as
2.2 Formal Description Techniques (FDTs) 57
2.2.4 Z
The Z notation is a general-purpose formal description technique developed
at Oxford University since 1980. It is based on set theory and predicate
logic and has been employed for specifying a variety of information proc-
essing systems [Haye87]. More recently, Z has also been used In the area
of communication systems [Duke88]. An introduction and reference manual
is provided in [Spiv89].
Predicate Logic
A language of formal logic is defined in two steps (see for example
[Mann74]). First, syntactic rules are given that determine the set of well-
formed formulas. In first order predicate logic (FOPL), symbols exist for
constants, individual variables, functions, predicates, quantors, and logical
connectives ('" v, ..." =>, <0>, V, 3). Terms are defined as constants, vari-
ables, or function symbols applied to terms. An atomic formula is either a
predicate symbol applied to terms, or an equality between two terms. A
formula can be an atomic formula, or may consist of formulas combined
by logical connectives.
Z
A Z specification comprises definitions of mathematical objects like types,
functions, relations, sets etc., and a number of schemas. Data typing mech-
anisms are based on sets. Several basic sets are predefined and new types
can be constructed by using set operations, functions or relations over sets,
cartesian products etc. Schemas provide a framework for declaring a
number of objects that are associated with variables and a number of pred-
icates that describe properties of the schema by relating the variables.
NSAP
Isps-:--s-eq--S-p---------------------------------------
Packets
I pack :-s-e-q-P-O-U--------------------------------------
OTE_state
LC
------------------------------------------
8 •• 4895
LC_status {free, pending, busy}
p state {pI, p2, p3, p4, p5, p6, p7}
LC = lc
LC_status = free
p state = pI
NConReq
~----------------------------------
6 X_25_DTE
CR PDU CALL_REQUEST
N_CR_SP : N_CONNECT_request
N_CR_SP = head ( sps' )
p state' = pI
LC_status' = free
sps = tail ( sps' )
CR POU.header.q bit = false
CR-POU.header.d-bit = N CR SP.receipt confirmation selection
c
C(POU. header. 1 _number = LC - - -
p state = p2
LC_status = pending
pack
N_CONNECT_request
called_address
--------------------------------
: ADDRESS
ca 11 i ng address : ADDRESS
receipt-confirmation selection : BOOLEAN
expedited data selection : BOOLEAN
quality_ot_service NetworkQualityOfService
user_data : OCTETSTRING
Packet_header
q bit
--------------------------------
BOOLEAN
d-bit BOOLEAN
modulo {modulo 8, modulo 128}
lc number 9 •• 4995- -
packet_type_id : OCTET
CALL_REQUEST
header
---------------------------------
: Packet header
calling dte address length: Z -
called dte address length : Z
cal 1ed-dte-address- : BCDString
calling dte address : BCDString
facility length : Z
facility-field : Facilities
user_data : OCTETSTRING
Figure 33. Z type definitions for network SPs and X.25 PlP packets
The degree of abstraction reached with Estelle and SDL Is too low, resulting
in overspecification. No programming language should be employed for
specifying abstract services and data types. Nondeterminism as a means of
expressing alternative behavior is important and should be available. Syn-
chronous communication is appropriate for specifying abstract service
aspects and should be provided as well. FDTs employing state transition
models should offer language constructs that allow thorough structuring of
the transition space. True parallelism within a state machine cannot be
expressed.
The degree of abstraction and the sound mathematical basis of the Z nota-
tion are appealing, but similar arguments apply as for Petri nets. The repre-
sentation and parallel composition of protocol entities is difficult to describe.
Modelling communication via SPs at SAPs according to the basic concepts
of open systems is not straightforward. This is because the basic architec-
2.3 Comparative Assessment 63
From the languages evaluated in the last section, LOTOS meets best the
requirements for an FOT to be applied for specifying communication
systems. The technique focuses on external observability and provides pow-
erful concepts supporting communication system design. The abstraction
from internal states of specified systems is advantageous when abstracting
from particular implementations, but also poses considerable problems.
Parameter dependencies, local and global constraints, and protocol rules
are difficult to formalize without the concept of an internal state if they are
of realistic complexity. Multi-way synchronization is considered inadequate
for describing communication between distributed processes. Although pro-
viding an excellent semantical basis, the algebraic style of writing abstract
data type speCifications has to be improved for LOTOS in order to be appli-
cable in practice.
The results of the evaluation of existing FDTs has been the motivation to
search for an alternative approach that tries to combine the advantages of
the existing techniques while avoiding their main drawbacks. The new
approach is presented in the next chapter.
64 2 Protocol Specification with Formal Description Techniques
3 Protocol Specification with
Communicating Rule Systems
The resulting CRS language as used in this thesis is presented in the fol-
lowing. The data definition constructs provided by X-ASN.1 are explained in
section 3.1. How rules and rule systems can be specified is described in
section 3.2, including an assessment according to the criteria developed in
chapter 2. The operational semantics is given in section 3.3. A number of
examples taken from the X.2S packet level protocol (PLP) [1508208]
[1508878] are provided as illustrations of the various concepts introduced in
this chapter.
ABSTRACT SYNTAX
~~OCOI"\j / "',
(e
LOCAL SYNTAX LOCAL SYNTAX
locol ~
\pre!entotio j epre~entotiO!
System A \ ,/ System B
" //
Encoding/Decoding Encoding/Decoding
A t--f T T t--f B
TRANSFER SYNTAX
TYPE DLSeg- typedef struct {
RECORD char .Id dota;
loodDt : ARRAY [1..512 J OF CHAR; T
) lnt more:
more : BOOLE AN; dlseg;
END
BEGIN
EXPORTS .,.
IMPORTS .••
END
Figure 35. ASN.1 module definition frame example
tocols. Several modules can be created for different protocol layers, service
Interfaces, functional units, or other aspects of grouping.
When talking about data types where the representation of values and the
implementation of associated operations is fixed, the notion concrete data
types is often used. Data types that are defined without using a specific
representation and implementation are called abstract data types (ADTs)
(see for example [Clea86]). The basic idea of ADTs is to separate the use of
a type from its implementation. By defining possible operations on ASN.1
types, predefined ADTs are provided to users of X-ASN.1. For the type
constructors this results in a generiC type concept. Completely new ADTs
may be defined (if required) using data abstraction in CRS (see section 3.2).
Nothing has been said so far about another ASN.1 facility: the macro nota·
tion. By using macros, a user of the technique is able to extend the prede-
fined ASN.1 syntax and to introduce completely new type definition
constructs. Thus, the ASN.1 macro notation means much more than the
textual substitution available in assembler languages. Since the syntax of
ASN.1 is not fixed if macros are used, analysis tools for the language are
70 3 Protocol Specification with Communicating Rule Systems
The simple types, structured types, and subtypes that can be defined using
X-ASN.1 and the possible operations available are explained in the fol-
lowing. Some type definitions for data structures used in the X.25 PLP are
given as examples.
SImple types
The following simple types are provided by X-ASN.1:
• BOOLEAN
values TRUE, FALSE
• INTEGER
values all integer numbers
• REAL
values all floating point numbers
• BIT STRING
comments The length of the string can be restricted by using the SIZE
construct in the type definition. The concatenation opera-
tion takes two string arguments and delivers the concat-
enated string as the result. The substring operation takes
one string argument. the starting position. and the length
of the substring to be delivered as the result. The length
function takes one string argument and delivers the
number of bits in the string. In addition. particular bits can
be associated with identifiers (named bits).
• OCTET STRING
comments The length of the string can be restricted by using the SIZE
construct in the type definition. The concatenation opera-
tion takes two string arguments and delivers the concat-
enated string as the result. The substring operation takes
72 3 Protocol Specification with Communicating Rule Systems
::= BOOLEAN
d1 0 bit type ::= TRUE
d2 O=bit=type ::= FALSE
~ d1 = FALSE
d1 v d2 = TRUE
d1 A d2 = FALSE
(2) Sequence_numbers ::= INTEGER
Window_sizes ::= INTEGER {small_default(2), large_default(8)}
LENGTH(pti) =8
! pti ='11118188'B
pti II ! pti =' 11111111' B
(5) User_data ::= OCTET STRING (SIZE(8 •• 128))
LENGTH(ud1) =5
LENGTH(ud2) = 2
SUBSTR(ud1, I, 2) = '6865'H
CONCAT(ud1, ud2) = '68656C6C6F2821'H
(6) P_state_type ::= (p1(l), p2(2), p3(3), p4(4), p5(5), p6(6), p7(7)}
• ENUMERATED
operations
• NULL
values null
operations
examples
These simple types are similar to most simple types in specification and
programming languages. The indices of operation names are omitted in
specifications (overloading) because the operations can always be identi-
fied by the context in which they are used. A number of character string
types (PrintableString. IA5String etc.) are derived from the general OCTET
STRING type and predefined in [IS08824]. The same operations as defined
for OCTET STRING are also defined for these character string types.
74 3 Protocol Specification with Communicating Rule Systems
structured types
Structured types can be defined in X-ASN.1 by using type constructors that
facilitate the construction of data structures frequently required in communi-
cation systems. Complex types can be formed by combining existing types
in various ways.
- SEQUENCE
N_CONNECT_request := SET {
ca 11 ed address OCTET STRING,
calling address OCTET STRING,
receipt-confirmation selection BOOLEAN,
expedited data selection BOOLEAN,
quality of service Network Quality of Service,
user_data - OCTET STRING - -
N_DATA_request := SET {
user data OCTET STRING,
recelpt_confirmation_selection BOOLEAN
• SEQUENCE OF
values Given a single type, the constructed type contains all
values being sequences of values from this type.
• SET OF
values Given a single type, the constructed type contains all
values being multlsets of values from this type.
LENGTH(dps) = 2
dps[1] = { header { ..• },
p r 9,
more bit TRUE,
p s - 1,
packet_type_identifier '9'B,
user data '68656C'H
• CHOICE
LENGTH(dsps) = 1
{ user_data '68656C6C6F'H, receipt_confirmation_selection TRUE} E dsps = TRUE
The X-ASN.1 type constructors allow the flexible definition of the abstract
structure of data objects being exchanged between entities in a communi-
cation system. The constructs provided cater for the fact that some parame-
ters of SPs and fields of PDUs are often optional, vary in size, may come in
a different order, or may take several alternative forms. The operations
defined in combination with the type constructors are generic and prede-
fined for all types built with these constructors. The indices of operation
names are omitted in specifications (overloading). The notion of
parameterized types (or polymorphic types) is also often used for such a
typing mechanism [Card85].
Subtypes
Subtypes comprise a subset of the value set of a parent type (called base
type in the following). Different constructs exist for the specification of those
sUbsets:
• multiple values
X25_PDU :z CHOICE {
ca 11 request CALL REQUEST
incoiiiing call INCOMING CALL
call_accepted CALL_ACCEPTED
call connected CALL_CONNECTED
clear request CLEAR REQUEST
clear-indication CLEAR-INDICATION
clear-confirmation CLEAR-CONFIRMATION
data - DATA -
interrupt INTERRUPT
interrupt confirmation INTERRUPT CONFIRMATION
receive ready RECEIVE_READY
receive=not_ready RECEIVE_NOT_READY
reset request RESET REQUEST
reset-indication RESET-INDICATION
reset=confirmation RESET-CONFIRMATION
restart request RESTART REQUEST
restart-indication RESTART-INDICATION
restart-confirmation RESTART-CONFIRMATION
di agnosti c DIAGNOSTIC
reject REJECT
registration_request REGISTRATION_REQUEST
registration_confirmation REGISTRATION_CONFIRMATION
NETWORK_SPS := CHOICE {
n_connect_request N_CONNECT_request
n_connect_indication N_CONNECT_indication
n connect response N_CONNECT_response
n-connect- confi rm N CONNECT confi rm
n-data request N-DATA request
n-data-indication N=DATA=indication
n=data=acknowledge_request N_DATA_ACKNOWlEDGE_request
n data acknowledge indication N DATA ACKNOWLEDGE indication •
n=expedited_data_request N=EXPEOITED_DATA_request
n expedited data indication N EXPEDITED DATA indication
n-reset request - N-RESET request -
n-reset-i ndicat ion N-RESET-i ndicati on
n-reset-response N- RESET-response
n-reset-confirm N-RESET-confirm
n-disconnect request N-DISCONNECT request
n=disconnect=indication N=DISCONNECT=indication
• INCLUDES
values including all values from the base type
• value range
values all values from the base type in the specified range
• SIZE
values all values from the base type satisfying the size require-
ments
• FROM
values enumerated following the base type (which must be a
string)
• WITH COMPONENTS
values as given for the base type with or without optional com-
ponents
• types are also equivalent if they represent just renamings of the same
type;
With this definition of type equivalence, two given values of equivalent types
may be tested for equality. The operation = (equality) is defined for all
X-ASN.1 defined types and returns a boolean result.
UNIVERSAL Universal tags are the implicit tags defined by the ASN.1
standard for each simple type and for each type
constructor (for example BOOLEAN has the tag "UNIVERSAL
1" and types constructed with SEQUENCE have the tag
"UNIVERSAL 16"). Universal means that tags of this kind
are unique in all contexts.
context specific Tags belonging to this class are specific to the context
they appear in, for example, in a type definition or a
module. These tags are denoted by the tag number only,
the tag class being omiHed.
In the explicit form, tags are wriHen in square brackets and aHached to
types in the type definition. If IMPLICIT is used in the type definition only the.
explicit tag is encoded.
For the mapping between an abstract syntax specified with ASN.1 and a
concrete transfer syntax, encoding rules are used. Different sets of encoding
rules are possible, leading to different concrete representations of an
abstract syntax. Currently, ISO has standardized one set of encoding rules,
the so-called basic encoding rules (BER) for ASN.1 [IS08825]. In order to
illustrate the way encoding rules work, the BER are explained briefly.
84 3 Protocol Specification with Communicating Rule Systems
In BER, the structure of encoded values can take two forms: definite length
or indefinite length. Both forms are depicted in Figure 43. Each form can
be separated into three parts: (1) type identification, (2) length information,
(3) content. In definite length encoding, the actual length of the contents
field is calculated and precedes the contents field. If the length is smaller
than 127, one byte is used to encode the length, otherwise several bytes
are used (the first byte indicates that the length is encoded in the following
bytes). If definite length encoding is not appropriate (for example, for
strings or structured values), the indefinite length form is chosen. In indefinite
length encoding, the length field preceding the contents field indicates that
the contents field Is terminated by a special "end-of-contents" pattern. The
actual length of the contents field is not calculated in advance.
The type identification part for both encoding forms is structured as shown
in Figure 44. The first two bits of the identifier octet are used to encode the
tag class ("00" for UNIVERSAL, "01" for APPLICATION, "11" for PRIVATE and
"10" for context-specific). The next bit indicates whether primitive encoding
or constructed encoding is used. In primitive encoding, the contents field
represents an encoded value of a simple type according to encoding rules
for all simple types. In constructed encoding, the contents field represents a
CONTENTS DEFINITE
OCTETS LENGTH
number of octets
in the contents
octets
CONTENTS INDEFINITE
OCTETS LENGTH
Identifier Octet
Bits 8 7 6 5 4 3 2
NUMBER OF TAG
0= primitive
1 - constructed
The rule systems Network _ent ity 1 and Network_ent ity2 represent two
instances of an X.2S OTE. Thus, the behavior of each of the rule systems
Network_entityl and Network_entity2 corresponds to the specification
example used throughout chapter 2. A CRS specification of the configura-
3.2 Communicating Rule Systems (CRS) 87
G-(}G
Rul.. . .
G-(}G-
I
4. CD".
NSAP!
CD". II.
NSAP2 4,.
"":"01.,
... G- Rule.
I
G- <7
I
(rG-G
_Syriom
Network
RULE_SYSTEM Network_service;
STATE
at the rule system level. The behavior of the whole system is determined by
the behavior of the components.
Each rule system instance Is based on an EFSM. Major and minor state
objects are declared following the keyword STATE and may be of different
types. The possible transitions of the EFSM are specified using rules that are
defined in the RULES-part of a rule system specification. In order to express
the start condition and the effects of a rule, auxiliary objects and predicates
may be used that are listed following the keywords DECLARATIONS and
DEFINITIONS. Useful constant values can be defined following the keyword
CONSTANTS. A number of operators are provided by CRS that allow the spec-
ification of relations between rules acting independently on the rule system
state. These relations are defined in the SYN-part of a rule system specifica-
tion.
CONSTANTS
{<constant name> = <constant_value> ;)
STATE
{<state_variable_name> <state_variable_type> ;}
DECLARATIONS
{<declaration_variable_name> <declaration_variable_type>;)
DEFINITIONS
{<auxiliary_predicate_name> «formal_parameters» ~ <formula> ;)
RULES
SYN
{<rule_name> <synchronization_operator> <rule_name> ;)
STATE
r state R_state_type INITIAllY rI;
p state P_state_type INITIALLY pI;
(state O_state_type INITIALLY dI;
send_queue OataQueue;
receive_queue OataQueue;
DECLARATIONS
N CR SP N_CONNECT_request;
c"Rjiiu CALL_REQUEST;
RULES
END_RULE_SYSTEM X_25_0TE;
channel (LC). The state objects r _state, p_state, d_state determine the
major states of the rule system corresponding to the " restart", "call setup
and clearing", and "data transfer" states used in [IS08208]. Minor state
objects are declared for holding flow control information, user data to be
sent and received etc. Auxiliary objects are required for event parameters,
intermediate results etc. Some examples are given in Figure 48.
The object types and the rule paradigm employed in CRS are further
detailed in the following two sections.
Objects
In CRS, objects may be used as state objects or as local objects of rUles'.
The scope of state objects extends over the whole rule system, whereas the
scope of local objects is restricted to the start condition and effects formula
of a particular rule. Each object in CRS is of an object type. Depending on
the nature of the object, object types describe the abstract structure, the
possible operations, or the observable behavior of the object. According to
their object types, objects used in CRS specifications can be classified into
• gate instances or
Rule systems using only passive state objects are at the lowest level of a
rule system hierarchy defined by a CRS specification and are called basic
rule systems. Rule systems that are composed of active objects are called
communicating rule systems. This technical distinction is important for
defining the semantics of CRS in section 3.3.
, The term 'object' is used in a broader scope here, and not restricted to the object-
oriented interpretation.
3.2 Communicating Rule Systems (CRS) 91
<rule name>;
COND: <start condition formula> ;
EFFECTS: <effects formula;
The rule systems Network_ent ityl and Network_ent ity2 are examples of
basic rule systems. The state objects are of X-ASN.1 types (see section 3.1),
except for send_queue and receive_queue, which are instances of the ADT
DataQueue (see the rule system specification for X_25_DTE). How ADTs are
specified in CRS is explained in section 3.2.4. The rule system
Network_service specified in Figure 46 is an example of a communicating
rule system.
Rules
The syntax of CRS rules is shown in Figure 49. Each rule is identified by a
name and described by two formulas specifying the start condition and the
effects of a rule. The start condition is a predicate on the rule system state,
event occurrences, and requested event parameters. The effects predicate
defines a relation between the rule system state before the effects are
established ("old state") and the state afterwards ("new state"). A prime (')
is used in the effects formula when referring to an object of the old state.
Additionally, the effects formula describes event occurrences, event offers,
and offered event parameters. A rule may be started if the start condition
holds. A rule that has been started but not yet ended is called "running".
When a rule ends, actions establishing the specified effects are performed
atomically. Starting and ending a rule are two separate actions, occurring
at different points in time. After its termination, a rule may be started again
if the start condition is satisfied. As an example, a small part of a rule
describing the initiation of a connection establishment by a network service
user (resulting in the initiation of the X.25 PLP call setup procedure) is given
in Figure 50. In the start condition of the rule n_con_req, the
n_con_req;
COND: p_state = pI 1\ Nsap.N CONNECT req (N CR SP);
EFFECTS: p_state = p2 1\ Packets.Call request (CR-PDU)
A CR_PDU.user_data = N_CR_SP.user_data;
N_CONNECTJeq event is requested at the gate Nsap (see Figure 52 for the
syntax of event expressions) and requirements on the object p_state are
expressed. In the effects, the CallJequest event is offered at the gate
Packets and the values of event parameters are specified; a new value for
p_state is given. In this example, the local objects N_CR_SP and CR_PDU
have been used as event parameters. The scope of these objects is local to
the rule n_conJeq, but the value of N_CR_SP is remembered from the start
of the rule until execution of the actions establishing the effects. Thus, the
values of local objects are available for specifying the effects of a rule and
for describing offered parameter values, depending on received event
parameter values and state objects when the rule was started. Components
of objects of structured X-ASN.1 types are accessed using the X-ASN.1
selection operations as defined in section 3.1.
In order to describe how the X.25 PLP is used for establishing a connection
at the request of a network service user, the rule n_conJeq has to be speci-
fied in much more detail and several other rules are required for processing
the responses from the remote side (see [Mang90). Rules represent auton-
omous pieces of knowledge about a rule systems' behavior. In the area of
communication systems, rules are considered to be an excellent means for
capturing protocol knowledge and for supporting IntelligIbility of large pro-
tocol specifications. Each rule can be understood on its own and does not
immediately affect other rules, which reduces the complexity of the specifi-
cation task and simplifies extended or modified specifications. If several
rules can be applied in a certain state, the choice of which one to select is
nondeterministic, which realizes control abstractIon. By using predicate
logic, start conditions and effects of rules are specified in an
implementation-independent way.
Normally, most of the internal actions of basic rule systems are sequential
in nature. Therefore, rules in a basic rule system are mutually exclusive by
default. However, internal parallelism of rules inside one rule system is
sometimes useful. In CRS, three operators are provided for specifying
internal synchronization requirements. These operators can be used to
explicitly allow for parallel or privileged execution of rules. The
3.2 Communicating Rule Systems (CRS) 93
• parallel operator (II) is used for specifying that either rule can be
started even if the other one is already running ("semiparallelism in both
directions");
• prior operator (-<) is used for specifying that one rule has a higher pri-
ority if the start conditions of both rules are satisfied.
3.2.2 Gates
In CRS, gates are special objects shared by rule systems for the purpose of
communication. They may be considered as an abstract notion for the
SYN
fragment_data II send data;
send data " receive data;
receive_data " reassemble data;
send expedited data -< send data;-
receive_expedited_data -< receive_data;
Figure 51. CRS specification of X.25 PLP duplex and expedited data transfer
94 3 Protocol Specification with Communicating Rule Systems
location where communication events occur'. More than two rule systems
may share one gate, but events always occur between two rule systems. In
order to refer to an event in a specification an event expression is used
(see Figure 52). An event expression in the start condition of a rule repres-
ents an event request, whereas an event expression in the effects part
represents an event offer. An event of a certain type occurs at a certain
gate if an event offer of that type is made by one rule system and an event
request of that type Is made by another rule system. Additionally, the
offered event parameters have to satisfy the constraints imposed by the
requesting rule system. If the event occurs, the parameter values are passed
to the requesting rule system.
In a gate specification, possible event types and their parameter types are
defined, employing the syntax shown in Figure 53. In the
DECLARATIONS-part, the data types of event parameters are given. In the
EVENTS-part, possible event types are listed together with their individual
event parameters. Several gate instances may be created and allow for
the occurrence of events of the event types defined in the gate specifica-
tion. As examples, gate specifications for the gate types
EVENTS
{<event_name> ( <event_parameters> ) ;}
, Other FDTs also use the term 'gate' (lOTOS). or similar terms like 'label' (CCS).
'channel' (Estelle) or 'port' (TCSP).
3.2 Communicating Rule Systems (CRS) 95
EVENTS EVENTS
N CONNECT req (N CR SP); Call request (CR PDU);
N=CONNECT=ind (N=CI=SP); Incoming_call (IC=PDU);
The behavior of a basic rule system may still be complex. The experience
gained during specification case studies for existing protocols revealed a
lack of structuring mechanisms that can be applied to the set of rules in a
rule system specification [Monn89] [Mang90] [Velt90]. As a result, additional
concepts have been developed for structuring the rule set. In particular, the
following mechanisms are provided by CRS:
• contexts,
• views.
If these mechanisms are applied to specifications, structured rule systems
are obtained. Structured rule system specifications are easier to develop
and more intelligible than flat ones. The semantics of structured rule
systems is defined by describing how an equivalent flat rule system can be
constructed that results from expanding all definitions and resolving all con-
texts and views. These mechanisms are explained in the following.
Definitions
Auxiliary predicates are defined in the DEFINITIONS-part of a rule system
specification. A predicate name is defined and a list of formal parameters
may be given. The body of an auxiliary predicate definition is specified as
a formula with state objects and parameters as free variables.
3.2 Communicating Rule Systems (CRS) 97
DEFINITIONS
IF
(upper_window_edge >= lower_window_edge)
THEN
(upper_window_edge - lower_window_edge) < window_size
ELSE
(upper_window_edge + cycle_size - lower_window_edge) < window_size
FI
, Note that the formula' IF a THEN b ELSE c ' is equivalent to ' a "b v -,a" c '.
98 3 Protocol Specification with Communicating Rule Systems
context condition and effects formulas. The syntax used for contexts is given
in Figure 56. If the context condition formula is A-connected to the start
condition formula, and the context effects formula is A-connected to the
effects formula of all the rules in the context, an equivalent flat rule system
is obtained. This is called resolution of contexts.
Different views are defined on the set of rules to focus on different aspects
in a rule system specification. This is done by splitting start condition and
effects formulas of rules into several parts and include these parts under the
same rule name in different views defined in the specification. In this way,
the complexity of rule start condition and effects formulas can be reduced
by separating constraints on different state objects, event occurrences, event
parameters etc. Into different views. The syntax used for views is given in
Figure 57. If the various parts of start condition and effects formulas of the
same rules from all views are A-connected, an equivalent flat rule system is
obtained. This is called resolution of views.
VIEW <view_name> ;
RULES
CONTEXT Call_setup ..•
VIEW Main state and events ...
VIEW User-data handling ...
VIEW Addresses-•••
VIEW Facility handling •••
VIEW Expedited data service .•.
VIEW Receipt confirmation service .••
VIEW Quality-of service .~.
VIEW Timers_and=counters •.•
CONTEXT Data_transfer ••.
Figure 58. Context and view structure of the X.25 PLP specification in CRS
An example of how several parts of rules can be spread over different views
for the case of data transfer in the X.25 PlP is given in Figure 59. A common
condition for all rules describing data transfer aspects of the protocol is
given by the requirement on the state object p_state. which must have the
value p4. Similarly. the value of the state object d_state must be equal to
dl for all rules describing normal data transfer. The focus in the view
Main_state_and_events is on the main state objects (r_state. p_state.
d_state) and on event occurrences. The rules send_data and receive_data
are shown in the example. The data to be sent is passed by the network
100 3 Protocol Specification with Communicating Rule Systems
service user with the event N_DATAJeq, fragmented into pieces according to
the packet size used, and inserted into the ADT object send_queue
(described by the rule fragment_data which is not shown in Figure 59). The
rule send_data is allowed to start as soon as the send_queue contains some
data fragments, which is expressed by using the ADT operation empty on
the ADT instance send_queue. A DATA packet is sent in the effects part of
the rule send_data and the contents of the user_data field is retrieved from
the send_queue.
The data from incoming DATA packets is inserted into the ADT object
receive_queue as specified by rule receive data and retrieved for reas-
CONTEXT Data_transfer;
COND: pstate = p4;
CONTEXT Normal_data;
COND: dstate = d1;
send data;
COND: ' (send_queue.empty);
EFFECTS: Packets. Data (DATA_PDU) A DATA_PDU.user_data = send_queue. remove;
receive data;
COND: - Packets.Data(DATA PDU);
EFFECTS: receive_queue.insert(DATA_PDU.user_data);
VIEW Flow_control;
send data;
COND: window_open(next_to_send, last_ack_received, trans_window_size);
EFFECTS: DATA PDU.p s = 'next to send
A next_to_send = ('next_to_send-+ 1) MOO cycle_size
A DATA_PDU.p_r = 'next_to_receive A last_ack_sent = 'next_to_receive;
receive data;
COND: - window_open (next_to_receive, 1ast_ack_sent , recep_window_size)
A DATA_PDU.p_s = next_to_receive A p_r_valid (DATA_PDU.p_r);
EFFECTS: last ack received = DATA PDU.p r
A next_toJeceive = ('next_to_receive ;- 1) MOO cycle_size;
Figure 59. Contexts and views example for X.25 PLP data transfer specified with CRS
3.2 Communicating Rule Systems (CRS) 101
sembly by the rule reassemble_data (not shown in Figure 59). The flow
control aspects are specified in the view Flow_cont ro 1. An additional
requirement for starting the rule send_data is expressed in this view by
using the auxiliary predicate window_open defined in Figure 55. The state
objects next_to_send and last_ackJeceived marking the upper and
lower edge of the transmission window are supplied as actual parameters,
together with the state object trans_window_size. In the effects part of the
rule send_data in the view Flow_control, the values of the PJ and p_s
fields are specified and the window edges are updated. In a similar way,
flow control constraints are specified for the rule receive_data and windows
are rotated in the effects part. The other protocol aspects that are important
for the rules send_data and receive_data are specified in the other views
as shown in Figure 58, but have been omitted in the example.
State objects of ADTs may only be passive objects according to the classi-
fication of section 3.2.1. An operation is specified by two formulas
describing the precondition and the effects of the operation. The syntax
used for specifying operations Is given in Figure 61. The precondition
formula is a predicate on the ADT's state objects and operation input
parameters. The effects formula relates the new state reached after exe-
cution of the operation and the output parameters to the old state and the
input parameters. As in effects parts of rules. primes are used to refer to
state objects before execution of the operation.
In the example given in Figure 62. state objects for the ADT DataQueue are
declared holding the contents of the queue. the maximum size. front
and rear markers. Two other state objects are used to Indicate whether the
queue is empty or full . The operations defined for the ADT DataQueue
allow for initializing the queue (init). inserting and removing data (insert.
remove). and querying the status (empty. fu 11).
<operation name>;
PRE: - <precondition_formula>;
EFFECTS: <effects_formula>
ADT DataQueue;
STATE
DECLARATIONS
OPERATIONS
init(new size);
PRE: - TRUE;
EFFECTS: size = new size" front = 1 " rear = I
" empty = TRuE" full = FALSE;
insert(data);
PRE: ~(full);
EFFECTS: contents['rear] = data" rear = ('rear + 1) MOO size
" full = (front = rear) " empty = FALSE;
END_ADT OataQueue;
3.2.5 Assessment
The key goal of CRS is to model a system's externally observable behavior
by employing the EFSM model and predicate logic. The combination of
these two well-established approaches and the use of a rule paradigm
yields a powerful FOT. Additionally. the formal definition of CRS is facilitated
by these concepts. In section 3.3, the semantics of CRS as used in this thesis
is defined by using general labelled transition systems (LTSs).
104 3 Protocol Specification with Communicating Rule Systems
Abstraction is achieved with CRS in various ways. The rule paradigm and
nondeterministic selection of rules realizes control abstraction in CRS specifi-
cations. The abstract structure of data objects is separated from the con-
crete representation by using X-ASN.1 as the data description technique. The
CRS mechanisms allow the definition of ADTs and support data abstraction.
The objects and rules of a rule system are only used to specify the
externally visible behavior of a system.
Definition 3.3.1.a - - - - - - - - - - - - - - - - - - - - - - ,
Q is a set of states,
In general, neither Q nor ACT have to be finite. The elements of the set of
states Q are often defined as a cartesian product of several components. If
the transition relation - -+ is a (partial) function - -+: Q x ACT -+ Q, the
resulting LTS is deterministic. otherwise, there may be several transitions
with the same action resulting in different subsequent states [KeIl76]. The set
of actions ACT may contain single events, but also sets of events as ele-
ments. Different semantics of concurrency can be defined in this way.
The active state objects are rule system or gate instances and the passive
state objects are objects of X-ASN.1 types or ADT objects. Rule system spec-
ifications using state objects of both forms are considered as a shorthand
notation for two rule systems, running asynchronously in parallel, with the
state components being separated into the two corresponding forms.
is empty. Basic rule systems represent leaf nodes and their behavior is
defined by rules.
Example:
The rule system Network entityl of Figure 46 is an example of a basic rule system.
The rule system Network=service of Figure 46 is an example of a communicating rule system.
states
Let SV(rs) denote the set of state variables of a rule system 'rs', which are
declared in the rule system specification as
sV1 : type(sv,);
sVn : type(svn);
Primes (' I ' ) are used in CRS to reference state variables holding values of
the rule system state before the actions establishing the effects of a rule are
performed, whereas unprimed variables denote the state after execution of
these actions. Therefore, the following additional set of variables
is introduced, where each I sVj has the same type as sVj (i = 1... n).
108 3 Protocol Specification with Communicating Rule Systems
Let LV(rs) denote the set of local variables defined in a rule system 'rs' in
the form
Local variables are mainly used to save the values of event parameters and
state variables when a rule is started until the effects of the rule are estab-
lished. This is useful because starting a rule (checking the start condition)
and ending a rule (establishing the effects) are considered two separate
actions that might be interleaved with the starting or ending of other rules.
However. some local variables are only used in the start condition and
effects formula. respectively. In this case. these variables represent auxiliary
objects that are introduced to simplify logical expressions.
Exa.ple:
SV{Network_entityl} = {r_state. p_state, d_state,
next to send, last ack received,
next-to-receive, last ack sent,
send=queue, receive_queue~ ••• }
StatVal{Network_entityl} R state type x P state type x 0 state type
x Sequence numbers-x Sequence numbers -
x Sequence-numbers x Sequence-numbers
x DataQueue x DataQueue x -
lV{Network_entityl}
locVal{Network_entitYl}
{see the type definitions given in Figure 36, Figure 37, Figure 38, and Figure 62.}
3.3 Operational Semantics of CRS 109
The behavior of a basic rule system 'rs' is defined by the set of rules speci-
fied in the RULES-part. let
I RULES(rs)
denote the set of rules of the rule system 'rs'. Each rule takes the form
r;
CON D: F cond (IS,,) ;
where Fcond(rI,) is a formula with free variables in SV(rs) U lV(rs) and Fe/Jecls(n,r)
Example:
RULES(Network entityl) = In con req,
- send data, receive data,
fragment data, reassemble data,
send_expedited_data, receive_expedited_data, .•• J
Feond (Network_entityl, "_con_req) and Feffects (Network_entityl, "_con_req) are given in Fi gure 50.
After a rule has been started, the values saved in local variables belong to
the execution state of this rule. The set of execution states of rules is defined
as
where P(s) denotes the powerset of a set s. In a similar way as for state
variables, let 'lV(rs) denote the set of local variables holding values before
the actions establishing the effects of a rule are performed and lV(rs) the
set of local variables of the effects formula.
The state of a basic rule system 'rs' comprises the values of all state vari-
ables and the execution state of all running rules. The set of all possible
states Q,. is given by the cartesian product
Example:
The set of rule systems composed in parallel in the rule system Network_service is:
RS(Network_service) {Network user!, Network user2,
Network-entity!, Network entity2,
Network) -
The following examples illustrate how states from QNe~~1 are formed.
However, only some excerpts of the whole cartesian product can be shown:
qNetwork enlily10
= (( r I, pI, dI, e, e, e, e, ••• ), ({})
qNe~-~11 =
((r1, pI, dl, e, e, e, e, ••• ),
({(n con req,
(("called", "calling", FALSE, TRUE, {••• }, "hello"},
{{FALSE, FALSE, modulo_8, e, I}, 'eeeeI91l'B, 5, 5, "12345", "67899", e, "hello"},
) ) } ) )
qNeIwOlk_enIily1 2 = ((rl, p2, dl, e, e, e, e, ••• ), ({})
The three examples above refer to states of the rule system Network entityl. The rule
n_con_req can be started in the state qNeIwOlk e~10, n_con_req has been started and is
running in the state qNe~enlily11, and it has been ended and cannot be started in the
state qNe~ enIiIy1 2• These examples are used later in this section, when the requirements
for starting-and ending rules are formalized.
The following examples illustrate how states from QNelwOlk~M1 are formed.
Since the specification of the rule system Network userl-was not given in section 3.2,
the cartesian product is not detailed. However, it-is assumed that the rule
estab 1i sh _connect ion is runn i ng ; n the state qNelwOlk userl l and that ; tis no longer
runn i ng in the state qNetwork_USe,1 2. -
Actions
According to the classification, a basic rule system cannot use gate
instances as state objects, but only request or offer events at gates given to
the basic rule system as actual parameters in the instantiation. The gates
given as parameters to a rule system instance form the interface of this rule
system to the environment for both basic and communicating rule systems.
The events occurring at those gates are external events, perceptible by an
external observer. In communicating rule systems, gate instances may be
used as state objects to be shared by rule system instances. The events
occurring at those gates are internal events, not visible for an external
112 3 Protocol Specification with Communicating Rule Systems
observer. Thus, two sets of gates are derived from the STATE-part of the
specification of a rule system 'rs':
The set of gates of a rule system 'rs' and the overall set of gates in a CRS
specification is defined as
With each geGATES, a finite set ETYP(g) of valid event types is associated
having the admissible parameter domains EPAR(g,etyp).
Exa.ple: (the gate specifications are given in Figure 54)
Ext_gates(Network_entityl} ~ {NSAPl, Packetsl}
Int gates(Network entityl} & {}
Ext=gates(Network=service} • {}
Int_gates(Network_service} • {NSAPl, NSAP2, Packetsl, Packets2}
GATES(Network entityl} ~ {NSAPl, Packetsl}
GATES - • {NSAPl, NSAP2, Packetsl, Packets2}
ETYP(NSAPl} = {N_CONNECT_req, N_CONNECT_ind, ••• }
EPAR(NSAPl, N_CONNECT_req} = N_CONNECT_request (see Figure 38)
Definition 3.3.2.a
The events occurring at a gate 'g' have to be of an event type 'etyp' that
has been defined for 'g'; events may convey parameters 'epar' from the
parameter domain determined by 'etyp'. An event without parameters is
treated as a special case with an empty parameter domain. Each event
either represents an offer, request, or event. The set of events includes the
Internal event, not visible to the external environment. The symbol I is used
to denote an anonymous gate for the internal event type with no parame-
ters.
aR1 = e1
a0 1 = e2
aE1 = e 1
aO = (a E1 , event)
a1 = (a R1 , request)
a2 = (a 0 1 , offer)
Let
I requests(rs, r)
be the set of event requests (possibly empty) belonging to the Feond (r>, r)
formula of a rule 'r' in a rule system 'rs'. Each event request is of the form
114 3 Protocol Specification with Communicating Rule Systems
where
g E GATES(rs),
etyp E ETYP(g),
lY(req) is a tuple of local variables in LV(rs) denoting the requested event
parameters.
Similarly, let
Ioffers(rs, r)
be the set of event offers (possibly empty) in the F.""ct.(rs.r) formula of a rule
'f' in a rule system 'rs', with elements
where
g E GATES(rs),
etyp E ETYP(g),
Moff) is a tuple of local variables in LV (rs) denoting the offered event
parameters.
For a logical evaluation, the requests and offers in rule start condition and
effects formulas have to be regarded as propositional variables. To deter-
mine the truth value of the whole formula, an assignment function
is required. This assignment reflects the state of the rule system (state vari-
ables), the execution state (local variables) of the rule, and information
about occurring events.
3.3 Operational Semantics of CRS 115
Example:
requests(Network_entitYl, n_con_req) = {(NSAP1, N_CONNECT_req, (N_CR_SP»}
Compatibility of two rules is expressed by using the parallel (II) and semi-
parallel (~) operators. Priority of a rule is defined by using the prior (-<)
operator. If the SYN-part is empty, so are the relations comp and prIor.
Thus, all rules are mutually exclusive and the choice which rule to start
among those that are startable with respect to state and communication
reqUirements is nondeterministic.
For starting a rule 'r' in a basic rule system 'rs', the start condition of 'r' has
to be satisfied. Let 'actoffs' s;; EVENTS be a set of actual event offers which
are mapped by an injective function 'q/ to some or all of the event requests
of the rule 'r' (those which evaluate to 'true' in Fcond(rs,r». The requirements on
the given state of 'rs' and given event requests are summarized in the fol-
lowing predicate:
116 3 Protocol Specification with Communicating Rule Systems
Definition 3.3.2.b - - - - - - - - - - - - - - - - - - - - - - ,
The predicate startable expresses that in order to start a rule 'r' in a rule
system 'rs' in a 9iven state 'q' with actual event otters 'actotts'. the start
condition must be satisfied and the actual event otters have to match the
event requests of the rule 'r'. The values of the local variables of the rule 'r'
must be equal to the values of the ottered event parameters.
Definition 3.3.2.c - - - - - - - - - - - - - - - - - - - - - ,
The predicate endable expresses that in order to end a rule 'r' in a rule
system 'rs' in a given state ' I q' with actual event requests 'actreqs',
resulting in the new state 'q', the effects formula must be satisfied and the
actual event requests have to match the event offers of the rule 'r'. The
values of the local variables of the rule 'r' must be equal to the values of
the requested event parameters. In addition, the rule 'r' must be running in
the state" q'.
Example:
The predicates
and
Recall from Definition 3.3.1.a that an LTS is defined by a set of states, a set
of actions, and a transition relation between states labelled with actions.
Since rule systems are based on the EFSM model, the state space of the LTS
is defined by the state objects. The transition relation is determined by the
rules controlling internal and external actions of rule systems.
As far as the action set of the LTSs is concerned, the definition is not so
straightforward. Generally speaking, the elements of the action set are the
atomic observations that can be seen when observing the system and the
transition relation determines the possible temporal orderings of these
observations. Choosing different forms of atomic observations has a large
impact on the semantics of concurrency [Aceta 7].
118 3 Protocol Specification with Communicating Rule Systems
In CCS [Miln80] and CSP [Hoar85]. single events are regarded as the atomic
observations and the resulting semantical model is called Interleaving
semantics. Concurrency between systems performing a set of actions is
expressed by allowing actions to occur in any total order. This view suffices
to model the behavior of most concurrent systems.
The semantics for CRS defined in this section is based on the interleaving
model. This is because interleaving semantics is considered to be sufficient
for protocol engineering tasks to be supported in an integrated tools envi-
ronment as presented in chapter 5 of this thesis.
The tool support is based on operational formal descriptions that are exe-
cuted by runtime mechanisms in the kernel of the environment. These
runtime mechanisms are more easy to develop and they work more effi-
ciently if interleaving semantics is assumed. A multiset semantics for CRS
has been defined in [Schn90a].
Using the auxiliary definitions given in section 3.3.2. the behavior of a basic
rule system 'rs' without rule priorities (WP) is described by the following lTS:
3.3 Operational Semantics of CRS 119
Definition 3.3.3.a - - - - - - - - - - - - - - - - - - - - - - - ,
The labelled transition system LTS"WP for a basic rule system 'rs' without
priorities is defined as
ACTn := ACTIONS
v
( 3 a o• actreq:
(a = (a o• offer) 1\ actreq = tao} 1\
3 endruleeRunRules(rs): 3 lY..oorule: 3 'IY..ndrute:
( endable(endrule. actreq. 'q". q". 'IY..ndrule' IY..ndrule)
1\ rrlv = 'rrlv \ {(endrule. 'IY..ndrule)} ) ) )
satisfy the requirements for a rule start or end. one rule is selected in a
nondeterministic fashion.
Example:
The transitions
and
Definition l.l.l.b
The labelled transition system LTS" for a basic rule system 'rs' is defined
as
ACT" := ACTIONS
This definition makes use of the previous one by stating that a transition of
LTS" must be a possible transition of LTS"WP as well. However. the following
restriction is defined: if the transition action 'a' represents an event request
'a R' of a rule that is started ('startrule a /). then all other rules with the same or
3.3 Operational Semantics of CRS 121
another event request 'aR" that could have been started as well ('startrule"!!,')
must have the same or lower. but no higher priority.
Example:
With the specification example of Figure 51. a transition of LTSNe~~ enmy, with
rule send data as the 'startrule' is not possible if a transition wit" rule
send_expedited_data as the 'startrule' is possible as well.
Definition 3.3.3.c
The labelled transition system LTScrs for a communicating rule system 'crs'
is defined as
~n := Q.., x ... x ~
ACTc,. := ACTIONS
The "distributed" LTScrs of the communicating rule system 'crs' may perform
a transition with an event request (aR) or offer (a o ) at one of the external
gates (event classes request and offer) as the transition action if there is a
component rule system 'rs' making the request or offer during a transition of
its "local" LTS (first two cases in the definition). If the transition action is of
the class event. there have to be two distinct component rule systems 'rsreq'
and 'rsoa' performing transitions with the same event (a f ) tagged as request
for 'rsreq' and as offer for 'rsol" These rule systems participate in a two-way
rendezvous. The behavior of the communicating rule system 'crs' is
described by the possible transition sequences of LTScf$'
Example:
With rSreq = Network_entityl, rs ol = Network_userl, the transition
3. The possible set of states and actions and the definition of the transition
relation of an LTS provides complete information for building specification
interpreters and runtime environments for the simulated execution of
formal descriptions. The executability of the specification can be
exploited in various ways by tools supporting the system development
life-cycle.
3.3 Operational Semantics of CRS 123
The focus of this thesis is on the last item of this list. A runtime environment
for the CRS language, a way of achieving operational specifications, and an
integrated tools environment for developing communication systems is
described in chapter 5.
124 3 Protocol Specification with Communicating Rule Systems
4 Protocol Engineering with Formal
Description Techniques
can be generated from the PASS graph as well. The resulting "PROLOG"
program represents an executable version of a PASS specification. Unfortu-
nately, PASS specifications only capture the state machine aspects (no data
aspects) and only allow deterministic behavior.
• data structures representing the static net structure (places and transi-
tions);
In the PROSIT simulator, places are identified with integer numbers and a
pointer array is used for referencing token objects present at places during
runtime. All token objects that are created and deleted during runtime are
kept in a global object pool. Transitions are represented by the numbers of
connected places, pointers to token objects that are moved when the transi-
tion occurs, and information about the type and number of tokens. The net
markings are stored in a three-dimensional table holding the number of the
marking, the actual object pool, and object pointers for each place.
After the net specification has been compiled, the net components can be
displayed and edited using a graphical editor in the PROTEAN system. The
130 4 Protocol Engineering with Formal Description Techniques
specification objects appear one after the other and can be adjusted on
the screen by the user of the tool. When starting a simulation, the initializa-
tion code is executed and the initial marking of the net Is displayed.
Zooming functions are available to focus on specific parts of the net. All
transition conditions are evaluated and the set of enabled transitions is dis-
played (either graphically by highlighting or using color, or textually In form
of a list). The user of the tool selects an enabled transition and the transition
actions are executed, resulting in a new marking. The net markings
reached during net simulation are saved for backtracking purposes. The
whole, or selected parts of the reachability graph of a net can be gener-
ated this way.
For the Interactive use of Petri net simulators sophisticated graphical user
Interfaces are required. In an automatic mode, nets can be thoroughly ana-
lyzed with respect to various properties (reachablllty, Invariant conditions
etc.). The structure of data objects In a net specification is, however, rather
simple in most tools. As a consequence, the net simUlation is done at a low
level of granularity. Generating the reachability graph for protocols of real-
istic size causes both space and efficiency problems.
4.1.3 LOTOS
Interpreters for LOTOS are described in [Legr88] (ISLA) and in [Tret89]
[Eijk89b] (HIPPO). The interpretation is based on term rewriting techniques for
both the behavior and the data part of LOTOS. The semantics of LOTOS has
been defined using labelled transition systems, where the transitions
describe the transformation of behavior expressions after performing inter-
actions. Abstract data types are defined In LOTOS using the algebraic spec-
ification language ACT ONE. Consequently, the semantics of both parts of
the LOTOS language can be directly implemented as rewrite rules.
In the ISLA simulator, the rewrite rules for behavior expressions are Imple-
mented as "PROLOG" rules (see [Logr88]). As an example, the semantics of
the choice-operator In LOTOS is expressed as a "PROLOG" rule in Figure 63.
The interpreter runs on the Internal "PROLOG" representation implementing
the dynamic semantics of LOTOS as defined in [IS08807]. Whenever a value
expression has to be evaluated, an ADT interpreter is called as a subordi-
nate routine, using a "Ieftmost-Innermosr' evaluation strategy. The rewrite
4.1 Executable FDTs 131
rules for the ADTs in a specification are generated by a front-end tool after
parsing the specification and checking the static semantics.
The HIPPO simulator (see [Eijk89b] [Tret89]) also uses term rewriting to
compute possible continuation alternatives from a given behavior
expression as the result of a 'menu' function. The user of the tool has to
make a selection and has to supply Interaction parameters before Invoking
the 'next' function. LOTOS semantics in the form of communication trees
are used as the underlying formalism (see [Eijk88]). The tool has been
implemented in "C".
"PAR LOG" programs have been designed to behave like LOTOS processes
and gates.
Some work has been started recently on transforming LOTOS processes into
state machines [Eijk90b] [Mana89]. The approach has been theoretically
treated in [Karj88]. A prerequisite to accomplishing the transformation is that
the input specification is close enough to an implementation. Ideally, the
specification has been written in a state-oriented specification style
[Eijk90b]. The behavior part and the data part are kept separate. The tool
described in [Mana89] generates a finite automaton for each behavioral
unit in the specification that synchronizes with others. Each LOTOS process is
compiled into a reentrant "c" function that is executed as a separate oper-
ating system process. A complex runtime kernel using system calls to deter-
mine possible mUlti-way synchronizations is required. In the approach
described in [Eijk90b] this was avoided for efficiency reasons. Instead, a
given LOTOS specification is transformed by a tool implementing the LOTOS
expansion theorem. By applying this theorem, parallelism (and thus the
need for communication) is eliminated by introducing nondeterminism. For
the data part, the tool described in [Mana89] derives a rewrite system. In
the implementation experiment reported in [Eijk90b], ADTs have been trans-
lated manually.
the "PROLOG" interpreter tries to reason backwards from the goal to pos-
sible solutions. It searches a clause for which the head of the clause
matches the goal C, normally consisting of a predicate symbol and argu-
ments in form of constants, variables, or terms (for example, C = P( t 1 •
• • •• tm ). A more concrete example is given later. A matching clause
B +- A1 . . . . . A"
have been found for all subgoals. The "PROLOG" interpreter tries to solve
subgoals from left to right (resolving "AND"-nondeterminism) and searches
for matching clauses in the order given in the logic program (resolving
"OR"-nondeterminism). Whereas the order of solving subgoals (computa-
134 4 Protocol Engineering with Formal Description Techniques
tion rule) has no impact on the number and results of successful computa-
tions, the selection of matching clauses Is important. If the computation
does not succeed with a selected clause, backtracking is performed and
the next matching clause is taken. This is done in a depth-first manner and
may lead to infinite loops if recursion on the same clause occurs over and
over again. Breadth-first search was not implemented because of enormous
space requirements. The whole computation is performed on a symbolic
level. Unification. the most time-consumlng step, relies on pattern matching
algorithms.
where Sand 0 are variables. The "PROLOG" system will find a successful
computation, which states that there Is a transition from the state pI with the
input N_CONNECTJeq. Additionally, the system will find the answer substi-
e,
tution where
8 ={S -+ p2 , 0 -+ Call_request} .
logic interpreters can be used for multiple purposes on the basis of a single
logic program. This feature has been called Invertible execution in
[Boch86]. If the behavior of a protocol entity is specified as a logic program,
different goal clauses can be used to get information about transitions. The
focus can be on output and states, on states accepting a certain input, on
subsequent states from a given initial state etc.
• a control part,
both given as Horn clauses. The logic part represents the knowledge about
the problem domain, whereas the control part specifies how to use the
knowledge for generating answer substitutions.
logic interpreters are elegant tools for executing specifications with various
intentions in mind. However. care must be taken in the control part of a
logic program when providing clauses to achieve the intended goals
because of their relationship to the clauses of the logic part representing
the problem-specific knowledge. The efficiency of the interpretation
depends on the efficiency of the paHern matching algorithms. Serious prob-
lems are caused by possible infinite computations. Several "non-logical"
constructs have been invented in "PROLOG" ("cut" etc.) in order to avoid the
exploration of infinite paths. The fact that problem-specific knowledge and
control-oriented clauses are mixed in a logic program. and the inflexibility
of the interpretation algorithm are considered drawbacks of "PROLOG" as a
tool for executing specifications of communication services and protocols.
For service specifications, the user of these tools checks whether the speci-
fied behavior reflects the informal requirements by watching interaction
sequences and examining their accordance with local and global service
constraints. Given a protocol specification, the simulated behavior of the
protocol can be compared to the service specification. Particular transitions,
states, encoding/decoding of PDUs and the mapping between PDU fields
and SP parameters may be investigated. In an interactive simulation, a
certain number of interesting situations can be explored to validate specific
properties expected from the specification. In long lasting automatic simu-
lations, the aim is at finding deadlocks, livelocks, or other kind of erroneous
behavior. Such situations may be recognized during a simulation by ending
up in some unexpected state, looping without progress, receiving inappro-
priate or corrupted messages etc. Although complete certainty about
general properties of a specification cannot be reached, the confidence in
the correctness of a design is increased.
The number of alternative paths and situations that may be explored in rea-
sonable time during the simulation of a specification depends on the flexi-
bility of the simUlation tool. Facilities have to be provided for driving the
simulation to areas of interest, for retrieving information in each state, and
for entering data conveniently. In ESTIM and VEDA, a user interface in the
form of a command interpreter is employed. It has been pointed out in
[Jard88] that such an interface is not user-friendly enough. Only closed
systems that do not interact with the environment (the user of the tool) can
be simulated in VEDA In PATE/PACO, an external procedure is called during
execution of each input/output transition. For the purpose of validation this
procedure receives input from and directs output to a human operator. In
order to simulate systems sharing interaction points with the environment,
so-called user-driven transitions can be selected in WISE. The window inter-
face of the SMALLTALK system under which WISE was realized provides the
138 4 Protocol Engineering with Formal Description Techniques
• absence of deadlocks;
• absence of Iivelocks.
The main issues that have to be resolved during the compilation of protocol
specifications are layer structuring (threads, processes, procedures etc.),
communication between layers (interrupts, messages, procedure calls etc.)
and nondeterminism (scheduling, transition ordering etc.). A comprehensive
overview of implementation issues for 051 communication systems is pro-
vided in [Svob89]. As reported in [Vuon88], generated code contains fewer
errors and allows cheaper and faster protocol implementation. The effi-
ciency of manually-coded implementations, on the other hand, was not
achieved.
Whereas for lower layer protocols in the 051 model the control aspects con-
stitute the major part of an implementation, the situation changes in the
upper layers. In the application layer, application entities exchange struc-
tured data objects. This data has to be encoded into a common transfer
representation of the open system at the sending site and decoded at the
142 4 Protocol Engineering with Formal Description Techniques
ferent providers, testing each implementation against all others is not fea-
sible. Instead, each implementation under test (fUT) has to pass a number
of test cases of a standardized test suite. The importance of international
conformance testing efforts has been widely recognized as being crucial for
achieving the objectives of 051. The ISO and CCITT standards committees
are currently jointly developing a common methodology and framework for
conformance testing [1509646]. Surveys of this work can be found in
[Rayn87] [Sari89] [Linn90].
For all these different tasks, tool support is desirable and is currently the
subject of intensive research. A software environment for protocol testing
would ideally combine tools supporting all the activities above.
Test suite development is still a manual activity requiring much effort. The
development of standardized test suites for 051 protocols is currently con-
ducted by a number of experts from different institutions. The development
process is, however, quite slow and international acceptance is hard to
achieve. Besides speeding up the development process, automated test
suite development is desirable for at least two more reasons. Firstly, devel-
oping good test suites for communication protocols is a complex task due
to the concurrent and distributed execution of a protocol by several entities
and the various implementation options. Secondly, assuring correctness of
144 4 Protocol Engineering with Formal Description Techniques
test cases with respect to the informal protocol standard is difficult. By using
formal descriptions, "quality" measures for test suites can be defined math-
ematically and can be related to the specifications. The test cases gener-
ated from formal descriptions according to formal methods are inherently
correct with respect to the specification.
One problem with all these FSM-based methods is that they do not take
any data aspects into account. The question may be asked as to why each
transition is tested only once and not several times with varying data
parameters. Testing single transitions is not adequate, but possible event
sequences and parameter dependencies have to be considered. A test deri-
vation algorithm taking both control flow and data flow into account has
been proposed in [Ura187] and realized in a corresponding tool. Protocol
speCifications in Estelle serve as Input and are first transformed into a
normal form. Then, the underlying state machine graph, as well as the data
flow graph representing possible data flow between variables and inter-
action parameters are constructed. The test sequences derived from both
graphs aim at covering all "definition-usage" pairs. This way, errors may be
found that are related to variable usage without some defined value, or vari-
able definitions that are not used by the protocol. Test case derivation from
LOTOS specifications is still not as practical as the approaches described
above. The theory developed in [Brin88b] has been implemented in the
tools described in [Weze90] and [Alde90]. but the canonical testers gener-
4.2 Protocol Engineering Environments 145
Another problem encountered for test case generation tools is the output
format. Many tools use their own test description languages without any
formal semantics. For international distribution and for gaining mutual
recognition of test results by various parties, different test languages are not
appropriate. Therefore, ISO is currently developing a standardized test nota-
tion called the Tree and Tabular Combined Notation (TTCN). The definition
of HCN will become part of the ISO conformance testing standard
[1509646].
The ISO standard [1509646] also provides a framework for test case exe-
cution by detining several so-called abstract test methods, which are actu-
ally test configurations. The most important one is the distributed test
method, depicted in Figure 65. The functionality of the tester is divided into
an "upper tester" part, watching and controlling the upper service interface
of the IUT, and a "lower tester" part, exercising control and observation of
the IUT's lower service interface from a remote site. So-called Points of
Control and Observation (PCOs) exist in the distributed test method
between the IUT and the upper tester, and between the lower tester and an
146 4 Protocol Engineering with Formal Description Techniques
,-- f----
Test Coord.
LT Procedures UT
~
I-
I ASP s
. - PDUs -----.
1 ASPs
IUT
Service Provider
underlying service provider. The lower tester resides in the system where the
test is executed and is usually the major component of the whole test tool
(test driver). Normally, the upper tester is a relatively small module which
can be easily ported to different systems (test responder). The test system
is connected to the IUT via the underlying service provider, which may
involve a real network. Various forms of upper and lower testers are pos-
sible, however. A survey is provided In [Rayn87]. Test tools for the test
methods introduced in [IS09646] are described in [Mack88] [Chan90]
[StoI90].
Several existing FDTs have been evaluated in chapter 2 to assess their suit-
ability for specifying communication systems. Because of deficiencies in
these FDTs. a rule-based technique for the specification of communication
services and protocols has been proposed in chapter 3 (CRS. X-ASN.1). The
advantages of CRS in relation to a number of general criteria for FDTs and
the representation of architectural concepts of open systems have been
explained. This chapter shows the relevance of using CRS and X-ASN.1 for
building tools to automate protocol development. A protocol engineering
approach is described that is based on the constructive nature of CRS spec-
ifications. allowing specifications to be executed according to the opera-
tional semantics defined in chapter 3.
1. a rule base,
3. a rule interpreter.
The data base is used to store information about the problem domain and
Its actual state provides the basis for evaluating the condition part of pro-
duction rules. The actions of production rules may alter the state of the data
base. The rule interpreter usually works In a cyclic fashion and repeats the
following steps In each execution cycle: (1) find all rules in the rule base
applicable to the present state of the data base (matching), (2) select one
applicable rule (conflict resolution), (3) perform the actions of the selected
rule (action). If the rule interpreter starts from an initial state and applies
rules to work towards a goal state, it is called forward-chaining. If it tries to
reason backwards from a goal state to an initial state, it is called
backward-chaining. Since the rules in the rule base are used to infer new
knowledge from existing knowledge, the rule interpreter in a production
system is also called inference machine [Kric88].
objects constitute the data base. The mapping between specification and
implementation is illustrated in Figure 66 for two rule systems (RSl, RSZ)
communicating over a common gate (Gate). Each rule system is executed
by an associated CRS inference machine exercising control over the rule
base. In order to facilitate communication between rule systems, each gate
is handled by a CRS gate machine gathering event requests and event
offers from the inference machines and looking for matching pairs.
'0' D
RSl
D
Gate RS2
raque.t r-.qu •• t
. ofr.r offllr
~
.. 01f.r • ~
oU.r
requ •• l
reque,t
+ + +
• translation or
• Integration.
In the translation approach, the X-ASN.1 type definitions are translated Into
corresponding types in a target language. Variable declarations are gener-
ated for each X-ASN.1 data Instance and the X-ASN.1 operations are
mapped onto operations, functions, or procedures in the target language.
The ASN.1 compilers described In [Gora88a] and [Neuf90] are typical exam-
ples of tools realizing the translation approach, both using "C" as the target
language. For some ASN.1 types, the translation into "c" Is straightforward.
For example, the simple types INTEGER, REAL, and ENUMERATED have direct
counterparts in "C". Types constructed with the SEQUENCE and SET
constructors are mapped onto structured types in "C". However, there are
also ASN.1 simple types, as well as ASN.1 structured types, which cannot be
translated directly because adequate constructs do not exist in "c" (or in
similar programming languages).
Besides the difficulty of finding adequate representations for the ASN.1 types
in the target language the main disadvantage of the translation approach
is that the processing of data objects according to a protocol or service
specification has to be implemented using the generated type definitions in
the target language. Thus, checking the presence of optional fields, man-
aging list structures, handling strings etc. is the responsibility of the
implementor and is difficult to validate. A library of runtime routines can be
provided to support developers, but some parts have to be generated for
each ASN.1 type module (for example encoding/decoding routines) (see
[Gora88a]).
Representing X-ASN.1 type definitions and values in the form of tree data
structures is appealing because of the dynamic properties of X-ASN.1 data
objects. Tree structures are flexible and can be used to represent simple
types (just one node), structured types (hierarchies or lists of nodes), and
nested types (referenced subtrees). Nested types can be defined using
other structured types as components, or using the same type as a compo-
nent. In the latter case, recursive types are obtained and the tree structures
representing them are actually graph structures.
154 5 Protocol Engineering with Communicating Rule Systems
The idea is illustrated in Figure 67: the X-ASN.1 type definitions are con-
verted into an internal tree representation, called a structure tree (as for the
type Data in the example). Structure trees are available for retrieving type
information at runtime. The values of the different types are represented as
so-called data trees corresponding to structure trees (example value repres-
entations are given on the right-hand side of Figure 67). Generic
encoding/decoding routines can be designed to work for arbitrary X-ASN.1
data instances based on their underlying structure trees holding the type
information.
r---------- -+ selector
i type
structure
-- ----- -------...... block
! tag information
SYMBOL
TABLE size constraints
OPTIONAL indication
I
1
child block
Different fields in a structure block contain the component selector, the type
of the component (a reference to another structure block), the tag class,
number, and use of the IMPLICIT keyword, information about size con-
straints, and an indication whether the component is classified as optional.
In addition, an index number is assigned to each structure block, so that
the type representations are accessible via selectors from a symbol table,
or via indexes from an index table. The remaining fields are pointers to
parent, sibling, and child blocks in a structure tree.
2 I
CQ~4I~
.;$:
;.;:~ ..!:!;. - -
SEQLHCE
.y.:........ ~~:
25 JO J2
......
29 ,31
r;.~"
001'"-#"'-
::.""t'". . . raClIUty_
lenvth
Mcnltl•• u-.. rJGtA
• rsi7611C I-~
~ Jl{TQ;£R S01I.£/CE
ogCf'-
1m 111 • •1£1 c'O .. W III • • "
Figure 69. Structure tree tor the X,25 CALL REQUEST packet type
Data trees refer back to their structure trees and are dynamically created
and deleted during runtime. Arbitrarily many data tree representations may
exist corresponding to a single structure tree, which is only represented
once. The nodes of data trees are formed by data blocks, pointing to struc-
5.1 Executable CRS 157
s
y
M
B
o 1-----I
L I
T
A
B
L
E
S8: structure block
INDEX TABLE
ture blocks (see Figure 71). For identifying the structure block a data block
belongs to, the index number of the structure block is used. The value of the
field associated with the data block is some concrete representation in the
case of simple values, or a pointer to a subtree in the case of structured
values. The remaining fields in data blocks are pointers to the parent, child,
and sibling blocks.
parent block
iI structure
block
1
child block
The representation of structured values requires several data blocks for the
components to be linked according to the type structure (see Figure 73). A
possible value of the CALL_REQUEST type (see Figure 69 ) is represented as
a data tree in Figure 72. Inner nodes of the tree just carry the structure
block index and pointers to the components, whereas actual value informa-
tion is present in leaf nodes. In the particular instance depicted in
Figure 72, the optional component f ac il it i es of the CALL_REQUEST type
has been omitted. Data tree instances can be associated with an identifier
and written to a file according to an external format. Using the identifiers,
particular data trees can be loaded again at some later stage.
Since data trees point back to their corresponding structure tree, the tag
information stored in structure blocks, together with the value information in
data blocks, may serve as input to generic encoding/decoding routines.
The encoding/decoding is guided by the type structure given in the struc-
ture tree. The routines convert from data trees as the local syntax to byte
sequences in a transfer syntax (for example, defined by basic encoding
rules) and vice versa. Since the type information is passed as a parameter
.V .::1
simple value
structured value
to the routines, they can be designed in a generic fashion and need not be
generated for each user-deflned type.
Each CRS inference machine organizes the rules of its associated rule
system in different sets according to the execution state of the rule, as
shown in Figure 74. Rules may be blocked, ready, or running, similar to
processes managed by a dispatcher (see for example [Nehm85]). Besides
the actual values of the state objects, the execution state of all rules and
the values of the local objects of all running rules determine the state of a
rule system. As long as no rule is being started or ended, all rules are in
one of the three main rule sets:
Wstate which contains all rules that are not running and for which the start
condition is false due to a non-qualifying state (Wait for state);
ILcommitted
9
10
Wstote WES
WES which contains all rules that are not running and for which the start
condition is true with respect to the current state, but the rules are
requesting an outstanding event or are incompatible with some
running rule (Wait for Event or Synchronization);
Run which contains all rules that have been started, but not yet ended
(Running)-.
The inference machine ensures that these rule sets are always maintained
according to their meaning. Consequently, when a rule has been ended
and the actions establishing the specified effects have been performed,
rules may have to be transferred between the sets Wstate and WES (transi-
tions 9 and 10 in Figure 74). Single element sets named Start,
R_commlHed, and End serve as intermediate sets for transferring rules to
and from the set Run. These intermediate sets are needed in case of syn-
chronous communication as will be explained later. Startable rules are
taken from the set WES and are transferred to the set start (1). The accept-
ance of an event by the selected rule is indicated to the corresponding
gate machine.
Before a rule is started, it remains in the start set until the gate machine
acknowledges the acceptance of the event after having informed the
offering inference machine in case of a synchronous event (the details of
the protocol are explained later). A rule is started by transferring it from the
set start to the set Run (2). Once being in the set Run, a rule is called
"running".
A running rule with an asynchronous event (or without an event) in its effects
is ended by transferring it directly to the set End (3), performing actions
establishing the specified effects, and then passing it from the set End to the
set Wstate (7) or WES (8), depending on the current state of the rule system.
If a rule offers a synchronous event in its effects and a corresponding event
request is given, the event parameters are passed to the gate and the rule
is transferred to the set R_commlHed (4). If the event offer is accepted, the
- Remember that starting and ending a rule occur at two different pOints in time.
162 5 Protocol Engineering with Communicating Rule Systems
rule can be ended by transferring it to the set End (6). If the offer is refused,
the rule is transferred back to the set Run (5). A new aHempt to end the rule
Is made when a new event request arrives, or the values of the event
parameters change.
If the three single element sets start, R_commlHed, and End are empty, the
rule system is in an idle state. otherwise, at most one of these sets contains
a rule and no actions can be performed for the rule system until an answer
from the gate machine involved is received. The reception of gate machine
messages may trigger a rule start from the set Start, a rule end from the set
End via the set R_commlHed, or an unsuccessful termination from the set
R_commIHed. Start condition checks and actions establishing effects can
be executed atomically while the rule system state Is fixed.
The set model is further detailed for the sets WES and Run. The WES set
unfolds into three disjoint subsets as depicted in Figure 75. The Ready set
contains the rules having no event request in their start condition (8b, iDa)
and the rules coming from the set Wsyn (12). These rules may be imme-
diately selected for a rule start (1a). Rules are transferred to the set Wsyn
(8c, 10c, ii, 13) if they are not compatible with some running rule (see the
definition of the compatibility relation in chapter 3). Rules waiting for an
event are contained In the set Wevent (8a, 10b) and may be selected for a
rule start if a matching offer is indicated by the corresponding gate
machine (1b). These rules remain in the set Wevent if the event parameters
are not acceptable (15). Rules in the set Wevent are transferred to the set
Wsyn as soon as a rule is started with which they are not compatible (11).
When the conflicting rule is ended, these rules reach the set Ready (12). If a
matching event offer is still missing for these rules, they are again trans-
ferred to the set Wevent (14). If a rule being ended alters the rule systems'
state objects In such a way that the start condition of a rule in the set WES
is no longer satisfied, the rule is transferred from the set WES to the set
Wstate (9a, 9b, 9c). Rules have to remain in the set Wstate if there is a
matching event offer for them, but give a negative response to the gate
machine during transition 17.
Similar to the set WES, the set Run is split into three sets: R_fire, R_wfc, and
R_wfc_p, as shown in Figure 76. Rules with an asynchronous event offer (or
5.1 Executable CRS 163
End
without an event offer) are contained in the set R_flre (2b). Rules with a
synchronous event in the effects are collected in the set R_wfc (2a). These
rules have to be ended via the set R_commlHed as explained above (4b).
If the attempt to end a rule is not successful because the offered parame-
ters are wrong, the rule is put into the set R_wfc_p (Sa). If other reasons
prevented the successful termination, the rule is transferred to the set R_wfc
(5b). From the set R_wfc_p, a rule may be selected again for termination
(4a) if there is another matching request. Rules are transferred back to the
set R_wfc (18) if the parameter values have been changed due to another
rule end.
Organizing rules this way leads to increased efficiency of the CRS inference
machines by means of a dedicated search mechanism. No pattern
matching techniques are employed for searching rules to be started or
ended. The different rule sets help restricting the number of rules to be
examined at each step. The overhead of maintaining the rule sets can be
kept small by using efficient implementation techniques for sets. Which rules
are potentially enabled or disabled immediately after ending another rule
can be determined by a static data flow analysis. This information can be
utilized to increase the inference machine's intelligence [Neum88].
(3
11
CONF_REQUEST
NO-EVENT
\
(I rue)
IND...MATCHJEQ IND...MATCHJlEQ
CONF REQUEST
f
~
(fal ••
check_requestsoO
IND...MATCH_OFFER
The possible incoming messages from inference machines are the fol-
lowing:
The protocol for a synchronous gate machine works as follows: in the state
Idle, arriving requests (message INO_REQUEST) are stored if no matching
offers are found (transition 2 in Figure 77). If matching offers are present, a
transition to the state check_offers is performed (1). Then, the message
5.1 Executable CRS 167
The protocol leaves open several possibilities to continue from the state
walt_for_conCrequest. A positive CONF_REQUEST message may arrive,
causing the event to occur and the message EVENT to be sent to both infer-
ence machines (5). In case of a negative CONF_REQUEST message, one of
the remaining matching offers is checked by performing a transition to the
state check_offers (7). The message NO_EVENT is sent to the offering infer-
ence machine. Alternatively, there may be matching requests remaining for
the offer received (6). The next request is selected and the message
IND_MATCH_OFFER is sent. In this case, the state is not changed. If there
are no matching offers or requests left, the message NO_EVENT is sent and
the state is changed to Idle again (8). A requesting inference machine
which receives a matching offer indication, but finds that the corresponding
rule is no longer startable in the current state of the rule system (the rule is
contained In wstate) returns a CANCEL_REQUEST message. Similar actions
as for a negative CONF_REQUEST message are performed (13, 14). Addi-
tionally, the event request is cancelled at the gate.
..... __ CONF_OQ
--...._/ ( A requests)
( :3 offers )
lND-HATCH_OFFE.:J
CONP_REQUEST
.,
(lal.e)
checlLrequestsoO
a local realization, all rule system and gate instances defined in the specifi-
cation are executed in a single address space and communication can be
achieved using shared memory. Basic ideas of such a local realization are
presented in the following. The different components of a local runtime envi-
ronment have been implemented according to these ideas as described in
[Sche89] [Schn87] [Schn89b].
Tree management
For executing CRS specifications which use X-ASN.1 data objects repres-
ented as structure trees and data trees, the runtime environment has to
provide routines for
For each X-ASN.1 type constructor a class is defined which provides index
and selection operations, respectively. Runtime checks are performed when
navigating through structure trees and data trees. The value fields in data
blocks can be changed by corresponding assignment functions. Copying
whole data trees is supported, as well as structural assignment and com-
parison, by recursively applying the operations to subtrees. The tree man-
agement routines are called by the generic machines executing rule
systems and gates.
170 5 Protocol Engineering with Communicating Rule Systems
Generic machines
CRS inference and gate machines can be provided in a generic fashion in
a local runtime environment for CRS specifications by employing the
concept of control blocks'o. The execution state of rule system instances is
represented by rule system control blocks and the execution state of gate
instances is represented by gate control blocks (see [Schn87] [Schn89b]).
The whole architecture of the local runtime environment for the simulated
execution of CRS specifications is depicted in Figure 79.
1. matching.
2. conflict resolution:
3. action:
• starting rules;
• ending rules;
• updating rule system control blocks.
The different functions work according to the rule set model described in the
last section and implement the actions necessary for transferring rules
between sets. Since many of these functions are independent from each
other they can be realized as separate procedures. By combining these
procedures differently inference strategies can be adapted to different
needs. For establishing events functions of the generic gate machines are
used.
'0 The idea of control blocks is similar to the pseudo processors proposed in
[Nehm85] to implement process management in operating systems.
5.1 Executable CRS 171
....- - - - -..
generic generic
inference gate
machine machine
scheduler
Rule system control blocks and gate control blocks are passed between the
generic inference and gate machines by a scheduler In the runtime envi-
ronment. The scheduler is responsible for managing rule system and gate
control blocks after they have been created and for passing them to the
generic machines according to the scheduling strategy used. The sched-
uling strategy should not be fixed for executing specifications, but it should
be possible to adapt it to different needs. These needs may be determined
by an application using the executable specification, or may be derived
statically from the specification.
·..
·..
Wstate
Ready
Wevent
·..
J
l rule J rule I ...
Wsyn
Start ··.... ,
··.......
R wfc
J
rule name
rule Id
rule .)'.tem name
I
rulo oyotom Id _cutabl. cod.
ta check the etart
compatibility Info candltlon
'::diti~~':'!:::~ronou.
..-. ...
prlorlt)' Info on tho ....cutable cod.
otato ta Inotoll the
Coured effeclo
on the
Eol.pred otelo
,.~::t~~~:!.~!~:!nou.)
"'UIelo ...
oQ..JIalo
cOUlelo
oOUlelo '!~d~tl~~':'!;~:~~nau.)
...
CQ"JIYIInt name
IG.-lvent name
executable cade
to chock tho otort
condition
... cutable codl
I
an tho
c..JMInt name
...n! to compulo tho ro~~.:~~r;~~~:'!~OUO)
...
=
1'-lIWInt name
....nt
parameter
Cov--pred ~vaIU"
Eov--prod
Parma - ~dP~
oIQrog.oroo ~
executable code
to compute the
• .t.d parum.
Chec!w>arm. rap aria local
variable
e
SeUvar. YGlue.
bar.
Iocalvariov
.tarafitl artla
m••• age Indication
"ergl
formed using simple logical operations on Run and Syn. If the rule requests
an event in the start condition, or offers an event in the effects, the event
types and references to gate control blocks are stored in the rule control
block.
The Fcond (II. ,) and Fe//ects (II. ,) formulas of a rule are implemented by several
functions and references to these functions are stored in the rule control
block. According to the execution model used by the CRS inference
machine (see Figure 74), the constraints on the rule system state and on
events are separated. Each rule is implemented by five functions:
checks whether the state of the rule system qualifies for a rule
start;
Cev_pred checks whether the offered event parameters meet the con-
straints of an event request;
Set_lvars determines settings of the local variables;
Est_pred performs actions establishing the effects on the state objects;
Eev_pred computes the event parameters to be offered.
The separation of start condition and effects parts into different functions is
possible under the assumption made by the CRS implementation concepts
that event requests and offers in rule start condition and effects parts are
always I\-connected to the constraints on state objects. If no event is
requested or offered, respectively, the corresponding functions are "empty"
and simply return 'true'. The generic inference machine working on rule
system control blocks invokes the functions in rule control blocks to check
start conditions, save local variables, and realize effects during execution of
a rule system. The results of these rule functions and the availability of gate
messages determine whether rules can be transferred between the different
sets.
The structure of gate control blocks is illustrated in Figure 82. The execution
state of a gate comprises the state of the gate protocol and the event
requests and offers available. Requests and offers stored in gate control
blocks (Requests, Offers) are those that have been delivered to the gate
by inference machines, but for which matching counterparts have not been
found yet. Lists are used to represent sets of requests and offers. Some aux-
5.1 Executable CRS 175
Requests ...
Offers ·..
Chacluequ..to
... {:::0111 ~~I ...
ChoclLoIfwn
... ..
Off
Req ·..... ...
lu'r....u.quMIo
8uffwmlpffwn ·.. Requests/Offers Set
Type
Name
State
iliary sets are used for holding event requests to be checked against an
offer and vice versa (CheckJequests, Check_offers), an actual pair consid-
ered for a match (Req, Off), and requests/offers buffered until the gate
machine returns to the idle state (BufferedJequests, Buffered_offers).
The name of the gate and an indication of whether It is of synchronous or
asynchronous type is static information in gate control blocks.
The elements of the request and offer sets are represented by event control
blocks (see Figure 83). In each event control block, an identification of the
event type is required (event name). Requested or offered event parameters
can be retrieved via a reference to the rule making the request or offer,
respectively.
event name
rule control block
rule ...
5.1.3 Compilation
The implementation of a compiler generating code for the local runtime
environment from a given CRS specification (incorporating X-ASN.1) is
described in [Clar89] and [Sch090]. After parsing and analyzing an input
specification, an attributed syntax tree and a global symbol table are built.
The code is generated from this internal representation and comprises type
definitions for the state objects of rule systems and ADTs, local objects, and
event types, as well as five functions for each rule and one function for
each ADT operation. Initialization procedures are generated for creating
control blocks and for storing the initial values of the state objects.
The different steps in the compilation process are Illustrated in Figure 84. A
CRS specification is parsed and analyzed by the CRS compiler front-end
and the internal representation Is built. The X-ASN.1 type definitions used in
the specification are extracted and serve as input to an X-ASN.1 compiler
generating structure tree representations according to the concepts pre-
sented in section 5.1.1. These structure trees are used by the CRS compiler
back-end generating the X-ASN.1 extended "C++" code for the specifica-
tion. The extensions are removed by the X-ASN.1 preprocessor and the code
is translated to plain "c" code by a "C++" preprocessor. The final "C"
5.1 Executable CRS 177
+
.trueture---+- CRS Complier .
tr...
Pr'proe... or '
C loure. cod.
C Complier
obleet fU ••
tree monollem.nt
and
lIenerle moeh!n ..
(runtime Ilbrarle.)
•• eeutabl • • p.clflcallon
sources are compiled and linked with runtime libraries providing the func-
tions described in section 5.1.2 to form an executable specification.
In the following, the principles employed for the compilation of the different
parts in a CRS specification are explained in more detail.
X-ASN.1 preprocessing
In section 5.1.1, the integration of X-ASN.1 into a target implementation lan-
guage and the representation of types and values as structure trees and
data trees has been described. One way to realize this approach is by
employing a preprocessing tool that transforms all occurrences of X-ASN.1
variables and expressions into the target language representation, before
compiling the sources into object code. The tree representation is hidden to
programmers or code generator tools, respectively, using X-ASN.1 as the
178 5 Protocol Engineering with Communicating Rule Systems
II <--------------------->
II "C" access
II <-------->
II sensitive
II selector
// <------------------->
II X-ASN.1 access
// <------>
1/ X-ASN.1
II component
The preprocessor works in two phases, called marking phase and transfor-
mation phase. In the marking phase, the X-ASN.1 types and expressions
are analyzed and type compatibility is checked. Type, variable, and
selector identifiers are stored in a symbol table. In the transformation phase,
all X-ASN.1 related statements are transformed into their "C++" counterparts.
The implementation of the runtime support routines for the tree manage-
ment (see section 5.1.2) is also described in [Sche89]. The class hierarchy is
outlined in Figure 86. The most general class is ASN_ EXPR, fixing the repre-
II ASH EXPR <----- ASH EXPR INT <----- ASN VAR IHT
II - <----- ASN=EXPR=REAL <----- ASN=VAR=REAL
II <----- .,. <----- ...
II
II <----- ASN_EXPR_OTHER <----- ASN_VAR_OTHER
class ASN EXPR {
DT data tree;
DB data-block;
}; -
class ASN EXPR INT : public ASN EXPR {
public: - - -
void operator = (ASN_EXPR& source); II assignments
void operator = (int i);
int operator == (ASN_EXPR& second); II comparison
int operator int(); II conversion
Compilation of gates
The compilation process for gates results in a header file and a source file
for each gate specification. The attributed syntax tree built during the
parsing phase serves as the basis for generating these files. As an example,
the header file and source file for the gate Network_service_access_point
(see Figure 54 in chapter 3) as generated by the CRS compiler are outlined
in Figure 87 and Figure 88.
The header file contains type definitions for each event type defined for the
gate (see part I I in Figure 87). The X-ASN.1 type modules which are
required for defining these types are included by corresponding X-ASN.1
preprocessor directives (I). All identifiers generated by the compiler (type
identifiers in this example) are constructed based on the identifiers used in
the specification text. Besides the type definitions, the interface description
of a 'copy'-function is generated for each event type defined in a gate
specification (I I 1). The 'copy'-functions for event types are called by the
generic runtime routines in order to copy event parameter values between
memory areas when requesting and offering events at runtime. The structure
of these memory areas does not have to be known by the generic
machines and the implementation of the 'copy'-functions for event types
can be hidden in the gate source file. Another function declaration is con-
tained in the gate header file for the 'create'-function, serving for the cre-
ation of gate instances (IV). The 'create'-function is called whenever a new
instance of a gate specification has to be allocated and initialized. The
implementation of this function is given in the gate source file.
5.1 Executable CRS 181
At the beginning of the gate source file, the gate header file is included to
make all the type definitions available (see part I in Figure 88). Then, the
code generated for the event parameter 'copy'-functions follows (I I). The
N_CONNECTJeq_ev_coPY-function is shown as an example in Figure 88. Two
generic pointers (from, to) are given as parameters. These pointers refer to
objects whose sizes and structure are unknown outside the function. Within
the function, the addresses passed in the parameters are assigned to local
pointers (pev, from_casted) of appropriate types (N_CONNECTJeq_ev).
//-------------------------------------------------------------------------11 --
//-- III --------------------------- external declarations for COPY-functions --
extern int N_CONNECT_req_ev_copy (Gen_pointer from, Gen_pointer *to);
//----------------------------------------------------------------------- III --
//-- IV ---------------------------- external declaration for CREATE-function --
extern PSynGateset CR_Network_service_access_point (char *name);
//------------------------------------------------------------------------ IV --
Figure 87. Example gate header file
182 5 Protocol Engineering with Communicating Rule Systems
if (pev != NULL) {
new_Isn_vlr pev->asn_n_connect_req;
if (from!= NULL) {
from casted = (N CONNECT req ev *) from;
*pev:>asn_n_connect_req : *from_casted->asn_n_connect_req;
} /* end if */
*to = (Gen pointer) pev;
return (6);
else {
return (1);
//------------------------------------------------------------------------ II
return(p);
}
//----------------------------------------------------------------------- III --
The code generation starts from the symbol table and an aHributed syntax
tree corresponding to a specification which is expanded, resolved, and nor·
mallzed. This means, auxiliary predicates, contexts, and views are
removed in a number of passes (see [MiII90]), resulting in a flat rule system
(see chapter 3). Additionally, all formulas used in the specification are trans-
formed into prenex-disjunctive normal form by employing a corre-
sponding algorithm (see for example [Mann74J).
The types defined in the header file are included in the source file gener-
ated from a rule system specification (see Figure 90, part I). other header
files are included for all gates used by the rule system. Similar to the event
parameter 'copy'-functions given in the source file for gates, 'copy'-
functions for the state objects and local objects of a rule system are gener-
ated (I I). As explained in section 5.1.2, five functions are generated for
each rule in the rule system specification, serving to check start conditions
and to realize effects (I I I). How these functions are obtained is described
later. An example is given in Figure 93 for the rule n_conJeq (see
Figure 50).
} X 25 DTE decl;
typedef X 25 OTE decl *PX 25 DTE decl;
//-------=--=---=--------=--=---=---------------------------------------- III
After the rule system control block has been allocated and initialized, rule
control blocks are allocated for each rule (function NEW_RULE provided by
the runtime environment). The rule-specific data is passed in a number of
parameters. Then, the new rule control block is inserted into the Wstate set
of the rule system control block.
5.1 Executable CRS 185
11------------------------------------------------------------------------ IV --
Figure 90. Example rule system source file
186 5 Protocol Engineering with Communicating Rule Systems
Compilation of rules
Most of the complexity encountered for the compilation of CRS specifica-
tions is due to the first order predicate logic (FOPl) used for specifying the
start conditions and the effects of rules. According to the implementation
concepts for the CRS inference machine explained in section 5.1.1, code
has to be generated to evaluate the start condition with respect to state and
event constraints, to determine appropriate values for local objects, to
perform actions on the state, and to offer events for each rule. Appropriate
restrictions on the form of predicates used in rule specifications had to be
found in order to make an automatic translation feasible.
As already mentioned above, the start condition and effects formulas of rule
specifications (F cond (I>. r) and F_cis (I>. r)' see section 3.3) are transformed into
prenex-disjunctive normal form (DNF), before the code generation phase
starts. Quantors are not supported. In general, the formulas are then of the
form
and represents one alternative for satisfying the whole formula. For a Cj to
be satisfied each lj (j=1 .. m) must be satisfied. The lj are called literals and
are of the form
A or -,A.
where t1••••• tk are terms. Terms may be just variables. or some function con-
stant (for example. +. I. etc.) applied to terms. The symbol p represents a
predicate constant (for example. ~. >. etc.).
5.1 Executable CRS 187
The DNF form of formulas is more suitable than a conjunctive normal form
because the implementation concepts presented in section 5.1.1 are based
on the assumption that event requests and offers are always f\-connected
to the rest of the predicate and that state and event requirements are
checked separately. Code can be generated from the DNF for each alter-
native C I ..... Cn• where an interaction expression. if present. has to be part of
every alternative and is always f\-connected to state requirements and con-
straints on event parameters. Most preferably. start conditions and effects
formulas consist of just one alternative CI and several alternatives are
expressed using several rules. instead of v-connected sub-formulas.
Ie assigns
• elements of D to individual constants.
Iv assigns
• elements of D to individual variables.
• state variables.
• auxiliary variables.
The state variables are declared in the STATE-part of a rule system specifi-
cation. Both local variables and auxiliary variables are declared in the
DECLARATIONS-part of a rule system specification. They are called "declara-
tion variables" in the following. Local variables are those declaration vari-
ables that are used both in the Feond (ro. r) and Feileen (1$. r) formula. Auxiliary
variables are either used in Feond (l$.r) or Fe/Jeen(I$,r). but not in both formulas.
The code generated for the five functions implementing a rule serves to
check models of Feond (l$.r) and Felleen (l$.r). respectively. Depending on the par-
ticular function. possible models are partly defined by the state of the rule
system. the offered event parameters. or the values of local variables of
running rules. The missing parts ofa model have to be determined by a
static analysis of the formula. Appropriate values obtained from such an
analysis are propagated into local variables. the new state of the rule
system. or event parameters being offered. The approach taken In [Sch090]
to realize the generation of code for checking (respectively constructing)
models of rule specifications is further detailed in the rest of this section.
Starting from Feond (II. r) and Feileen (1$. r) given in DNF. variable occurrences in
literals (~) are separated into defined occurrences and used occurrences.
In defined occurrences. possible values of a variable are restricted by a
predicate. For example.
x < 5
is a literal. where the value of the variable x is restricted to the set {4. 3. 2•
... } by the < predicate. In general. several defined occurrences of the same
variable may be given in a formula. For example. in the formula
x<5 1\ x>3
In a formula like
x< 5 A X > 3 A Y = x
Classifying the variable occurrences in a formula this way does not neces-
sarily deliver a unique result. For example, in the formula
x<5 A x>3 A Y=X A y=4
In the literal
x + 1 = 2
Before the code is generated, the Fcond (It. r) and Feffects (IS, r) formulas of a rule
specification are analyzed to find the variable dependencies. During several
passes over the attributed syntax tree of a formula, a dependency graph
is built for each conjunction.
This is illustrated I:;>y the dependency graph of the rule n_con_req shown in
Figure 91 (see the specification given in Figure 50). In the general case (a
190 5 Protocol Engineering with Communicating Rule Systems
rule with several v-connected conjunctions), the dependency graphs for all
conjunctions are connected to form the graph for the whole formula in DNF
(see Figure 92). After analyzing the variable dependencies, the code for
the five different functions implementing a rule is generated based on the
dependency graph. If variables remain without a defined occurrence in
neither Fcond (fl. ,) nor Fel/ecfs (fl. ,), no code generation is possible for this rule.
Defined occurrences that are found result in assignment statements,
whereas the used occurrences result in expressions corresponding to the
predicate in the literal.
As an example, the code generated for the functions of the rule n_conJeq
are given in Figure 93. All functions have two parameters holding pointers
to the rule control block (r) and the rule system control block (pm) of the
rule. Within the functions, the addresses passed via parameters are
assigned to local pointers, referring to individually structured objects in
memory. In the n_conJeq_CST-function, the requirements on the actual
5.1 Executable CRS 191
graph ~~=::j_~
nert
return(I}:
Compilation of ADTs
The compilation of ADT specifications works similar to rule systems. In
general, the task is simpler due to the following reasons:
• ADT objects, unlike rule system instances, are passive objects and their
operations are invoked from outside the ADT;
• ADT operations are specified by a precondition (PRE) and effects
(EFFECTS), but, unlike rules, their execution is atomic;
• ADT objects are defined using a number of state objects, but, unlike rule
systems, there are no local objects used by rules.
The code generation for ADT specifications also starts from the attributed
syntax tree, where all formulas used in operation specifications have been
expanded and normalized to DNF. In the header file generated from the
ADT specification, a type is defined for the state objects of the ADT. An
example is given in Figure 94 for the ADT DataQueue specified in chapter 3
(see Figure 62). The X-ASN.1 type definitions required for the state objects
are included by a corresponding preprocessor directive (part I in
Figure 94). Then, a type definition summarizing the state objects is gener-
ated (I I). The ADT 'copy'-function and procedures for all ADT operations are
exported to other modules by external function declarations contained in
the ADT header file (I I 1. IV). Finally, an external declaration for the 'create'-
function of the ADT is given (V). The implementation of these functions is
contained in the source file for the ADT.
In the source file generated from an ADT specification, the header file is
included (see part I of the example given in Figure 95). Then, the imple-
mentation of the ADT 'copy'-function follows (I I), which works in a similar
way to gates and rule systems. Every operation defined in the ADT specifi-
cation is translated into a single procedure checking the precondition and
194 5 Protocol Engineering with Communicating Rule Systems
11------------------------------------------------------------------------ IV --
11-- V ----------------------------- external declaration for CREATE-function --
extern PDataQueue state CR DataQueue ();
11---------------:--------:------------------------------------------------ V --
Figure 94. Example ADT header file
//----------------------------------------------------------------------- III --
return{state_area);
}
//------------------------------------------------------------------------ IV --
Figure 95. Example ADT source file
//------------------------------------------------------------------------ II --
//-- III --------------------------------------- create rule system instances --
network_entitYl = CR_X_25_DTE ("Network_entityl". nsapl. packetsl. I);
INS_RS (&SCHEDQUEUE. network_entityl);
//----------------------------------------------------------------------- III --
returnee);
and Inserted Into the scheduling queue for rule systems (SCHEDQUEUE)
managed by the scheduler (I I I). All parameter values that are required to
create the instances are given in the specification. The procedure
1n1t1alize_system is called by the runtime environment before the
dynamic execution of the specification is started.
Apart from the design and realization of each single tool, the integration of
these tools for all development activities into a common environment is nec-
essary in order to support the whole development process. As illustrated in
chapter 4, many existing protocol development tools focus on a single
activity and are only loosely coupled with tools for other activities in existing
environments. Very often the capabilities of an FDT simulator are used to
accomplish additional tasks besides design validation, for example, trace
analysis, test generation etc. However, since these additional tasks were
not included in the design of the simulators, flexibility Is sometimes severely
limited in such tools.
5.2.1 Architecture
The tools identified in chapter 1 (see section 1.3) can be divided Into two
classes:
Another important integration aspect is the following: tools used in all the
phases of communication system development require and produce know-
ledge about the services or protocols they are working on. This knowledge
may be represented differently, together with corresponding storage,
retrieval, and inference facilities. State tables, attributed syntax trees,
reachability graphs, behavior expressions, predicates, and rules are just a
few examples. Therefore, the second basic idea of the integrated environ-
ment architecture is that protocol knowledge is shared by different tools
(knowledge Integration).
and testing, depending on the degree of abstraction required and the strat-
egies and heuristics used. Such an integrated environment has considerable
advantages:
5.2.2 Kernel
In the kernel, information about the communication system under develop-
ment has to be represented and processed. The information about services
and protocols is given by formal descriptions in textual or graphical form.
This external format has to be translated into an internal format by a set
of system tools. The goal is to represent the protocol knowledge in an ade-
quate way and to provide mechanisms for knowledge management and
retrieval.
TRee
mRnRc;anenT
GATE
mACHinES
Data aspects
A large number of concepts have been developed for representing data In
systems. Despite many differences, all concepts Introduce a clear sepa-
ration between data structures (or data schemes) and data items (Instances
of a certain structure). A data management component has to provide
structuring mechanisms, as well as storage and retrieval mechanisms for
data items [Kort86].
Data schemes for SPs and PDU formats can be created by using the X-ASN.1
type definition constructs explained in chapter 3. The X-ASN.1 complier
described in section 5.1 checks syntax and static semantics, resolves
external references, and converts the type definitions into the internal struc-
ture tree representation used by the X-ASN.1 data management component.
202 5 Protocol Engineering with Communicating Rule Systems
For each type module the global symbol and index tables are built, serving
for the retrieval of type information from structure trees.
Behavioral aspects
A communication service is defined by a set of SPs exchanged between a
service provider and a service user, possible sequences of SPs, and param-
eter dependencies. This view focuses on the externally visible behavior of a
communication system and abstracts from the internal behavior. How a
service is provided by a number of distributed entities is described in a pro-
tocol specification. The protocol determines the behavior of each entity: the
set of possible input events in each state, the actions to be executed in
response to various inputs, and the corresponding output events.
5.2 CRS Integrated Tools Environment 203
Using CRS, the relation between input events and output events, possible
event sequences, and possible event parameter ranges are described by
rules defining the behavior of rule systems. An internal state concept is used
to facilitate the description of sequencing aspects. Several rule systems can
be composed in parallel and cooperate to provide a service. The behavioral
information contained in CRS specifications can be represented in form of
production rules in the kernel, as explained in section 5.1. Besides formal
logic, procedures, and frames, production rules are a basic technique for
representing knowledge in systems [Barr81] [Fros86]. In the production
systems obtained with the CRS compiler described in section 5.1, a mixed
form of representing knowledge about behavioral aspects is used. Whereas
production rules capture the input/output relations and spontaneous
actions, rule body procedures represent the knowledge about internal state
conditions and event parameter constraints.
5.2.3 Shells
Experiments with the first prototype Implementations of the X-ASN.1 and CRS
system tools (see [Schn87] [Schn89a]) clearly showed that providing flexible
access to the environment kernel via appropriate interfaces is of utmost
importance for building application tools. The Implementation of an appli-
cation program interface provided in a function library interfacing with
kernel routines was a major step towards a comprehensive integrated tools
environment. This application program interface constitutes the rule-based
shell and is described in more detail in the following.
However, the rule-based shell is not adequate for application tools working
on higber levels of abstraction, for example, for tools working on externally
observable behavior sequences or global states. Therefore, two additional
shells providing complete transparency of the techniques used in the kernel
are described in this section: the state-based shell and the event-based
shell. By combining functions from different shells, application tools can use
different views of the specified system in an Interleaved fashion. The shells
act as bridges between different models and allow advantage to be taken
of one model while avoiding the disadvantages of others.
Rule-based shell
Figure 99 illustrates the application program interface constituting the rule-
based shell of the X-ASN.1 and CRS based kernel. The functions provided
are tailored towards the techniques and work directly on the internal repres-
entations of data objects, rule systems, gates, and rules [Schn89b]. The set
of functions provided by the rule-based shell can be divided Into the fol-
lowing groups:
• Logging functions, which control the data logged during system exe-
cution. These functions may be called at any time to increase the
amount and granularity of information that is written to disk for a subse-
quent analysis, or to decrease the level of detail to speed up execution
when no interesting events are expected. The scheduling of rule systems
and gates, the selection of rules to be started or ended, the events to
request and offer, the transitions of rules between sets, state changes,
and other kinds of information may be logged while working with the
system.
5.2 CRS Integrated Tools Environment 205
• Gate functions, which return information about the state of gates and the
available event requests and offers. There are also functions provided in
this group which can be used to add or remove event requests and
offers at external gates.
GRTE
mACHines
. . ffi:r
For most of the functions of the rule-based shell, some mechanism for iden-
tifying specification objects has to be used. The names of rule systems,
rules, and gates suffice to interact with application tools, but more efficient
approaches can be taken as well. Also, structure trees, data trees, and con-
straint trees can be exchanged via the application program interface. The
rule-based shell is appropriate for application tools working directly on rules
and other objects that are specific to CRS and X-ASN.1. Therefore, important
data structures managed in the rule-based shell are:
State-based shell
The functions of the rule-based shell are mainly used for retrieving informa-
tion about rule systems and rules defined in the specification and for
invoking state transitions by starting and ending rules. No means are pro-
vided to work on global states of the system, or to step back and take
some alternative execution path after having executed a number of rules.
This kind of support is provided by functions of the state-based shell (see
Figure 100).
Since CRS is based on the EFSM model an explicit notion (and represen-
tation) of states is given by the values of state objects, the execution states
of rules and local objects, and the event offers available at gates. The
internal representation consists of data trees and control blocks. For man-
5.2 CRS Integrated Tools Environment 207
• The function save_state, which creates a copy of the current state of the
system on the system stack. Copies of the control blocks for rule
systems, rules, gates, event requests, and event offers are required, as
well as copies of data trees representing state objects and local objects.
208 5 Protocol Engineering with Communicating Rule Systems
other functions required in the state-based shell are mainly state manage-
ment functions, serving for searching, moving, copying single states etc.
Complete search and backtracking strategies have to be realized by appli-
cation tools according to individual needs. State management and organ-
ization is, however, taken over by the state-based shell. In turn for the extra
effort of implementing backtracking algorithms, application tools can flex-
ibly adjust backtracking strategies to their needs. Experience with
"PROLOG", for example, shows that a predefined fixed backtracking
strategy becomes inappropriate with growing search spaces.
Event-based shell
A lot of application tools work only on the basis of the externally visible
events of a system and do not use any details of the internal model of a
service or protocol specification. Such application tools should access the
kernel mechanisms via an event-based shell. For the X-ASN.1 and CRS
based kernel such an event-based shell has been implemented on top of
the rule-based and state-based shells as described in [Roor90] (see
Figure 101). The functions provided by the event-based shell are the fol-
lowing:
" Note that this is an equivalence on states which is rather strong with respect to
externally visible behavior.
5.2 CRS Integrated Tools Environment 209
• The function stimUli, which lists all events that can be accepted by the
system in a given state at the external gates. Gates serving for internal
communication between system parts are not considered.
• The function select, which marks one of the possible stimuli as being
selected for subsequent behavior. This function is called for making a
choice, but it does not yet invoke any actions.
210 5 Protocol Engineering with Communicating Rule Systems
• The function answers, which returns all possible responses after some
specific selection. The list of events returned as the result of the function
contains all events that can be offered by the specified system in the
state reached after the selected event has been accepted.
In order to find out which events can be accepted (offered) by the specified
system, rules have to be started (ended) and states have to be saved and
resumed (using functions of the rule-based and state-based shells). The
stimuli-function, for example, searches for startable rules that request events
at external gates in their start condition. The answers- function has to start
each rule requesting the selected event separately from the current state.
Then, one of the three following cases applies: (1) the started rule offers an
event at an external gate, (2) the started rule offers an event at an internal
gate, (3) the started rule offers no event in its effects. In case (1), a possible
answer has been found. In case (2), matching event requests from startable
rules in other rule systems have to be found, these rules have to be started,
and the procedure is applied recursively to all states reached. In case (3),
all startable rules without event request in the same rule system have to be
started and the procedure has to be repeated for every state reached.
However, all this internal processing is hidden from the application tools
using the event-based shell.
1. Event info contains the list of external gates in order to be able to distin-
guish between requests/offers made at internal and external gates. Sim-
5.2 CRS Integrated Tools Environment 211
Function keys allow zooming into selected rule system and gate instances
in order to get more detailed information about rules, or event requests and
offers. The logging flags can be set appropriately to trace the simulated
behavior. Using the menu bar, scheduling and inference machine strategies
can be adapted. The execution mode can be set to follow predefined strat-
egies individually for each rule system and gate instance at the conven-
ience of the user. For each X-ASN.1 defined object the X-ASN.1 data tree
5.2 CRS Integrated Tools Environment 213
, ,
OJI"lFIUURRTlOn 5CREEfl
I I
Rule System Scheduler 1 Inference Machine Searched Set Actual Rule 100lo I
t Jc=.=:.J
......... '-
Evert' Hdlory • 1'"'-' -' 1 c:=J
EJ 0
UDUD U
. .................
• • e ____ " _ . _ . _ • • • •
................... ..
•
TRACING 1T----siJ 1M SS AR ~
('f1-trocV ([2-8 C CY (TJoz...-S> ~ (f5' GoV
After scheduling a rule system, the startable or endable rules in the current
state of the rule system are listed in a menu. By making selections from this
menu, rules can be started and ended, which brings the whole system into
a new state. The backtracking features of the state-based she" can be used
to resume the simulation from previously saved states. The events occurring
during the simulation are displayed and stored in an event stack. The user
may also add event requests and otters at external gates for triggering
actions in the executable specification.
With the control facilities described above, a protocol engineer can easily
influence the execution of the specification and drive it to areas of interest.
More or less detailed traces may be produced and analyzed by other tools
after the simulation. The experiences made with a prototype of the CRS sim-
ulator showed that such a tool is a powerful instrument to validate a design
for the most interesting situations and that it is also useful for teaching ser-
vices and protocols to newcomers. However, the execution mechanisms pro-
vided may also be used to set up long-term automatic simulations. Several
strategies may be employed (full reachability, modified reachability,
random state exploration etc.).
never be exhaustive. The production of test cases and their aggregation into
a complete test suite covering as many protocol aspects as possible, as
well as the related questions about test purpose, test selection, test quality,
test coverage, and test execution are major research topics in protocol
engineering today. Considering the variety and complexity of today's and
future protocols, tool support for test case development becomes Increas-
ingly important since such tools speed up the production of tests and help
to improve test suite quality.
For all these reasons, a test case development tool (instead of an automatic
test case generation tool) operating in an interactive fashion with a test
case designer in the integrated tools environment is considered to serve
existing needs. A first prototype of such a tool has been implemented
according to the configuration shown in Figure 103 (see also [Velt89]). Test
case design is conducted on the basis of an executable reference specifi-
cation of the protocol, excluding the possibility of errors and providing all
216 5 Protocol Engineering with Communicating Rule Systems
I----~
I TEST LOGIC: \
I • algorithms \
I • heuristics \
I • strategies
.1--------- \
TTCN
Editor (TTCN-GR)
necessary Information about the protocol to be tested. The user of the tool
retrieves protocol information from the kernel using functions of the event-
based shell.
With the zoom-function, he can focus on a number of test events that are
interesting for achieving a specific test purpose. Then, the stimuli-function
can be used to list the test initiatives together with their parameter con-
straints. One event can be selected with the select-function and a combina-
tion of parameters can be supplied. By calling the answers-function, the
5.2 CRS Integrated Tools Environment 217
The output of the test case development tool is displayed in standard TTCN
format (see section 4.2.3) using the HCN editor described in [8aer89]. A test
case in TTCN consists of a tree of test events (see [1509646]). The events in
each path of the tree starting from the root and ending in some leaf node
occur in sequential order; events at sibling nodes represent test alternatives.
Each test event is of the form
A peo denotes the Point of Control and Observation where the event
occurs. The Event _ i d is usually associated with an SP or PDU exchange
and the exclamation mark (question mark) means sending (receiving) the
event. Values may be assigned to test variables when the event occurs. A
condition in the form of a boolean expression can be associated with each
event (only if this condition is satisfied may the event occur). All declara-
tions of PCOs, events, test variables etc., and the test case behavior tree are
contained in tables of fixed formats. All information required for creating
these tables can be retrieved from the protocol specification represented in
the environment kernel.
218 5 Protocol Engineering with Communicating Rule Systems
1. protocol Independence,
The review process for test suites includes checking the HCN syntax and
static semantics, as well as validating the correctness of the test suite with
respect to the protocol standard the test suite has been developed for.
Checking the syntax and static semantics of HCN can be automated by
employing parser tools accepting the HCN language (see for example
[8aer89]). Checking automatically whether a test case assigns 'pass' ver-
dicts only if allowed behavior has been observed, 'fail' verdicts only if an
error has been found, and vice versa, is a more complicated and yet
unsolved problem for manually developed tests.
software tools. In the integrated tools environment. all information about the
protocol for which a test suite should be validated can be represented in
the kernel. based on a specification of the protocol in X-ASN.1 and CRS. The
TTCN test description is parsed. loaded into the TTCN editor. and checked
against the executable protocol specification by Interpreting the TTCN con-
structs (see Figure 104). The approach is rather pragmatic as long as a
formal TTCN semantics is stili missing. but may be justified by relating TTCN
to the FDTs employed for protocol specification (see for example [Sari88]).
or to more basic models (for example. labelled transition systems).
'TEST \
" ASSESSMENT: \
\
, • correctne.. \
, • quality \
l - - - -t- - - - -
TTCN
Executor
While running the test suite validation tool, statistics can be maintained to
gather information about which part of the protocol (service aspects, pro-
tocol aspects, state transitions, parameter combinations etc.) are tested thor-
oughly, and which parts are probably not tested at all. These statistics may
be evaluated afterwards to allow qualitative and quantitative statements
about test coverage (depending on whatever definition of coverage is
used).
222 5 Protocol Engineering with Communicating Rule Systems
6 Conclusions
The main benefits gained from applying FDTs in the protocol development
process are preciseness and the ability to employ tools. The formal syntax
and semantics of FDTs improves the understanding of the basic architec-
tural concepts of communication systems and facilitates the provision of
tool support. However, applying FDTs to the development of systems is not
trivial. The formalization step is difficult and appropriate techniques have to
be used in order to achieve a suitable formal description in reasonable
time. Only if the technique correctly represents the basic architectural con-
cepts of communication systems and offers constructs supporting intuitive
and structured protocol specifications, it can be useful in practice. The feasi-
224 6 Conclusions
bility of building tools that process the formal descriptions is crucial since
tool support is the key motivation for the formal approach.
The rule-based formal description technique CRS has been adopted to serve
the existing needs. Employing the rule paradigm aimed at providing appro-
priate means to achieve intuitive and intelligible formal protocol specifica-
tions in relatively short time. Concerning the development of tools, it could
be demonstrated that rules are a general and flexible mechanism for
representing the specification knowledge and that they can be used by
tools supporting various protocol engineering activities.
About half a year was required by two students to develop the complete
X.25 packet level protocol specification, including X-ASN.1 type definitions
for all X.25 packets and rules for call setup, connection handling, data
transfer, fragmenting/reassembling and retransmission of packets, call
clearing, and the restart procedures. The final specification achieved was
discussed with X.25 experts. It turned out that the rules describing the pro-
tocol could easily be understood and that the specification reflected the
standard very well. An interesting experience during the discussions was
that the experts could sometimes give no answers to the questions arising
out of those parts of the specification that were most difficult to develop.
Most of the times this was because the standard is not precise or contains
no information at all. In fact, the corresponding protocol functions often
226 6 Conclusions
The local runtime environment for CRS specifications has been implemented
completely, including the generic interpreters for CRS rule systems and
gates, the scheduler, and the X-ASN.1 structure and data tree management.
First prototypes of the CRS compiler and of the X-ASN.1 preprocessor gener-
ating the specification-specific code for the runtime environment have been
completed as well. Most of the specification examples mentioned above
have been compiled into executable form. The transport service specifica-
tion and a subset of the X.25 packet level protocol specification are opera-
tional. The restrictions imposed on the form of predicate logic formulas were
found acceptable for the trial specifications, although some parts of the ori-
ginal specifications had to be adapted in order to allow the transformation
into executable form. The modifications made are a matter of style,
however, and do not change the behavior of the protocols.
Some of the event sequences prescribed by the X.25 packet level test suite
have already been checked using the test case validation tool. So far, it has
been detected that admissible alternative behavior is missing in some of
the test cases. Support for checking· data constraints also has to be added
in the test case validation tool and some work remains to be done con-
cerning the mapping of HCN types to ASN.1. The experiences made so far
show that the interworking of the tools in the integrated environment poses
no difficulties; rather large parts of the system tools and of the kernel repre-
sentation can be shared.
Many new applications are possible given the transmission rates of optical
fibers and the installation of high-speed networks (FOOl, B-ISON etc.). These
networks will also require new protocols and will emphasize the importance
of non-functional protocol aspects. New language constructs, corresponding
semantics, and formal methods for specifying, simulating, and predicting
the performance of communication systems have to be Included into FOTs.
The formal models can be used to identify bottlenecks, to validate perform-
ance measures, and to come up with better Implementations. Extensions to
FDTs have to be developed for specifying timing aspects. This does also
apply to CRS.
References
[Acet87] L. Aceto, R. DeNicola, A. Fantechl Testing Equivalences for Event
Structures Mathematical Models for the Semantics of Parallelism, M.
Venturini Zilli (editor), Lecture Notes in Computer Science 280, Springer
1987, pp. 1-20
[Atle90J M. Atlevl SDT - a Real-time CASE Tool for the CCITT Specification Lan-
guage SDL Proc. 2nd Int. Cont. on Formal Description Techniques for Com-
munication Protocols and Distributed Systems, S. Vuong (editor),
North-Holland 1990, pp. 37-41
[Baer89J U. Bar Werkzeuge zur Entwicklung und Ausfuhrung von OSI Conform·
ance Tests fUr TTCN Masters Thesis, University of Kaiserslautem (Germany),
1989 (in German)
[Boot90] R. Booth An Evaluation of the LCF Theorem Prover using LOTOS Proc.
2nd Int. Conf. on Formal Description Techniques for Communication Proto-
cols and Distributed Systems, S. Vuong (editor), North-Holland 1990, pp.
83-99
[Brln88b] E. Brlnksma A Theory for the Derivation of Tests Proc. 8th Int. Symp. on
Protocol Specification, Testing and Verification, S. Aggarwal, K. Sabnani
(editors), North-Holland 1988, pp. 63-74
[Burg90] S.P. v.d. Burgt, J. Kroon, E. Kwast, H.J. Wilts The RNL Conformance Kit
Proc. 2nd Int. Workshop on Protocol Test Systems, W. Effelsberg, L. Mackert,
J. de Mear (editors), North-Holland 1990, pp. 279-294
[Chan90] R.I. Chan, B.R. Smith, G. Neufeld, S.T. Chanson, W.B. Davis, S.T. Vuong,
H.L See, S. Chan A Software Environment for OSI Protocol Testing
Systems Proc. 9th Int. Symp. on Protocol Specification, Testing and Verifica-
tion, E. Brinksma, G. Scollo, C.A. Vissers (editors), North-Holland 1990
[Chap89] D. Chappell Abstract Syntax Notation One (ASN.1) Joumal of Data and
Computer Communications, Vol. 1, No.4, 1989, pp. 36-46
[Cour87] J.P. Courtiat How Could Estelle Become a Beffer FDT? Proc. 7th Int.
Symp. on Protocol Specification, Testing and Verification, H. Rudin, C.H. West
(editors), North-Holland 1987, pp. 43-60
[Dhas86] C.R. Dhas, V.K. Konangl X.25: an Interface to Public Packet Networks
IEEE Communications, September 1986, pp. 18-25
[Dlaz86] M. Diaz Petri Net Based Models in the Specification and Verification
of Protocols Petri Nets: Central Models and Their Properties, W.Brauer, W.
Reisig, W. Rozenberg (editors), Lecture Noles in Compufer Science 254,
Springer 1987, pp. 135-170
[Dwye90] D.J. Dwyer Progress in Conformance Testing Services? Proc. 2nd In!.
Workshop on Protocol Tesl Systems, W. Effelsberg, L. Mackert, J. de Meer
(editors), North-Holland 1990, pp. 17-27
234
[EIJk88] P. v. EIJk Software Tools for the Specification Language LOTOS Doc-
toral Dissertation, University ot Twente (The Netherlands), 1988
[EIJk89a] P.H.J. van EIJk, C.A. Vissers, M. Dlaz The Formal Description Tech-
nique LOTOS North-Hoiland 1989
[EIJk89b] P.H.J. v. EIJk The Design of a Simulator Tool The Formal Description
Technique lOTOS, P.H.J. v. Eljk, C.A. Vlssers, M. Diaz (editors), North-Hoiland
1989, pp. 351-390
[Eljk90a] P. v. EIJk Tools for LOTOS Specification Style Transformation Proc. 2nd
Int. Cont. on Formal DeSCription Techniques tor CommunlcaHon Protocols
and DIstributed Systems, S. Vuong (editor), North-Hoiland 1990, pp. 43-51
[Favr87] J.·P. Favreau, R.J. Linn Automatic Generation of Test Scenario Skele-
tons from Protocol Specifications written In ESTELLE Proc. 6th Int. Symp.
on Protocol Specification, Testing and VerificaHon, B. Sarikaya, G. v.
Boehmann (editors), North-HOiland 1987, pp. 191-202
[Feld87] F. Feldbrugge, K. Jensen Petri Net Tool Overview Petri Nets: Central
Models and Their Properties, W.Brauer, W. Reisig, W. Rozenberg (editors),
lecture Notes in Computer Science 254, Springer 1987, pp. 20-61
[Gora90] W. Gora ASN.1 Stand und Trends DATACOM, No.2, 1990, pp. 114-122
(in German)
[Haye90] I.J. Hayes. M. Mowbray. G.A. Rose Signalling System No. 7 - The
Network Layer Proc. 9th Int. Symp. on Protocol Specification, Testing and
Verification, E. Brinksma, G. Scollo, c.A. Vissers (editors), North-Holland 1990
[Jens87J K. Jensen Coloured Petri Nets Petri Nets: Central Models and Their Prop-
erties, W.Brauer, W. Reisig, W. Rozenberg (editors), Lecture Notes in Com-
puter Science 254, Springer 1987, pp. 248-299
[Unn90] R.J. Unn Conformance Testing for OSI Protocols Computer Networks
and ISDN Systems, Vol.18, No.3, 1990, pp. 203-219
[Roor90] S.B. Roorda CRS Supported Development of TTCN Test Cases Masters
Thesis. University of Twente (The Netherlands). 1990
[Sabn87] K.K. Sabnanl, A.M. Lapone PAV - Protocol Analyzer and Verifier Proc.
6th Int. Symp. on Protocol Specification. Testing and Verification. B. Sarikaya.
G. v. Bochmann (editors). North-Holland 1987. pp. 29-34
[Sche90] U. Scheere ASN.1 Definition of X.25 Packets and X.25 Encoding Rules
Internal Report. IBM European Networking Center Heidelberg. 1990
References 241
[Sldha9] D. Sidhu, T.-K. Leung Formal Methods for Protocol Testing: a Detailed
Study IEEE Transactions on Software Engineering, Vol. 15, No.4, April 1989,
pp.413-426
[StoI90] W. Stoll KATE - a Test System for 051 Protocols Proc. 2nd Int. Workshop
on Protocol Test Systems, W. Effelsberg, L. Mackert, J. de Meer (editors),
North-Holland 1990, pp. 215-229
[Tre190J J. Trelmans Test Case Derivation from LOTOS Specifications Proc. 2nd
In!. Conf. on Formal Description Techniques for Communication Protocols
and Distributed Systems, S. Vuong (editor), North-Holland 1990 pp. 345-359
[Turn87J K.J. Turner An Architectural Semantics for LOTOS Proc. 7th In!. Symp.
on Protocol Specification, Testing and Verification, H. Rudin, C.H. West
(editors), North-Holland 1987, pp. 15-28
[Vuon87] S.T. Vuong, D.O. Hui, D.O. Cowan VALIRA - a Tool for Protocol Vali-
dation via Reachabilify Analysis Proc. 6th Int. Symp. on Protocol Specifi-
244
[Vuon88] S.T. Vuong, A.C. Lau, R.I. Chan Semiautomatic Implementation ot Pro-
tocols Using an Estel/e-C Compiler IEEE Transactions on Software Engi-
neering, Vol. 14, No.3, March 1988, pp. 384-393
[West87] C.H. West Protocol Validation by Random State Exploration Proc. 6th
Int. Symp. on Protocol Specification, Testing and Verification, B. Sarikaya, G.
v. Bochmann (editors), North-Holland 1987, pp. 233-242
[Whee85] G.R. Wheeler Numerical Petri Nets - A detinition Telecom Australia, Res.
Labs. Rep. 7780, May 1985
Index
A communication protocol 1
abstract data type specification 101 communication service 1
abstract data type (ADT) 69, 101 communication system 1, 5
abstract syntax 67 compatibility 115
abstract syntax notation one (ASN.1) 4, compositionality 30, 88, 101, 104
65,66 concrete data type 69
abstract test method 145 configurafton compilation 195
abstracfton 30,96,104 conformance testing 142,214
ACT ONE 49, 53 connecfton 10, 14
active object 90 constraint tree 203
ADT compilation 193 constructed encoding 84
application tool 197,198,211 construcftve techniques 58
architectural concept 11 consfructivity 31, 105
architectural semantics 31 context 96
ASN.1 65,66 context resolution 98
ASN.1 complier 152 contexts 97
assignment funcfton 114 control abstraction 92
asynchronous communication 95 CRS 65
asynchronous gate machine 168 CRS compilation 1 76
asynchronous gates 95 CRS complier 203
auxiliary predicate 96 CRS gate machine 164
auxiliary predicate definition 96 CRS inference machine 159
auxiliary predicate expansion 97 CRS interpreter 226
CRS runftme environment 168, 203
B CRS simulator 212
backward-chaining 150
base type 79 D
basic encoding rules (BER) 67,83 data abstracfton 101
basic rule system 90, 106 data base 150
behavior expression 49 data block 156
data tree 151, 154, 202
C data type 69
canonical tester 145,215 dependency graph 189
communicating rule system 90, 106 descriptive techniques 58
communicating rule systems (CRS) 3, distributed test method 145
65, 223
246
E G
effects 86, 91, 102 gate 86,93
encoding rules 67,83 gate compilation 180
endable 117 gate control block 170
entity 10, 13 gate specification 94
Estelle 31, 33, 126 generic gate machine 171
event 91,94 generic inference machine 170
event control block 175
event expression 94 H
event occurrence 91 high-level Petri net (HLPN) 44
event offer 86,91,94,113
event request 86, 91, 94, 113
event-based shell 204, 208 implementation environment 140
executable CRS K25 packet level pro- implementation under test (IUT) 143,
tocol specification 227 214
executable specification 125 inference machine 150
exhaustive validation environment 139 informal specification 22
expressive power 95 integrated environment 146
expressiveness 30, 104 integrated tools environment 197
extended abstract syntax notation one intelligibility 30, 92, 96, 104
(X-ASN.1) 66 interactive behavior simulation 212
extended finite state machine interleaving semantics 11 8
(EFSM) 33 internal event 112, 113
extemal event 111 internal synchronization 92
interpretation 187
F invertible execution 135
finite state machine (FSM) 32
flat rule system 96 K
formal definition 30, 101, 103 kernel 197,198,200
formal description 29
formal description technique (FDT) 3 L
formal description techniques (FDTs) 22, labelled transition system (LTS) 56, 66,
29 103,105
formal methods 15 layer 8,12
formal semantics 29 local object 90
formal syntax 29 local syntax 67
forward-chaining 150 logic interpreter 1 32
functional requirements 21 LOTOS 49, 51, 130
Index 247
X-ASN.1 66
X-ASN.1 compiler 201
X-ASN.1 data tree editor 202
X-ASN.1 encoder/decoder 202
X-ASN.1 integration 153
X-ASN.1 preprocessor 177,202
X-ASN.1 translation 152
X.25 packet level protocol
specification 225
X.25 packet level protocol (PLP) 22
z
Z 57, 58
Relative Com'plexities
of First Order Calculi
von Elmar Eder