ISO/IEC TR 10024:1992
(Main)Information technology — Telecommunications and information exchange between systems — Formal description of ISO 8073 (Classes 0, 1, 2, 3) in LOTOS
Information technology — Telecommunications and information exchange between systems — Formal description of ISO 8073 (Classes 0, 1, 2, 3) in LOTOS
Describes the classes 0 to 3 of the OSI transport protocol, defined in ISO 8073 using the formal description technique LOTOS, which is defined in ISO 8807. Transport protocol class 4 and NMCS are not covered. In view of complexity and widespread use of OSI standards it is imperative to have precise and unambiguous definitions of these standards. Formal Description Techniques form an effective approach to providing such definitions. Annexes A and B give definitions relating to the Transport and Network Services, Annex C gives an interpretation of ISO 8073, Annexes E and F include indices of process and type definitions.
Technologies de l'information — Télécommunications et échange d'informations entre systèmes — Description formelle de l'ISO 8073 (classes 0, 1, 2 et 3) en LOTOS
General Information
Standards Content (Sample)
ISO/IEC
TECHNICAL
REPORT
TR 10024
First edition
1992-07-O 1
---_---p -_.~ _____- -----.--- ----
..--.--- --------. -b-P___-
--
Information technology
- Telecommunications
and information exchange between systems -
Formal description of IS0 8073 (Classes 0, I9 2,
3) in LOTOS
Technologies de /‘information -- T6kcommunications et khange
d’informations entre syst&nes -- Description for-me//e de l’IS0 8073
(classes 0, I, 2 ei 3) en LO7-OS
Reference number
lSO/l EC TR 10024: 1992(E)
---------------------- Page: 1 ----------------------
l§O/lEC TR 10024 : 1992(E)
Contents
Foreword.i v
..v
Introduction .
..I
1 Scope.=
....................
..................................
.I
2 Normative references
.
3 Definitions.
..........................................
.............................. .I
4 Symbols and abbreviations
..I
5 Conven~ons .
.
6 Requirements. .
......................
.2
7 Introduction of the formal description.
.......................
-3
8 Specification parameters data types
....................................
IO
9 Static conformance
10 Dynamicconformance.ll
...................................
.I1
41 Service constraints
....................................
.I2
12 Service primitives.
.................................. .I3
13 Protocol constraints.
.....................................
.I5
14 Event Structures
....................
.I8
15 Identification of transport connections.
.......................
.22
16 Provision of a transport connection
......................... .26
17 Usage of a network connection.
.................. .28
18 Relationship between TPDUs and NSPs.
.....................................
.31
19
Abstract TPDUs.
...................... .41
20
Provision and negotiation of options
.................. .47
21 Relationship between TSPs and TPDUs.
.......................
.51
22 Release of a transport connection.
................................. 54
23 Numbering of TPDUs.
...................................
56
24 Explicit flow control
...................... .60
25
Assignment to network connections
............................. .67
26
Reassignment after failure.
..6 8
27 Errorrecovery. .
0 ISO/IEC 1992
All rights reserved. No part of this publication may be reproduced or utilized in any form
including photocopying and microfilm, without
or by any means, electronic or mechanical,
permission in writing from the publisher.
ISO/lEC Copyright Office l Case Postale 56 l CH-1211 Gen&ve 20 l Switzerland
Printed in Switzerland
ii
---------------------- Page: 2 ----------------------
ISO/IEC TR 10024 : 1992(E)
...........................
Retention and retransmission .70
28
...........................
acknowledgement of TPDUs. .77
29
....................................
Resynchronization .78
30
Association of TPDUs with transport connections. . .81
31
.....................
Multiplexing of a network connection .87
32
..............................
Resequencing in class 4. .90
33
Useofchecksum.9 0
34
.............................
Retransmission in Class 4. .90
35
Optional retransmission procedures in class 4 . 90
36
.............................. .90
37 Concatenation of TPDUs.
............... .92
38 Use of the network service expedited option.
............................
39 Treatment of protocol errors .93
..................................
40 Encoding of TPDUs. .95
..................................
41 Auxiliary definitions .I1 8
.............
Annex A Definitions relating to the Transport Service 131
..............
Annex B Definitions relating to the Network Service 139
.........................
.I44
Annex C Interpretation of IS0 8073.
....................................
Annex D Bibliography. .I45
.........................
Annex E Index of process definitions. 147
...........................
Annex F Index of type definitions. .I50
---------------------- Page: 3 ----------------------
ISO/IEC TR 10024 : 1992(E)
Foreword
IS0 (the International Organization for Standardization) and IEC (the Inter-
national Electrotechnical Commission) together form the specialized system
for worldwide standardization. National bodies that are members of IS0 or
IEC participate in the development of International Standards through tech-
nical committees established by the respective organization to deal with
particular fields of technical activity. IS0 and IEC technical committees col-
laborate in fields of mutual interest. Other international organizations,
governmental and non-governmental, in liaison with IS0 and IEC, also take
part in the work.
In the field of information technology, IS0 and IEC have established a joint
technical committee, lSO/IEC JTC 1.
The main task of technical committees is to prepare International Standards,
but in exceptional circumstances a technical committee may propose the
publication of a Technical Report of one of the following types:
when the required support cannot be obtained for the
- type 1,
publication of an International Standard, despite repeated efforts;
- type 2, when the subject is still under technical development or where
for any other reason there is the future but not immediate possibility of
an agreement on an International Standard;
- type 3, when a technical committee has collected data of a different
kind from that which is normally published as an International Standard
(‘state of the art’, for example).
Technical reports of types 1 and 2 are subject to review within three years
of publication, to decide whether they can be transformed into International
Standards. Technical reports of type 3 do not necessarily have to be re-
viewed until the data they provide are considered to be no longer valid or
useful.
lSO/IEC TR 10024, which is a technical report of type 2, was prepared by
Joint Technical Committee lSO/IEC JTC 1, Information technology.
Annexes A, B and C form an integral part of this Technical Report. Annexes
D, E and F are for information only.
iV
---------------------- Page: 4 ----------------------
ISO/IEC TR 10024 : 1992(E)
Introduction
In view of the complexity and widespread use of Open Systems Intercon-
nection standards it is imperative to have precise and unambiguous
definitions of these standards. Formal Description Techniques form an ef-
fective approach to providing such definitions. The use of Formal
Description Techniques in this area, however, is relatively new, and their ap-
plication on a wide scale requires an appropriate habituation period. Formal
descriptions should be introduced gradually in standards if initially the
number of National Bodies that are able to contribute to their development
is too small, thus allowing time to gain experience an to develop education
material.
Within lSO/IEC JTC l/SC 6 an ad-hoc group for the formal description in
LOTOS of the Transport Standards, viz. the Transport Service IS0 8072
and the Transport Protocol IS0 8073, was established in October 1985. The
Formal Description Technique LOTOS, defined in IS0 8807, was still under
development at that time within IS0 TC 97/SC 21. Following the position of
a majority of National Bodies, SC6 decided in January 1988 to progress both
formal descriptions as Type 2 Technical Reports. The main reason for not
incorporating them into the standards was that National Bodies expressed
their current lack of expertise on the subject of Formal Description Tech-
niques. It seemed therefore appropriate to let a period of time pass, during
which the formal descriptions can be read and compared with the standards,
and after which the status of the formal descriptions can be re-evaluated.
The purpose of this Technical Report is to provide a complete, consistent
and unambiguous description of classes 0,1,2 and 3 of IS0 8073. It forms
therefore a companion document to IS0 8073. This Technical Report has
successfully passed correctness and completeness tests with respect to
syntax and static semantics, according to the requirements of clause 3 of
IS0 8807. Tools are available that provide interactive simulation facilities, so
that confidence can be gained about the correctness of the description with
respect to the dynamic semantics (e.g. deadlock-freedom), and about its
correctness and completeness with respect to representation of intended
behaviour requirements. These tools are still at the stage of prototypes,
however.
This Technical Report contains the description of classes 0,1,2,3. Class 4
and NCMS are not yet included. This is due to the limited amount of resourc-
es allocated in JTC l/SC 6 to the work on formal descriptions.
Significant contributions for the application of LOTOS in this work have been
provided by Universities and research laboratories.
---------------------- Page: 5 ----------------------
This page intentionally left blank
---------------------- Page: 6 ----------------------
TECHNICAL REPORT lSO/lEC TR 10024 : 1992(E)
Information technology -Telecommunications and information
exchange between systems - Formal description of IS0 8073
(Classes 0,1,2,3) in LOTOS
1 Scope
This Technical Report describes the classes 0,1,2 and 3 of the OSI Transport protocol, defined in IS0 8073 using the formal de-
scription technique LOTOS, which is defined in IS0 8807. Transport protocol class 4 and NCMS are not covered.
2 Normative references
The following standards contain provisions which, through reference in this text, constitute provisions of this Technical Report. At
the time of publication, the editions indicated were valid. All standards are subject to revision, and parties to agreements based on
this Technical Report are encouraged to investigate the possibility of applying the most recent editions of the standards listed be-
low. Members of IEC and IS0 maintain registers of the currently valid International Standards.
IS0 7498: 1984, Information Processing Systems - Open Systems interconnection - Basic Reference Model.
Open Systems Interconnection - Transport service definition.
IS0 8072: 1986, Information Processing Systems -
lSO/IEC 8073’1, Information Technology - Telecommunications and information exchange between systems - Connection orient-
ed transpor? protocol specification.
IS0 TR 8509:1987, Information Processing Systems - Open Systems Interconnection - Service conventions
IS0 8807:1989, Information Processing Systems - Open Systems Interconnection - LOTOS - A formal description technique
based on the temporal ordering of observational behaviour.
lSO/IEC TR 10023:1992, Information Technology - Telecommunications and information exchange between systems - Formal
description of IS0 6072 in LOTOS.
Definitions
3
The definitions contained or referred to in clause 3 of IS0 8073 are adopted in this Technical Report.
4 Symbols and abbreviations
This Technical Report uses the symbols defined in clause 6 (formal syntax) and Annex A (data type library) of IS0 8807.
The symbols and abbreviations contained in clause 4 of IS0 8073 are employed in this Technical Report. When used without ref-
erence, ‘the protocol’ and ‘the service’ refer to IS0 8073 resp. IS0 8072.
Usage of other symbols and abbreviations is explained upon their first occurrence.
5 Conventions
Informal explanations precede the formal definitions to which they refer, separated from them by a line identical to the first line
below. Separation of formal definitions from subsequent informal explanations is indicated by a line identical to the second line
below.
*
>
*
(
NOTE - This convention is consistent with the rules on delimitation of comments defined for LOTOS in IS0 8807. The formal text is set in Courier and the LOTOS
keywords and operators are in boldface. Identifiers from the formal text are set in italics when used in the non-formal text.
The conventions defined in IS0 TR 8509 are adopted, but together with the following one: the term “Request” refers both to request
and to response service primitives, and the term “Indication” refers both to indication and to confirm service primitives,
1) Under revision
---------------------- Page: 7 ----------------------
lSO/lEC TR 10024 : 1992(E)
The conventions defined in IS0 TR 8509 are adopted, but together with the following one: the term ‘Request’ refers both to request
and to response service primitives, and the term ‘Indication’ refers both to indication and to confirm service primitives.
Parentheses are omitted in this specification in the following cases, where their removal is allowed by IS0 8807:
a) In expressions where, due to the fact that binary infix operators associate to the left, no ambiguity arises from removal of
parentheses (subclause 6.2.8 of IS0 8807). Thus, for example, the expression ‘(x gt 0) and (y It 5)’ is specified as ‘x gt 0 and
(y/t 5)‘.
b) In expressions where, due to the priority of LOTOS behavioural operators, no ambiguity arises from removal of parenthe-
( stop) ’ is specified as ‘g; stop'.
ses. Thus, for example, ‘g;
The LOTOS standard allows the use of explicit sort specification for simple-expression using the ‘ofsort’ terms. Such ‘ofsort’ terms
are present in the specification only in those cases where their absence would give rise to ambiguity.
6 Requirements
This Technical Report complies with the requirements defined by clause 3 of IS0 8807.
No conformity requirements are defined by this Technical Report, but the conformance requirements defined by IS0 8073 are rep-
resented formally in LOTOS.
7 Introduction of the formal description
The present specification is designed on basis of two major requirements, which together provide the appropriate framework for
the formal representation of the transport protocol architecture by way of a formal specification of a generic transport protocol en-
tity:
a) the formal specification is to be provably consistent with the formal description in LOTOS of the OSI connection-oriented
transport service IS0 8072 (TS FD for short, that is available in IS0 TR 10023), assuming a correct formal description in
LOTOS of the OSI connection-oriented network service IS0 8348 (NS FD for short),
b) the specification applies to any transport protocol entity which is claimed to comply with the requirements defined in the
conformance clause of the protocol.
Figure 1 shows the resulting structure of the specification.
A formal data type is provided for the implementor’s declaration of classes and options that are defined in the conformance clause
of the protocol. Such a declaration is formally represented by a parameter of the specification. A boolean-valued function can be
applied to the value of this parameter, that determines whether or not the value satisfies the static conformance requirements of
the protocol (see clause 9).
Only if the static conformance requirements are satisfied, does the specification describe active behaviour, viz. it provides the im-
plementor or tester with an abstract model of the protocol dynamic conformance requirements (see clause IO)
specification parameters:gates: t,n
SAP addresses
Implementation options
global type definitions: library data types
SAP address types
Implementation option types
Auxiliary data types
behaviour definition: if static conformance requirements are
satisfied by the implementation options
then dynamic conformance requirements
else no behaviour
Figure 1 - Structure of the specification
---------------------- Page: 8 ----------------------
ISO/IEC TR 10024 : 1992(E)
The t (resp. n) gate represents the transport (resp. network) service boundary accessed by the entity. It models the totality of
TSAPs (resp. NSAPs) at which the entity interacts with the TS user (resp. NS provider). Each TSAP (resp. NSAP) is uniquely iden-
tified by a TSAP address (resp. NSAP address) out of the set tas (resp. nas).
Proper co-operation between session and transport entities (and transport and network entities, resp.), within one open system, is
ensured by assigning the same tas to the session and transport entities (and the same nas to the transport and network entities,
resp.) residing in the same open system. This implies that a transport entity cannot co-operate with a session entity if they reside
in different open systems.
The event structure at gate f consists of a triple of values, resp. of sorts TAddress, TCH, TSP (see clause 8). The first value iden-
tifies the TSAP where the interaction occurs. The second value identifies the TCEP, within that TSAP, where the interaction occurs.
The third value is the Transport Service Primitive (TSP) executed in the interaction. A similar structure is shown by events at gaten.
These event structures are the same as in the respective service formal descriptions, with the exception that this Technical Report
describes a more refined, non-atomic execution of T-DATA primitives. This is required by correctness and generality of represen-
tation of the requirements relating to segmenting and flow control procedures. Clearly, also the data type definition of TSPs needed
corresponding refinements: the definition presented in this Technical Report is a conservative extension of the definition found in
the formal description in LOTOS of the transport service.
Full account is taken of the multiplicity aspects of the protocol. The behaviour of a never terminating transport entity is described.
According to the definition of process TpEnMy (see clause IO), some of the component processes describe constraints that apply
to, and depend upon, the behaviour of the protocol entity at only one of the two service boundaries. This class of constraints will
be referred to as ‘service constraints’ (see clause 1 I), whilst the term ‘protocol constraints’ will refer to those which are described
by the other components (see clause 12).
The service constraints ensure, for instance, that the address component of an interaction at t (resp. n) is a member of the set tas
(resp. nas), that the identification of a connection by means of a connection endpoint identifier is unique within the scope of any
given address, that the entity is ready to accept and support at least one TC and at least one NC, and so on.
The further decomposition of the protocol constraints exploits the usage of internal gates. Notice that, according to the formal se-
mantics of LOTOS, the presence of internal gates in the specification by no way constrains the internal structure of any
implementation, inasmuch as the specification requirements apply to the behaviour observable at service access points only.
The introduction of these internal gates and the definition of the event structures (see 14) enable a clear separation
of concerns between:
a) independent constraints on the provision of TCs (see clause 15, clause 16, clause 18, clause 20 through clause 24, clause
33 through clause
36, clause 39, clause 40),
b) independent constraints on the usage of NCs (see clause 17, clause 32, clause 37, clause 38),
c) dependencies between provision of TCs and usage of NCs, such as those relating to assignment of TCs to NCs (see clause
25), error recovery procedures (see clause 26 through clause 30), and association of TPDUs to TCs (see clause 31).
A distinction is made between the definition of abstract TPDU structures(see clause 19), where abstraction is made from the TPDU
information that relates to TC identification, encoding, and encoded TPDUs, which are octet strings where all of the TPDU infor-
mation is fully specified (see clause 40).
Some auxiliary definitions are finally presented (see clause 41), which do not directly represent constraints found in the protocol,
but are frequently employed in the preceding formal definitions. Processes that have a name beginning with Run are all defined in
clause 41.
Except for the definitions of the specification parameter types, definitions shared with the TS FD, IS0 TR 10023, and sharable with
a NS FD are presented in Annex A and Annex 6 respectively. The data types referred to in the library construct are imported from
the LOTOS library of data types.
*
)
specification TransportProtocolEntity[t, n]
(tas : TAddresses, nas : NAddresses, tpeo : TPEOptions) : noexit
library Set, String, NaturalNumber, NatRepresentations, DecNatRepr, Octetstring, Octet, Bit,
BitNatRepr, Boolean, FBoolean, Element
endlib
Specification parameters data types
a
81 . General
Two of the three specification parameters (see clause 7) have simple structures: finite sets of addresses and are presented in 8.2.
---------------------- Page: 9 ----------------------
ISO/IEC TR 10024 : 1992(E)
The options parameter contains the description of the optional procedures and their parameters, viz. supported classes, supported
roles (M&or or responder), maximum TPDUsize for each supported class and the optional procedures listed in table 9 of the
protocol.
It has a slightly more complicated structure, which can be summarized as follows: a value of sort TPEOptions is a 4tuple (see 8.3),
where the components correspond to the requirements mentioned in subclause 14.6 of the protocol. The component structures
are respectively described in 8.3.1 through 8.3.4.
82 . Address sets
Although some these definitions below are shared with the TS FD or can be shared with the NS FD, these definitions are presented
here, instead of in clause A.2, resp clause B.2, to allow description of the specification parameters.
*
>
type TransportAddress
is GeneralIdentifier renamedby
sortnames
TAddress for Identifier
opnnames
SomeTAddress for SomeIdentifier
AnotherTAddress for AnotherIdentifier
endtype (* TransportAddress *)
type TransportAddresses
is Set actualizedby TransportAddress using
sortnames
TAddress for Element
Boo1 for FBool
TAddresses for Set
endtype (* TransportAddresses *)
type NetworkAddress
is GeneralIdentifier renamedby
sortnames
NAddress for Identifier
opnnames
SomeNAddress for SomeIdentifier
AnotherNAddress for AnotherIdentifier
endtype (* NetworkAddress *)
type NetworkAddresses
is Set actualizedby NetworkAddress using
sortnames
NAddress for Element
Boo1 for FBool
NAddresses for Set
endtype (* NetworkAddresses *)
*
(
83 . Options
A value of sort TPEOptions is a 4-tuple constructed by the function TPEOptions. The functions Classes, Roles, OptionalProce-
dures and MaxTPDUSizeMap are projection functions, viz. application of each of them to a quadruple yields the value of one
distinct component. The definition of boolean equality is straightforward.
type TPEOptions
is Classes, TPEntityRoles, OptionalProcedures, MaxTPDUSizeMap, PrMaxTPDUSize
sorts
TPEOptions
opns
TPEOptions : Classes, TPERoles, OptionalProcedures,
MaxTPDUSizeMap, PrMaxTPDUSize --> TPEOptions
Classes -> Classes
: TPEOptions
Roles : TPEOptions -> TPERoles
OptionalProcedures --> OptionalProcedures
: TPEOptions
MaxTPDUSizeMap --> MaxTPDUSizeMap
: TPEOptions
PrMaxTPDUSize -> PrMaxTPDUSize
: TPEOptions
-= Boo1
: TPEOptions, TPEOptions
-eq_f -ne-
eqns
forall
4
---------------------- Page: 10 ----------------------
lSO/lEC TR 10024 : 1992(E)
t, t1, t2 : TPEOptions, c, cl : Classes, r, rl : TPERoles, p, pl : OptionalProcedures,
s, sl : MaxTPDUSizeMap, pm, pm1 : PrMaxTPDUSize
ofsort Classes
Classes(TPEOptions(c, rr p, s, pm)) = c;
ofsort TPERoles
Roles(TPEOptions(c, r, p, s, pm)) = r;
ofsort OptionalProcedures
OptionalProcedures(TPEOptions(c, r, p, s, pm)) = p;
ofsort MaxTPDUSizeMap
MaxTPDUSizeMap(TPEOptions(c, r, p, s, pm)) = s;
ofsort PrMaxTPDUSize
PrMaxTPDUSize(TPEOptions(c, r, p, s, pm)) = pm;
ofsort Boo1
TPEOptions(c, r, p, s, pm) eq TPEOptions(cl, rl, pl, sl, pml)
=
c eq cl and (r eq rl) and (p eq pl) and (s eq sl) and (pm eq pml);
tl ne t2 = not(t1 eq t2);
endtype (* TPEOptions *)
*
(
8.3.1 Protocol classes
The five protocol classes are represented by corresponding constants of sort Class. These are ordered by means of the auxiliary
function h, that maps classes to natural numbers, C/asses defines finite sets of protocol classes, enriched with the function High-
erC/asses which yields the set of classes higher than a given class. This function is made use of in the description of class
negotiation (see 20.2.2).
*
)
type Class
is NaturalNumber
sorts
Class
opns
--> Class
ClassO, Classl, Class2, Class3, Class4 :
--> Boo1
le-, -It-, -ge-, -gt- : Class, Class
- eq_f .Je.3 -
-> Nat
h : Class
eqns
forall
x, y : Class
ofsort Nat
h(ClassO) = 0;
h(Class1) = succ (h(Class0));
h(Class2) = succ (h(Class1));
h(Class3) = succ (h(Class2));
h(Class4) = succ (h(Class3));
ofsort Boo1
= h(x) eq
x WI Y h(y);
= h(x) ne
x ne y
h(Y);
= h(x) le
x le y
h(y);
= h(x) It
x 1t y
h(y);
= h(x) ge
x ge Y h(y);
= h(x) gt
h(y);
x gt Y
endtype (* Class *)
type BasicClasses
is Set actualizedby Class using
sortnames
Class for Element
Boo1 for FBool
Classes for Set
endtype (* BasicClasses *)
type Classes
is BasicClasses
opns
: Class 4 Classes
HigherClasses
eqns
forall
c, d : Class
ofsort Classes
---------------------- Page: 11 ----------------------
ISO/IEC TR 10024 : 1992(E)
HigherClasses(Class4) = {};
= succ(h(c)) => HigherClasses = Insert(d, HigherClasses(d
h(d)
endtype (* Classes *)
*
(
8.3.2 Entity roles
An entity can either initiate CR TPDUs (initiator), respond to CR TPDUs (Responder) or both (see 8.4 for TwoTuplet).
*
)
type TPEntityRole
is TwoTuplet renamedby
sortnames
TPERole for Tuplet
opnnames
Initiator for TheOne
Responder for TheOther
endtype (* TPEntityRole *)
type TPEntityRoles
is Set actualizedby TPEntityRole using
sortnames
TPERole for Element
Boo1 for FBool
TPERoles for Set
endtype (* TPEntityRoles *)
8.3.3 Optional procedures
OptionalProcedure defines constants for those procedures that have some ‘optional’ entry in table 9 of the protocol. The auxiliary
function h enables a concise specification of boolean equality. The boolean functionsApplies/n specify whether a given optional
procedure applies in a given class, or in some class of a given set of classes.
NOTE - The two functions Applies/n differ in the second argument.
*
>
type OptionalProcedure
is Classes, DecNatRepr
sorts
OptionalProcedure
opns
TPDUWithoutChecksum, NoFlowControl, ExtendedFormats, UseOfNSReceiptConfirmation,
-> OptionalProcedure
UseOfNSExpedited, UseOfSAck, UseOfRAck :
-> Nat
h : OptionalProcedure
: OptionalProcedure, OptionalProcedure --> Boo1
,eqJ ne
--> Boo1
-Appli&Ii- : OptionalProcedure, Class
-AppliesIn- : OptionalProcedure, Classes --> Boo1
eqns
forall
: OptionalProcedure, c : Class, cs : Classes
PI Pl
ofsort Nat
h(TPDUWithoutChecksum) = 0;
= succ(h(TPDUWithoutChecksum));
h(NoFlowContro1)
h(ExtendedFormats) = succ(h(NoFlowContro1));
= succ(h(UseOfNSReceiptConfirmation));
h(UseOfNSReceiptConfirmation)
h(UseOfNSExpedited) = succ(h(UseOfNsReceiptConfirmation));
= succ(h(UseOfNsExpedited));
h(UseOfSAck)
h(UseOfRAck) = succ(h(UseOfSAck));
ofsort Boo1
P eq Pl = h(P) eq h(Plb
= not(p eq pl);
P ne Pl
TPDUWithoutChecksum AppliesIn c = c eq Class4;
NoFlowControl AppliesIn c = c eq Class2;
ExtendedFormats AppliesIn c = c ge Class2;
UseOfNSReceiptConfirmation AppliesIn c = c eq Classl;
UseOfNSExpedited AppliesIn c = c eq Classl;
UseOfSAck AppliesIn c = c eq Class4;
UseOfRAck AppliesIn c = c eq Class1 or (c ge Class3);
6
---------------------- Page: 12 ----------------------
ISO/IEC TR 10024 : 1992(E)
p AppliesIn {} = false;
=> p AppliesIn cs = true;
c IsIn cs, p AppliesIn c
=> p AppliesIn Insert(c, cs) = p AppliesIn cs;
c NotIn cs, not(p AppliesIn c)
endtype (* OptionalProcedure *)
type OptionalProcedures
is Set actualizedby OptionalProcedure using
sortnames
OptionalProcedure for Element
Boo1 for FBool
OptionalProcedures for Set
endtype (* OptionalProcedures *)
*
(
8.3.4 Maximum TPDU sizes
MaxVYXISize defines seven constants that represent the values listed in subclause 14.6 of the protocol, and the functions TP-
DUSize, which yields the corresponding natural number, and AkxTPDUSizeFor, which yields the maximum TPDU size defined by
the protocol for each class (see subclause 13.3.4.b of the protocol). Equality and order of the constants are respectively specified
by means of equality and order of their corresponding TPDUSize value.
Max-TPDUSizes defines sets of MaxTPDUSize values, and the boolean functions Maxln, which tells whether a given AkxFW-
Size value is the maximum in a given set of such values, and Maximal, which tells whether a given set of AkxTpDusize values
contains all the values lower than or equal to the maximum value that it contains.
MaxTPDUSizelnClass defines pairs < MaxTPDUSize x C/ass > (see 8.4 for the definition of the generic type Pair). BasicMaxTP-
DUSizeMap defines sets of these pairs as values of sort MaxTPDUSizeMap.
In fact, a value of sort MaxTPDUSizeMap can be viewed as a binary relation between MaxTPDUSize and C/ass: in this view, the
type MaxTPDUSizeMap endows the basic type with the functions C/asses, which yields the range of the argument relation, and
MaxTPDUSizesOf which, for given class and relation, yields the subset of the domain of the given relation characterized by the
given class.
NOTE - The expression 7 + (2 + De@)) below denotes a string of decimal digits, where ‘+’ denotes digit concatenation with a digit string. The corresponding
natural number value (128, in this case) is obtained by ap
...
Questions, Comments and Discussion
Ask us and Technical Secretary will try to provide an answer. You can facilitate discussion about the standard in here.