ГОСТ Р ИСО/МЭК ТО 10023 -93
ГОСУДАРСТВЕННЫЙ СТАНДАРТ РОССИЙСКОЙ ФЕДЕРАЦИИ
ИНФОРМАЦИОННАЯ ТЕХНОЛОГИЯ
ПЕРЕДАЧА ДАННЫХ И ОБМЕН ИНФОРМАЦИЕЙ МЕЖДУ СИСТЕМАМИ. ФОРМАЛИЗОВАННОЕ ОПИСАНИЕ УСЛУГ ТРАНСПОРТНОГО УРОВНЯ
(ГОСТ 34.960-91) НА ЯЗЫКЕ
LOTOS
Издание официальное
БЗ 12-92/1177
ГОССТАНДАРТ РОССИИ Москва
ГОСТ Р ИСО/МЭК ТО 10023-93
Предисловие
I ПОДГОТОВЛЕН И ВНЕСЕН Техническим комитетом по стандартизации ТК 22 «Информационная технология»
2 УТВЕРЖДЕН И ВВЕДЕН В ДЕЙСТВИЕ Постановлением Госстандарта России от 29.12.93 № 293
Настоящий стандарт подготовлен на основе применения аутентичного текста международного стандарта ИСО МЭК ТО 10023— 92 «Информационная технология. Передача данных и обмен информацией между системами. Формализованное описание ИСО 8072 на LOTOS»
3 ВВЕДЕН ВПЕРВЫЕ
© Издательство стандартов, 1994
Настоящий стандарт не иожет быть полностью или частично воспроизведен, тиражирован и распространен в качестве официального издания без разрешения Госстандарта России
П
ГОСТ Р ИСО МЭК 10 10023-93
СОДЕРЖАНИЕ
I Область применении '.....
2 Нормативные ссылки . . .....
3 Определения ... . . , . ,
4 Символы и сокращения.......
5 Соглашения ........
6 Требования . .
7 Введение о формализованное описание
3 Типы данных на интерфейсе ...
9 Глобальные ограничения . . . .
10 Обеспечение транспортного соединения
I I Локальные ограничения для оконечного пункта ТС
12 Межоконечяые ограничения для -одного ТС
13 Идентификация транспортных соединений
м Принятие транспортных соединений
15 Управление потоком пун помощи обратной связи
16 Передача в режимебез-устаиоэлсиия-сосяинения Библиографические данные......
I 1 2 о
2 Я о
.и 37 В 45 46 47
49
III
ГОСТ Р ИСО'МЭК ТО 1002.4-9,1
ГОСУДАРСТВЕННЫЙ СТАНДАРТ РОССИЯСКОП ФЕДЕРАЦИИ
Информационная технологии
ПЕРЕДАЧА ДАННЫХ И ОБМЕН ИНФОРМАЦИЕЙ МЕЖДУ СИСТЕМАМИ. ФОРМАЛИЗОВАННОЕ ОПИСАНИЕ УСЛУГ ТРАНСПОРТНОГО УРОВНЯ с ГОСТ 34.960 -91) НА ЯЗЫКЕ LOTOS
Inlonnalion Technology. Telecommunications, and Inionnation Exchange Bel ween Systems. Formal Description of 8072 in LOTOS
Дата введения (994—07—01
1 ОБЛАСТЬ ПРИМЕНЕНИЯ
Настоящий стандарт распространяется на транспортный уровень эталонной модели взаимосвязи открытых систем (ВОС) и определяет услуги транспортного уровня ВОС, определенные в ГОСТ 34.960. при1 помощи метода формализованного описания LOTOS, определенного в ИСО 8807.
Примечание — Формальное определение типов данных и процессы, представленные в настоящем стандарте, могут использоваться для формализованного описания протоколов транспортного и сеансового уровней ВОС на языке LOTOS
2 НОРМАТИВНЫЕ ССЫЛКИ
Нижеперечисленные стандарты содержат положения, которые путем ссылок на них по тексту образуют положения настоящего стандарта. Все ссылки предполагают последнее издание указанных стандартов.
Национальные комитеты — члены МЭК и ИСО имеют списки международных стандартов, действующих на текущий момент.
ГОСТ 28906- 91 (ИСО 7198-84. ИСО 7498-84 Доп. 1-84) Системы обработки информации. Взаимосвязь открытых систем. Вазовая эталонная модель
ГОСТ 34.960—91 (ИСО 8072— 86, Доп. 1—86 ИСО 8072—86) Системы обработки информации. Взаимосвязь открытых систем. Определение услуг транспортного уровня
Издание официальное!
ГОСТ Р ИСО.'МЭК ТО 10023-93
ИСО 8072—86/Поп. 1 Системы обработки информации. Взаимосвязь открытых систем. Определение услуг транспортного уровня. Техническая поправка I*.
ИСО/ТО 8509—87 Системы обработки информации. Взаимосвязь открытых систем. Соглашения по услугам *.
ИСО 8807—89 Системы обработки информации. Взаимосвязь открытых систем. LOTOS — метод формализованного описания, основанный на упорядочении во времени наблюдаемого поведения ♦.
ИСО/МЭК ТО IOO24 92 Информационная технология. Передача данных п обмен информацией между системами. Формализованно описание ИСО 8073 (разделы 0. I. 2 и 3) на языке LOTOS *.
3 ОПРЕДЕЛЕНИЯ
В настоящем стандарте используются определения, приведенные в ГОСТ 34 960.
4 СИМВОЛЫ И СОКРАЩЕНИЯ
В настоящем стандарте используются символы, определенные в разделе 6 (формальный синтаксис) и приложении А (библиотека типов данных) ИСО 8807.
_В настоящем стандарте используются сокращения. Содержащиеся в разделе 4 ГОСТ 34.960. Использование других символов и сокращений поясняется при первом их появлении.
5 СОГЛАШЕНИЯ
Неформальные пояснения, предшествующие формальным определениям. к которым они относятся, отделяются от последних показанной ниже верхней линией. Отделение формальных определений от последующих неформальных пояснении обозначается показанной нижней линией.
♦ До пряного применения данного документ! а качестве государственного стандарта его- распространение осуществляет секретариат ТК 22 «Информационная технология».
2
ГОСТ Р ИСО МЭК ТО 10023-93
Примечание — Это соглашение соответствует правилам, ощапичсиий комментариев, определенным для LOTOS в ИСО 6807. Формальный текст представлен курсивом, з ключевые слова и операторы LOTOS — полужирным- шрифтом. Идентификаторы из фурмагчфощнкого текста в неформатированном тексте набраны курсивим,
Соблюдаются соглашения, определенные в ИСО/ТО 8509, но с учетом следующего: термин «запрос» означает как запросные, так и ответные сервисные примитивы, а Термин «индикация» Означает сервисный примитивы как индикации, так и подтверждения.
6 ТРЕБОВАНИЯ
Настоящим стандарт отвечает требованиям, изложенным в разделе 3 ИСО 8807 (более подробную- информацию см. в приложении С к указанному стандарту). Настоящий стандарт не содержит каких-либо требований к соответствию.
7 ВВЕДЕНИЕ В ФОРМАЛИЗОВАННОЕ ОПИСАНИЕ
Вся граница услуг формально представлена в виде единственного шлюза I. Структура события в I представляет собой тройку значений типа TAddress. ТС El, TSP (см, раздел 8). Первое значение идентифицирует TSAP. в котором происходит взаимодействие. Второе значение идентифицирует ТСЕР внутри TSAP. о котором происходит взаимодействие. Третье значение — это выполняемый при взаимодействии примитив транспортного уровня (TSP). Конкретные значения зависят от многих аспектов услуги.
Описывается поведение поставщика услуг бесконечного вида. Спецификация не содержит параметров-.
Используется стиль спецификации, ориентированный на ограничения. поскольку он наиболее подходит для определительного характера стандарта по- услугам. Описание ориентировано на характеристики модальностей поведения поставщика услуг исключительно в терминах последовательности выполняемых TSP, т. е. без каких-либо предположений о внутренней структуре самого поставщика.
В основе первой декомпозиции специфицируемого поведения лежат следующие отдельные ограничения:
а) поставщик услуг может допускать множество, возможно.одновременных соединений (представленных процессом TConnodiofis? см. раздел 9). вместе со
Ь) средством выбора среди одновременных соединений нужного (представленным процессом TCIdentHication, см. раздел 13), но при
3
ГОСТ Р ИСО. МЭН ТО 10023-93
с) возможности внутреннего нелетерцинизма при установлений любого дополнительного соединения, если, по меньшей .мере, одно соединение уже поддерживается (представленной процессом TCAcceptance, см. раздел 14), и
il) возможности внутреннего нсдетерминмэма при передаче Даниил (представленной процессом ТВаскрге$$иге. см раздел 15); при помощи этого принимающий пользователь вызывает эффект управления потоком, сообщая об этом передающему пользователю.
Спецификация динамического поведения предваряется спецификацией типов данных на интерфейсе (см. раздел 8). Такие определения являются общими для формализованных описаний, которые могут взаимодействовать, а именно для протоколов транспортного и сеансового уровней.
Порядок представления остальных определений обоснован желанием следовать порядку, установленному ГОСТ 34.960, который в основном связан с обеспечением единственного ТС. Описание требований, являющихся локальными для обеспечения одного ТС (представлены в разделах 10, II и 12), предшествуют описаниям глобальных требований, упомянутых выше в Ь), с) и d) соответственно.
Типы данных, определенные конструкцией library, импортируются из библиотеки типов данных LOTOS.
--------------------------------------------------------------„> specification TransportService|t] : noexit
library Set. Element, OctetSlring, N at Re presentation, NaluralNum* ber. Boolean. FBoalean. DecNatRepr end lib
8 ТИПЫ ДАННЫХ НА ИНТЕРФЕЙСЕ
8.1 Общее описание
В соответствии с представлением взаимодействий на границе транспортных услуг (см. раздел 7) типы данных на интерфейсе состоят из трех основных определений, которые соответственно составляют вилы TAddress (см. 8.2), TCEI (см. 8.3) н TSP (см. 8.4). Параметр TSP — качество услуги — определяется в 8.5, а остальные параметры — в м.6 В 8.7 представлены вспомогательные определения.
8.2 Транспортный адрес
В ГОСТ 34.960 не определена структура транспортного адреса. Следующее определение использует определение Generalidentifier
4
ГОСТ Р ИСО МЭК ТО 10023—93
(см. 8 7) и позволяет представлять бесконечное число транспортных адресов.
-------------------------------------------------------------------’) type Transport Address
is General Identifier renamed!))' sort names
TAddress for identifier opnnames
SomeTAd dress for SomeJdentifier
AnotfierTAddress For Another Identifier endtype (* TransportAddress *)
l „т.,.,»..,,,..»^,^.^.».....^-.....—«... -_-__-___...—-—«. ^.... .^...•-« — .--.-—---.-- —---
8 3 Идентификатор оконечного пункта транспортного соединения
В ГОСТ 34.900 не определена структура идентификатора оконечного пункта транспортного соединения. Приводимое ниже первое определение позволяет представить бесконечное их число. Второе определение представляет идентификаторы оконечного пункта транспортного соеанийния, которые являются глобальными для всей границы транспортных услуг. Каждый из них представляет собой пару TAddfessXTCEl (общее определение Pair и General-Identifier см. в 8.7).
type TCEndpointIdentifier
is General Identifier renamedby sort names
TCEI for identifier
opnnames
SomeTCE! for SomeJdentifier
AnotherTCEl for Another Identifier
endtype (“ TCEndpointfdentifier *)
type TCEIdentificalion
is Pair actualizedby TransportAddress. TCEndpointfdentifier using soTtnames
TAddress for Element
TCEI for Element
Bool for Fbool
Tld for Pair opnnames
Tld for Pair
5
ГОСТ Р ИСОМЭК ТО 10023-93
ТА for First
TCEl for Second
endtype (’ TCEIdentificalion *)
Г____________________________________________________________
8 4 Сервисный прими тин транспортного v ров-ft я (Т S Р)
8.4.1 Общее описание
Тип данных TCP представлен, начиная с базовой конструкции значений вида TCP (см. ниже). Эта конструкция является прямой формулировкой определения, приведенного в таблице 3 ГОСТ 34.560. Функции, генерирующие значения TCP. называются «конструкторами ТСР». Это определение заимствует определения, связанные с параметрами TCP (см. 8.6).
Примечание — 8 некоторых TCP параметр L’serData представляет собой OctetString, ямеюшнй фиксированные Гранины, хак определено t» ГОСТ 34 960 По техническим сопряжениям эти требование формально представлено пролессом ограничения (см 11.1 и 11-4), а не ограничивавшим типам.
В 8.4.2 приведена классификация TCP. которая позволяет, с одной стороны, простым путем расширить базовую конструкцию дополнительными функциями (см. 8.4.3). а с другой — консервативно расширить тип данных в формализованном описании транспортного протокол».
type BasicTSP
is TransportAddrcss, TEXOptior. TSQuality, OctetString. TDlSRca-son, TsCIQuality sorts
TSP
opns | TCONreq, TCONind | TAddress. TAddress. TEX- |
TCONresp, TCONconf | Option, TQOS. Octet String —> TSP TAddress. TEXOption. TQOS. | |
TDTreq, TDTind | OctetString —> TSP OctetString — > TSP | |
TEXrcq, TEXind | OctetString —> TSP | |
TDISreq | OctetString —> TSP | |
TDJSind | TDlSReason. OctetString | |
TUDTreq, TUDTind | —> TSP TAddress, TAddress. CIQOS, |
6
ГОСТ Р ИСО.'МЭК ТО 10023-93
OctetString —> TSP endtype (* BasicTSP *)
С............................................
8.4 2 Классификация сервисных примитивов транспортного уровня
8.4.2.1 Базовая классификация
Базовая классификация TCP определена при помощи TCPSuh-sort, состоящего из набора констант, каждая из которых задает имя TCP в соответствии с таблицей 3 ГОСТ 34.9=60.
Тип TCP BasicClassi tiers — это функциональное расширение базовой конструкции в 8.4.1. где:
а) функция Subsort генерирует имя TCP;
b) булевы функции на TCP, названные «определителями подвида ТСР», определяются в соответствии с базовой классификацией, введенной при помощи TCPSubsort.
Примечание — Вспомогательная функция И. отображающая имена TCP на натуральные числа, определяется для упрощения спецификации Нулевых операций равенств ла именах TCP (так же, как на TCP в 8.4 33) Определение IsRcquest vindication (иа именах TCP) я laTreq. blind (на TCP) отражает соглашение, введенное в радел 5.
type TSPSubsort is NaturalNumber sorts
TSPSubsort op ns
TCONNECTrequesi. TCONNECTindication. TCONNECTres-ponse, TCONNECTconfirm. TDATArequest, TDATAindica-lion. TEX DATA request. TEXDATAindicaiion, TDISCONN-request, TDlSCONNindication, TU DATA request, TUDATA-indication ; — > TSPSubsort
h : TSPSubsort • —> Nat
Even, Odd ; Nat —> Bool
IsRequest, ^Indication : TSPSubsort —> Bool
eq—ne_ : TSPSubsort, TSPSubsort
—> Bool eqns forall
s, si : TSPSubsort, n : Nat of sort Nat
h (TCONNECTrequesi) = 0;
7
ГОСТ Р ИСО .МЭК ТО 10023-93
h(TCONNECTindicatiOn) = SuccfblTCONNECTrequest)); h (ICON МЕСТresponse) = Slice (h (TCONNECTindication)); MTCQNNECTconfinn)-Succ(h(TCONNECTresponsc)); h(TDATArequest) = Succ(h (TCONMECTconfirm));
h(TDATAindication) = Succ (h(TDATArequest)); h(TEXDATArequest) = Succ(h (TDATAindication)); h(TEXDATAindicalion) = Succ (h (TEXDATA request)); h(TDlSCONNrequest) = Succ th (TEXDATAIndicaiion)); h(TDI5CONNindication)-Succ(h(TDISCONNrequest));
ofsort Bool
Even(O) = true:
Even(Succ(.0)) -false.
Even (Succ (Succ (n) ))»* Even (n);
Odd(n) ~ not (Even (n));
IsRequesl(s) = Even (h (.$))< Islndication(s) = Odd(h(s)>; s eq si = h(s) eq h(sl);
s me si = not(s eq si): endtype (* TSPSubsort *) type TSPBasicCla?sifiers is BasicTSP, TSPSubsort opns
Subsort : TSP —> TSPSubsort
IsTCON. IsTCON!, lsTCON2. IsTDT, IsTEX. IsTDIS, IsTCONreq. isTCONind, IsTCONresp, IsTCONconf, IsTDTreq. IsTDlSind, IsTReq. IsTlnd : TSP — > Bool cqns forall
a. ah a2 : TAddress, ж : TEXOption. q : TQOS, d : OctetString, r : TDISReason, t : TSP. dq : CLQOS ofsort TSPSubsort
Subsort(TCONreq(al, a2. x. q, d))—TCONNECTrcqucst;
Subsort (ICON! nd (a I, a2. x. q, d))-TCONMECT-indication;
Subsort (TCONresp(a, x, q. d)) =TCONNECTresponse; Subsort(TCONconf(a. x, q. d)) =TCONNECTconfirm; Subsori (TDTrcq(d)) -TDATArequest;
Subsort (TDTind(d)) ^TDATAindication;
Subsort (TEXreq (d) j =TEXDATArequcsk Subsort (TEXind(d)) =TEXDATAindication; Subsort (TDlSrcq(d)) =TD!SCONNrequest; Subsort f.TD!Sind(r, d)) =TDlSCONNindicat5on;
В
ГОСТ Р ИСО МЭК ТО 10023-93
Subsort (TUDTreq (al, а2, dq. d)) =TUDATArequest;
Subsort (TUDTind (al, a2, do, d)) =TUDATAindication; ofsort Boo!
bTCON0)~lsTCONI(l) or lsTC0N2(t);
IsTCONI(t)-IsTCONreq(t) or !sTCONind(l);
lsTCON2(J)~ IsTCO\:resp(t) or FsTCONconf (I);
IsTDT (t) =l$TDTreq(t) or (sTDTind(t);
IsTEX (t) = IsTEXreq(t) от IsTEX ind (I);
IsTDIS(t) =lsTDISreq(t) or IsTDISind(t);
IsTCONrcq(t) = Subsori (I) eq TC ON NEGI request;
IsTCONindfO Subsort(t) eq TCONNECTindication;
IsTCONresp(l) = Subsort(t) eq TCOMNECTresponse;
IsTCONconf(t) =Sub$orl(t) eq TCONNECTconfinn;
IsTDTrcqO) = Subsort (t) eq TDATArequest;
IsTDTind(t)— Subsort (t) eq TDATAindication;
IsTEXreq(t) “Subsort (t) eq TEX DA TA request;
IsTEXind (t) “Subsort (t) eq TEXDATAindication;
IsTDISreq(t) “Subsort(t) eq TDISCONN request;
IsTDISind(t) “Subsort(t) eq TDFSCONNindicaticn; hTUDT(t)“lsTUDTreq(t) or IsTUDTind (t);
IsTUDTreq(t) —Subsort(t) eq TU DAT A request;
IsTCDTindil) “Subsort(t) eq TUDATAitidieation;
IsTReq(t) - JsRcquest (Subsort (t));
IsTlnd(t) - Is Indication (Subsori (t));
endtype (*TSPBasicC!a$$ifiers *)
Г__________________—__
S.4.2.2 Вспомогательная классификация
TDATA AtomSubsort вводит дальнейшую классификацию элементарных составляющих примитивов данных, а именно октеты данных пользователя и ограничители СБДТ. Однако в данной спецификации эти составляющие не специфицированы.
Примечание — Единственная причина Представления TDATAAtomSub-sort в этом описании состоит и том. что таким способом тип данных TransporlServicePrimmve допускает консервативное расширение, при котором можно ввести более изящное неэлемемгариос представление примитивов данных Такое расширение необходимо в формализованном описании транспортного протокола для правильной формулировки требований, связанных с сегментацией и управлением потоком.
Булева функция Terminates, определенная в TSPClassifiers, связывает элементарное выполнение примитивов данных, что характерно для определения услуг. с не элементарным их выполнением, присутствующим в формализованном описании протокола.
3 Зак. 363
9
FOCI P ИСО МЭК TO 10023-93
type TDATAAtomSubsort
is FourTuplet renamedby wtnamw
TDATASubsort for Tuplet opnnames
TDATAOCT request for TheOne
TDATAOCTindication tor TheOther
TEOTrequest for TheThird
TEOTindication for TheFourth
endtype (• TDATAAtomSubsort •)
type TSPCIassifiers
is TSPBasicClassifiers, TDATAAtomSubsort opus
Terminates : TDTASubsort, TSP —> Bool e-qns forall
•I : OctetString, s : TDTASubsort, t : TSP ofsort Bool
TEOTrequest Terminates TDTreq(d> =tme;
TEOTindication Terminates TDTind (d) «true;
TEOTrequest Terminates TDTind(d) = false;
TEOTindication Terminates TDTreq (d) = false;
TDATAOCTrequest Terminates t = false;
TDATAOCTindication Terminates t = false; not(lsTDT(t)) => Terminates t = false;
endtype (* TSPClassiflers •)
8.4.3 Функции сервисных примитивов транспортного уровня
8.4.3.1 Общее описание
В 84.3.2 конструкция, представленная в 8.4.2, расширяется функциями, допускаклцнмн определение значений конкретных параметров TCP. В 8.4 3 3 в эту конструкцию добавляются булевы равенства. В 8.4.3.4 представлены дальнейшие функциональные расширения, которые полезны для представления согласования (см. 11.3.2) и педетермилизма поставщика услуг (см. 12.3.3).
8.4.3.2 Селекторы параметров сервисных примитивов транспортного уровня
Для сравнения или селекции значений конкретных параметров TSP определены булевы функции. Причина для такого непрямого представления — неполнота определения при помощи равенств.
10
ГОСТ Р ИСО МЭК ТО 10023—03
Единственное исключение имеется в прямом представлении параметра данных пользователя при помощи функции UserData, так как этот параметр можно определить во всех TSP.
type TSPParameteTSelectors
is TSPClassifiers
opns
-IsCalledOf-, -IsCallingOf-, -IsRespondingOI- : TAddress, TSP —>Bool
-IsTEXOpiionOf-r TEXOption. TSP
-IsTQOSOf- :TQOS. TSP
-IsReasonOL : TDISReason,
UserData : TSP
—> Bool
— > Bool
TSP -> Bool
—> OctetString
eqns
fora 11
a, al, a2 : TAddress. x, xI, : TEXOption, q. ql : TQOS, d : OctetString, r, rl : TDISReason, t : TSP, clq. clql : C1Q0S
of sort Bool
a IsCalledOf TCONreq(al, a2, x, q, d)«a eq al;
a JsCalledOI TCONind(aI, a2, x, q, d) = a eq al;
a IsCalledOf TUDTreqfal, a2, clq, d)~a eq al;
a IsCalledOf TUDTfnd(a!, a2, clq, d) —a eq al; not(IsTCONl(t)) -> a IsCalledOf t = false;
a IsCallingOf TCONreq (a 1. a2, x, q, d)« a eq al;
a IsCallingOf TCONind(al, a2, x, q, d) — a eq al;
a IsCallingOf TUDTreq(al, a2, clq. d)«a eq al; a IsCallingOf TLDTind(al, a2, clq, d)«a eq al; not(IsTCONl (t)) »> a IsCallingOf I — false; a IsRespondingOI TCONrespfal, x, q, d) «a eq al; a IsRespondingOI TCONconffal, x, q. d)=a eq al; not (I$TCON2(t))) => a IsRespondingOf I»false;
x IsTEXOptionOf TCONreq(aI. a2. xl, q, d) = x eq xl
x IsTEXOptionOf TCONind(ai, a2, xl. q, d)=x eq xl x IsTEXOptionOf TCONrespfa, xl, q. d) = x eq xl x IsTEXOptionOf TCONconffa, xl, q. d)=x eq xl notUsTCON(t)) => x IsTEXOptionOf t“false;
q IsTQOSOf TCONreq(al. a2. x. ql. d)=q eq ql q IsTQOSOf TCONindfaL a2. x, ql. d)=q eq ql q IsTQOSOf TCONrespfa, x. ql. d) = q eq ql q IsTQOSOf TCONconffa. x. ql, d)-q eq ql not(lsTCON(t)) -> q IsTQOSOf t-false;
11
ГОСТ Р ИСО МЭК ТО 10023-9»
г IsReasonOf TDISindl rl. d) = г eq rl: notllsTDISind(t)) => r IsReasonOf t = falsO; clq JsCIQOSOf TUDTreq(al, a2. dql. d)=clq eq clql clq IsClQOSOf TUDTind(al, a2, clql, d)=c!q eq clql ofsort OctetString
UserData(TCONreq(al, a2, x, q. d))—d;
UserDatafTCONind (al, a2. x. q.d))=d;
UserData (TCON resp (a, x, q, d})=d;
UserData (TCONconf (a. x, q, d))=d;
UserData (TDTreq (d)) = d;
UserDat a (TDTind (d)) = d
UserData (TEXreq(d)) =d:
UserData (TEXind (d)) =d;
UserData (TDISreq(d)) =d
UserData(TDlSind(r, d))-d;
UserData (TUDTreq (al, a2, clq, d)) =d;
UserDa(a(TUDTind(al. a2, clq. d))-d;
endtype (* TSPPara melerSeJectors *) сг..........................................
8 4.3.3 Равенство сервисных примитивов транспортного уровня
Булево равенству на TSP определяется как конъюнкция равенства имени TSP (см. 8.4.2.1> и попарного равенства параметров TSP Кроме того-, для примитивов данных требуется равенство ограничителя (см. 8.4.2 2).
----------------------------------------------------------#) type TSP Equality
is TSPParanieterSelectvrs opns
_.eq_. ne .,-eqTerm_: TSP. TSP —> Bool eqns forall
a, al. a2. a3 : TAddress. x. xl : TEXOption, q. ql : TQOS, d, dl ; OctetString. r, rl : TDISReason, t, tl : TSP.
clq. clql : CIQOS
ofsort Bool
Subsort(t) ne Subsort(tl) => t eq tl —false;
TCONrcq(a, a2, x, q. d) eq TCONreq(al, a3, xl, ql, dl) = (a eq al) and (a2 eq a3) and (x eq xl) and (q eq ql) and id eq dl);
TCONind(a, a2, x, q,d) eq TCONind(al, a3, xl.ql, dl)-
12
ГОСТ Р ИСО И ЭК ТО 10023-93
(a eq а I) and (а2 eq аЗ) and (х eq xl) and (q eq q I) and (d eq dl):
TCONresp(a. x. q, d) eq TCONresp(a 1, xl. ql. dl) = (a eq al) and (x eq xl) and (q eq ql) and (d eq dl);
TCONconffa, x. q. d) eq TCONconlfa I, xl, ql. dl)» (a eq a 1) and (x eq x 1) and (q eq ql) and (d eq dl);
TDIStnd(r, d) eq TDISind (rl. dJ) = (r cq rl) and (d cq dl); TUDTreq(a. a2. clq. d) eq TUDTreq(al, a3. clql, dl)» (a eq al) and (a2 eq a3) and (clq eq clql) and (d eq dl); TUDTindfa, a2. clq, d) eq TUDTind(al. a3, clql, dl) = (a eq al) and (a2 eq a3) and (clq eq clqI) and (d eo dl); not (IsTCON (I) or IsTDlS(t)) = > t eq 11
= (Subsort (t) eq Subsort (tl)) and (UserDataO) cq UserData(tl)) and (IsTDT(t) implies (t eqTerm II);
t ne tl -*»not(t eq tl);
I cqTertn 11
= TEOTrequest Terminates t ill (TEOTrequest Tepminates tl) and (TEOTindication terminates t iff (TEOTindication Terminates II));
endtype (* TSPEquality *)
Г________._
843.4 прочие функции сервисных примитивов транспортного уровня
Функция ProviderGeneratedlnd характеризует TSP, генерируемые исключительно поставщиком услуг. Эта функция используется для описания возможного недетерминизма поставщика услуг (см. 12.3.3).
Функция IsIndicationOf связывает выполнение TSP в каждом оконечном пункте- транспортного соединения с предварительным выполнением соответствующего примитива в другом пункте того же самого транспортного соединения (см. 12.3.3). Эта функция также представляет требования по согласованию в отношении возможного иедетерминизма поставщика услуг (см. раздел 10 я 14.2 ИСО 8072).
type TransportServicePrimitive is TSPEqualiiy
■opns ProviderGeneratedlnd : TSP —> Bool
- IsIndicationOf _,_IsValidTCON2For_: TSP. TSP -> Bool
33
ГОСТ Р ИСО МЭК ТО >0023-93
eqns (oral!
1,11 : TSP, a, al, а2, аЗ : TAddress, х, xl : ТЕХОрНол, q. ql : TQOS. d. dl : OcldSMng, clq, clql : CIQOS
ofsort Bool
PrividerGeneratedlnd(t)
= IsTDlSind(i) and (Provider IsReasonOf (t) and (UserData(t) eq O);
TCONconRat. xl, ql, dt) IsVakdTCON2For TCONreq(a, a2, x, q, d) —(al eq a) and (ql eq q) and ((xl eq UseTex) implies (x eq UseTEX));
TCONresp(al, xl, ql, dl) UValidTCON2For TCONind(a, a2. x. q, d) = (al eq a) and (ql eq q) and ((xl eq UseTex) implies (x eq UscTEX));
not ((IsTCONconf (t I) and IsTCONreq(t)) or ((IsTCON-resp(tl) and IsTCONind (i))) = > 11 lsValidTCON2For t^ false;
TCONind(al. a3. xl, ql, dl) IsIndicationOf TCONreq (a. a2. x. q. d)=»(al eq a) and (a3 eq a2) and (x! eq x) and (ql к q) and (dl eq d};
TCONconf(al, xl, ql, (11) IsIndicationOITCONrMpta, x. q. d) = (al eq a) *nd (xl eq x) and (ql eq q ) and (dl eq d); IsTCON (t), not(IsTReq(t)) => tl IsIndicationOf t-false; IsTCON(1). IsTReqtf). h(Subsort(U)) ne Succ(h(Sub-sort (t).)) =>fl IsIndicationOf t = Ialse;
TUDTind (a!. аЗ. clql, dl) IsIndicationOf TUDTreqfa, a2. clq, d) = (al eq a) and (a3 eq a2) and (clql 1c clq) and (dl eq d);
not(IsTCON(t) or IsTUDT(())=> tl IsIndicationOf t — IsTReq(t) and IsTInd(tl) and (h (Subsort (41)) eq Succ(h(Subsortft)))> and ((TEOTindication Terminates tl) iff (TEOTrcquest Terminates t)) and (UserDataft!) eq User Data (t)>;
endtype (* TransportServiccPrimitive •)
8.5 Качество услуг (КУ)
8 5.1 Общее описание
Структура рараметра КУ подразделяется в соответствии с определением, приведенным в разделе 10 ГОСТ 34 960
Первая декомпозиция выделяет параметры КУ: производительность ТС, приоритет ТС и зашита ТС. Эти структуры определяют-
14
ГОСТ Р ИСО МЭК ТО 10023-93
ся в 8.5.2—8.5.4 соответственна и ссылаются на вспомогательные определения КУ, приведенные в 8.5 5.
Как конструкция TQOS, так и конструкция ТС Per forma псе. а также их подструктуры в основной состоят из декартова произведения, образованного функциями проекции, каждая нз которых лает один .множитель значения произведения и булевых Функций. специфицирующих равенство и частичное упорядочение КУ, как определено в разделе 10 ГОСТ 34 960
В 8-5.2 г виде пояснения представлены видовые произведения, относящиеся к производительности ТС.
Примечания
I Порядок, в которой представлены определения КУ. отличается от пор ял ха. продета военного в разделе 10 ГОСТ 34.960, что обеспечиввст группирование (в формальном контексте) сходных определений. что облегчает чтение.
2 Представление значений TQOS формально полное только для той области. которая оказывается необходимой. чтобы обеспечить абстрактную спеиифи-кайлю таких значений, как параметры TSP. и соответствующих требований по согласованию КУ (см. четвертый абзац раздела )0 ГОСТ 34.960) Дополнительные функции, позволяющие оценивать КУ при тесгировакил н примеры измерений не определены Оценка каким-либо образом КУ не связана с динамическими требованиями, представленными паетоящим формализованным отданием, так как семантика LOTOS абстрагируется от количественных аспектов, таких хак время и вероятности.
3 В настоящем описании не указано, является ли значение КУ абсолютным требованием пользователя или приемлемо также пониженное значение.
Структура параметров КУ режима-без-установления-соединения представлена в виде декартова произведения параметров TCTransitDelay, TCProtection. NCProbability и TCPriority.
-------------------------------------------------------------,} type TSQuality
is POThreeTuple actuatazedby TCPerformanee, TCPriority, TCProtection using sort names
TQOS for ThreeTuple
TC Performance- for Element
TCPriority for Elements
TCProtection for Elements
Bool for FBool
opnnames
TQOSPeriarmanc? for First
TQOSPriority for Second
TQOSProtection for Third
TQOS for Tuple
bndtype (* TSQuality *)
15
ГОСГ Р ИСОМЭК ТО 10023-93
type TSCIQuatity
is POFourTuple’aclualizcdby Cl.TransitDelay, TCProtection, Probability, TCPriority using sort names
Bool for FBool
CLQOS for FourTuple
CLTrans Delay for Element
TCProtection for Element?
Prob for Elements
TCPriority for Elemeni4 opnnames
CLQOSTransDelay for First
CLQOSProlection for Second
CLQOSProbabiHty for Third
CLQOSPrioritv for Fourth
CLQOS for Tuple
endtype (* TSCIQuality ")
Г______—
8.5.2 Параметры производительности
8.5.2.1 Общее описание
Параметры производительности, составляющие компонент параметрон КУ, имеют следующую структуру четверки:
TCPerformance- DelaysxFailuresxThroughput xPER. что представлено в данном ниже определении. Определения компонентов даны в 8.5.2 2—8.5.2.5.
Примечание — Вспомогательные определения КУ (см 8 5.5) полезны для понимания определений параметра производительности, содержащегося в 8.5 2 2—8.5 "25 При первом чтении настоящего стандарта рекомендуется сначала ознакомиться с 8.5-5.
---------------------------------------------------------------) type TCPerformance
is BasicTCPerformance opns
-It-, -Ie-, -gt_.
-ge . : TCPerformance, TCPerformance —> Bool eqns forall
d. di : Delays, f, fl : failures,’ t, tl : Throughput,r.
rl : TPRER, pf, pf! : TCPerformance ofsort Bool
Performance (d, f. t, r) le Performance (di, fl. tl, rl) = (d ge di} and (f ge fl) and (t le tl) and (r ge rl);
ГОСТ Р ИСО/МЭК ТО 10023-53
pf It pft = (pf le pfl) and notfpfl Ie pf);
pf eq pEl = (pf Ie pfl) and (pll le pt);
pf ne pf I = not (pf eq pfl);
pf ge pH = рП le pi;
pf gt рП = (р( ge pfl) and not(pfl ge pf);
endtype (* TCPerforman.ee *)
type BasicTCPerformance
is FourTuple actualizedby TCDelays, TCThraughput TCResidualErrorRate, TCFailureProbabilities using sort names
TCPerformance for FourTuple
Delays for Element
Failures Гог Element
Throughput for Elements
TPRER for Element4
Bool for FBoo)
opnnames
Performence for Tuple
Delays for First
Throughput for Second
RER for Third
Failures for Fourth
endtype (♦ BasicTCPerformance *)
85.2.2 Параметры задержки
Параметры задержки имеют следующую структуру тройки:
Delays- EstDelayxTransDclayxRelDeiay, где:
EsiDelay = Nat
TransDelay = Nat*
RclDelay = Nat2
EstDelay — вил параметра задержки установления ТС, который имеет линейную структуру (таким образом определена единственная взаимно однозначная проекция).
TransDei dy — вид параметра транзитной задержки, который имеет структуру четверки. Каждая проекция представляет транзитную задержку для отдельного направления передачи и скорости (а именно «максимальная» и «средняя», см. 10.3 ГОСТ 34.960). Это определение представлено как переименование вспомогательного определения, приведенного в 8.5 5.
RelDelay — нид параметра задержки освобождения, который имеет структуру двойки. Каждая проекция представляет задержку освобождения ТС для отдельного пользователя ТС (которому
4 Зак. 363
17
ГОСТ Р ИСОМЭК ТО 10023—«3
сигнализируется об успешном освобождении, см. 10.7 ГОСТ 34.960). Форма этого определения —экземпляр общего определения (приведенного в 8.5.5), полученный использованием в качестве актуального типа параметра Nat Represent tio ns, который определен в библиотеке типов данных LOTOS.
type TCDelays
is POThreeTuple actualized by TCEstablishmenlDelay, TransitDelay, TCReleaseDelay using
sortnames
Delays for ThreeTuple
EstDelay for Element
TransDelay for Element Rei De] ay for Elements Bool for FBool
opnnames
TCEstablishment for First
Transit for Second
TCRe lease for Third
DeJay for Tuple
endtype {* TCDelays *)
type TCEstablishmentDelay
is Nat Representations sorts
EstDelay
opns
EstDelay : Nat —>EstDelay
Time : EstDelay —> Nat
_eq., _ne-, -le-. -It-, -ge-, -gt_ : EstDelay, EstDelay
—> Bool
eq ns
forall
n, nl : Nat, e, fel : EstDelay
ofsort Nat
Time(EstDelay (n))» n;
ofsort Bool
EstDelay (n) le EstDelay(n I) * n le nl;
e It el = (e le el) and notfei le e);
e eq el = (e le el) and (el lee);
e ne el=not(e eq el);
e ge el =e] le e;
e gt e! = (e ge el) and not (el ge e);
)8
ГОСТ Р ИСО МЭК ТО 10023—S3
endtype (’ TCEslablishiiieiitDeday *)
type TransitDelay
is DTRaleDirecilonQOSPararneter renamedby
$0H names
TransDelay for DQOSP op n names
TransDelay for RDQOSP
endtype (* Transitbelay *)
type TCReleaseDelay
is PODoubleParameter aclualizedby NatRepresentations using sortnames
Nat for Element
Nat for Element?
RelDelay for Pair
Bool for FBooI opnnames
AtCalling for First
AtCalled for Second
RelDelay for Pair endtype (* TCRcleaseDelay *) type CLTransitDelay is NaiuralNumber renamedby sortnames
CLTransDelay for Nat endtype (•CLTransitDelay *) Г____________________________________________________
8.5.2.3 Пропускная способность
Параметры пропускной способности: имеют следующую структуру четверки:
Throughput” Nat*
---------------------------------—----------------—..... •) type TCThrough put
is DTRateDirectionQOSParameier renamedby sortnames
Throughput for RDQOSP
opnnames
Throughput Гот RDQOSP endtype (* TCThrouhput *)
19
ГОСТ Р ИСО МЭК ТО 30023—9)
8 5.21 Вероятность отказа
Параметры вероятности отказа имеют следующую структуру четверки:
Failures® Prob4
----------------------------------------------------,} type TCFailureProbabilities
is POFourTuple actualizedby Probability using sortnames
Prob for Element
Prob for Elements
Prob for Elements
Prob lor Element4 Bool for FBool Failure for FourTuple opnnames
TCEstablishmeni for First
Transfer for Second
TCResilience for Third TCRelcase for Fourth Failures for Tuple endtype (* TCFailureProbabilltes *)
8 5 2.5 Коэффициент необнаруженных ошибок Параметры коэффициента необнаруженных ошибок (КНО) имеют следующую структуру двойки: КНО = Prob2
Каждая проекция представляет КИО для отдельного направления передачи. Форма этого определения аналогична той. которая использована для задержки освобождения ТС (см. 8.5.2.2). но с другим типом актуального параметра, а именно Probability (см. 8.5.5). На самом деле. КНО определен в ГОСТ 3-4.960 как отноше-мне измеренных значений, а не как вероятность. Однако это ие имеет значения для образования типа, поскольку значения КНО (любая из двух проекций) и операции на КНО совпадают со значениями и операциями вероятности соответственно.
___________________________________________________________________„’)
type TCResidualErrorRate
is POPair actualizedby NaturaiNumber using sortnames
TPRER for Pair
Nat for Element
Nat for Element2
20
ГОСТ Р ИСО МЭК ТО 10023—93
Bool for FBool opn names
RER for Pair
Target for First
Minimum for Second endtype (* TCResidualErrorRate *)
8.5.3 Приоритет TC
При помощи переименования натуральных чисел уровни приоритета представлены как полностью упорядоченное множество. В ГОСТ 34.9&0 указано, что число уровней приоритета ограничено. Это также применимо к реализации типа данных NaluralNumbcr.
type TCPriority
is NaturalNumber renamedby
sortnames
TCPriority for Nat
opnnames
Lowest for 0
Higher for Succ
endtype (• TCPriority *>
Г______________________________________________
8.5.4 Защита TC
Упорядоченное множество и» четырех констант представляет варианты зашиты, определённые в 10.9 ГОСТ 34.960.
type ТС Protection
is OrderedFourTuplet renamedby
sort names
TCProtection for Tuple!
opnnames
NoProtection for TheOne
Monitoring for TheOther
Manipulation for TheThird
Full Pro tec: ion for TheFourth
endtype (• TCProtection *)
Г__________________________________________
8.5.5 Вспомогательные определения КУ
В тиле Probability вид Prob задает интервал действительных чи-
21
ГОСТ Р ИСО.М ЭК ТО 10023-93
сел [0. I] вместе с элементом Undefined, который представляет от-ношения, не входящие в этот интервал.
DTRateDireciionQOSParameter поддерживает определение пл Р а метра КУ в виде натурального числа, который имеет четыре компонента (или проекции). каждый из которых индексируется скоростью передачи данных и направлением передачи. Виды DTRatc и DTDirection обеспечивают эти индексы. Компоненты генерируются функцией Pro]. Конструкция этого типа представлена снизу-вверх. используя определения типов DTDirectionQOSPar к DTDirectionQOSParameter для построения структуры четверки ид двух двоек. Общее определение параметра PODoubleParameter см. в 8.7.
Примечание — Определение в 3.7 необходимо для понимания приведенных ниже определений. При первом «тении рекомендуется сначала прочесть в. 7.
type Probability
is NaturalNunnber sorts
Prob
ODOS
-J- : Nat. Nat —> Prob
Undefined : —> Prob
_eq_._ne_,_le_, -IL,..ge_^.gt_ : Prob, Prob —> Bool
eqns forall
ni. n, j, k : Nat, p. q : Prob ofsort Prob
mi gt n or (n eq 0) => m/n = Undefined;
in le n, n ne 0, j me 0 = > (m * j) / (n • j) =m/n; ofsort Bool
m le n. j le k, n ne 0. k ne 0 = > m / n le (j / k) = (m * k) le (J*n);
tn le n. n m 0 = > Undefined le (m/n) = false;
p le Undefined = true:
p It q=fp le q) and notfq le p);
p eq q = (p le q) and (q le p);
p ne q=not(p eq q);
p gc q-q le p;
p pt q— (p go q) arid itot (q ge p);
endtype (• Probability *]
ГОСТ Р ИСО'МЭК ТО 10023-93
type DTDirectionQOSPar
is POPair actualizodb) NaturalNumber using sorlnames
Nat for Element
Nat for Element
DQOSP for Pair
Bool for FBool opnnames
FromCalling for First
FromCalled for Second
DQP for Pair
endtype (* DTDirectionQOSPar *) type DTRateDireciionQOSParameter is POPair actualizedby DTDirectionQOSPar using sortnamfes
Nat for Element
Nat for Element2
DQOSP for Pair
Bool for FBool opnnames
FromCalling for First
FromCalled for Second
DQP jot Pair
endtype (• DTDirectionQOSPar *) type DTRatcDirectionQOSParameier is POPair actualizedby DTDirectionQOSPar using sortnames
DQOSP for Element
DQOSP for Element2
Bool for FBool
RDQOSP for Pair opnnames
Max for First
Ave for Second
RDQOSP for Pair
endtype (“ DTRaleD-rectionQOSParameter ♦)
8.6 Параметры сервисных примитивов транспортного уровня
Вариант срочных данных и параметры причины разъединения в TSP определяются типами TEXOption и TDISReason соответственно. Структура параметра КУ определена в 8.5 посредством
23
ГОСТ Р ИСО. МЭК ТО (0023-93
TSQuality. Другими типами параметрон TSP являются TAddress (см. 8.2) и OctetString (данные пользователя), которые импортируются из библиотеки типов данных LOTOS (см. раздел 7).
Примечание — Представление значений TDI Season соответствует опре-долепи» и М.2.1 ГОСТ 34.960, но без представления дополнительной информа-ини н примеров, приведенных в примечаниях (см. 87 для определения TwoTuplet).
type TEXOption
is TwoTuplet renamedby sortnames
TEXOption tor Tuplet opnnames
UseTEX for TheOne*
NoTEX tor TheOther
endtype (* TEXOption *)
type TDISReason
is TwoTuplet renamedby
sortnames
TDISReason for Tuplet opnnames
User for TheOne
Provider for TheOther
endtype (* TDISReason *)
(*__________________________________
87 Вспомогательные определения
General Identifier определяет бесконечное множество идентификаторов вместе с равенством на нем.
Element определен в библиотеке типов данных LOTOS, тогда как Elements. Elements и Element4 являются его отдельными изоморфными копиями. Эти типы используются в определениях Pair, ThreeTuple и FourTuple. которые определяют кортежи общего вн-ла из двух, трех или четырех значении, возможно разных видов, с равенством и проекциями TwoTuplet и FourTuplct определяют множества, состоящие соответственно из двух и четырех элементов, наделенных булевым равенством. OrderedFourTuplet является расширением FourTuplct с общим упорядочением.
POEIement — это общий тип Element с добавлением частичной упорядоченности, тогда как POEIement. POEIcment3 и POEIement4 являются его отдельными изоморфными копиями. Эти типы используются при построении POPair, POThreeTuple я
24
гост р исо мэк та 10023-93
POFourTuple. которые являются кортежами общего вида, расширенными частичной упорядоченностью.
----------------------------------♦ )
type Genera! Identifier
is Boolean sorts
Identifier
opns
Sorneldentifier : —> Identifier
Anotherldentifier : Identifier —> Identifier
-eq-., ne.. : Identifier. Identifier
—> Bool cons forall
a. al : Identifier
ofsort Bool
Sorneldentifier eq Someldentifier= true;
Anot her Identifier (a j eq Someldentifier-false;
Someldentifier eq Anotherldentifier(a) = false;
Anotherldentifier(a) eq Anotherldentlfier(al) =a eq al;
3 ne al = not(a eg al);
endtype (* Generalfdentifier •) type Element2
is Element renamedby
.sortnames
Element? for Element
endtype (* Element? *) type Elements is Element renamedby sortnames Elements for Element
endtype (• Elements *)
type Element4
is Element renamedby sortnames
Element4 for Element
endtype (• E)ement4 *) type Pair
is Boolean, Element. Element?
sorts
Pair
opns
25
ГОСТ Р ИСО/МЭК ТО 10023-93
Pair | : Element. Element? | —> Pair |
First | : Pair | —> Element |
Second | : Pair | —> Element2 |
cq , -ne- | : Pair, Pair | —> Bool |
eqns forall
el : Element, c2 : Element2. p. pl : Pair ofsort Element
First (Pair(rl. e2)—cl: ofsort Element
Second (Pair (el, e2))=e2; ofsort Bool
p = pl => p eq pl=truc;
First(p) ne First (pl) =>p eq pl = false:
Second (p) ne Second (pl) => p eq pl=falsfe;
p ne pl = not(p eq pl);
endtype (’Pair *) type ThreeTuple’ is Element, Element2, Elements. Boolean sorts
ThreeTuple opns
Tuple : Element. Elements, Element3 —> ThreeTuple
First : ThreeTuple —> Element
Second : ThreeTuple —> Elements
Third : ThreeTuple —> Elements
-eq-, _ne- : ThreeTuple. ThreeTuple —> Boot
cqns forall
x, у : ThreeTuple. xl. yl : Element, x2, y2 : Elements, x3. y3 : Elements
ofsort Element
First (Tuple(xI. x2. x3))-xl;
ofsort Element?
Second (Tuple(xl, x2, x3))=x2;
ofsort Elements
Third(Tuple(xl, x2. x3)) = x3;
ofsort Bool
First (x) eq First (y), Second (x) eq Second (y), Third (x) eq
Third(y) »>x eq y=True:
not (First (x) eq First (y)) ® > x eq у = False;
not (Second (x) eq Second (y)) ■»> x eq у» False;
not (Third (x) eq Third (y)) — > x cq у-False;
2G
ГОСТ Р ИСО'МЭК ГО 10023—93
endtype (* ThreeTuple *)
type FourTuple
is Element, Eiemen(2, Elements, Elements Boolean sorts
FourTuple
opns Tuple : | Element, Eteinent2, Elements, | Element4 |
—> FourTuple | ||
First | : FourTuple | —> Element |
Seco nd | : FourTuple | —> E!ement2 |
Third | : FoureTupEe | —> Elements |
Fourth | : FoureTupSe | —> Element4 |
_eq_, _ne | : FourTuple, FourTuple | —> Bool |
eqns
forall
xl. yl : Element. x2, y2 : Element2, x3. y3 : Elements, x4, y4 : Element?
ofsort Element
First (Tuple (xl. x2. x3, x4))-xl;
ofsort Elements
Second (Tuple(xl. x2, x3. x4))«=x2;
ofsort Elements
Third (Tuple (xl. x2. x3. x4)) =x3;
ofsort Elements
Fourth (Tuple (xl. x2, x3, x4))=x4;
ofsort Bool
Tuple(xl, x2. x3, x4) eq Tuple (xl, x2, x3, x4)—Truc;
xl ne yl »■> Tuple(xL x2. x3. x4) eq Tuple(yl, y2. y3. y4) -False;
x2 ne y2 => Tuplc(xl. x2. x3, x4) eq Tuplfe(y1, y2. y3, y4) = False;
x3 ne y3 => Tuple(xI. x2. x3, x4) eq Tuple(y1, y2, y3, y4) = False;
x4 ne y4 = > Tuplefxl, x2, x3, x4) eq Tupkfyl, y2, y3, y4)
-False:
endtype (• FourTuple *)
type TwoTuplet
is Boolean, Natural Number sorts
Tuplet
opns
TheOnc. TheOther : —> Triplet
_eq_, -ne- : Tuplet, Tuplet —> Bool
h : Tuplet —> Nat
ГОСТ Р ИСО.’МЭК ТО 10023-83
eqns forall u, v : Tuplet
ofsort Nat
h (TheOne) =0;
h (TheOther) - Succ (h (TheOne)); ofsort Bool
u eq u-h(u) eq h(v);
u ne v—not (u eq v);
endtype (* TwoTuplet *) type FourTuplet is TwoTuplet opns
TheThird. TheFourth : —> Tuplet
eqns ofsort Nat
h (TheThird) - Succ(h(TheOther));
h(TheFourth) ~Succ(h(TheThird));
endtype (• FourTuplet •) type OrdcrcdFourTuplet is FourTuplet
Opns
_lt_, -Ie-. _ge_,
-gt- : Tuplet, Tuplet — > Bool eqns forall
x, у : Tuplet ofsort Bool
x It y = h(x) It h(y);
x Ie y=h(x) Ie h(y);
x ge y=h(x) ge h(y);
x gt y=h(x) gt h(y);
endtype (* OrderedFourTuplet *) type POEIement is Element formalopns
-Ie-, _lt_. ge..
_gt_ : Element, Element —> FBool endtype (• POEIement ') type POEIemenl2 is POEIement rtenatnedby sort names
Elements for Element
28
ГОСТ Р ИСОМЭК ТО 10023- 93
endtype (* POEIement2 *)
type POElement3
is POElement renamedby sortnames
Elements for Element
endtype (* POEiement3 *)
type POEIement4
is POElement renamedby sortnames
Element4 for Element
endtype {* POElement4 *)
type BasicPOPair
is Pair actualizedby POElement, POE1ement2 using
endtype (• BasicPOPair ")
type POPair
is BasicPOPair opns
-le.-, -It-, -ge-,
-gt- ; Pair, Pair —> Bool:
eqns forall
x. у : Pair
ofsort Bool
First(x) le First(y). Second(x) le Second(y) = >x le y = true;
not (First (x) le First (у)) —> x le у * false;
not (Second (x) le Second (y)) ••> x le у=false;
x ne у — > x II y^x le y;
x eq у "> x It у = false;
x ge у« у le x;
x ne у = > x gt y=x ge y;
x eq у = > x gt у = false;
endtype (* POPair *)
type BasicPOThreeTuple
is ThreeTuple actualizedby POElement. POEiement2, POElement? using
endtype (* BasicPOThreeTuple *)
type POThreeTuple
is BasicPOThreeTuple opns
_le-, -It-, -ge_. _gt_ : ThreeTuple, ThreeTuple —> Bool eqns forall
29
ГОСТ Р ИСОГМЭК ТО 10023-93
х, у : ThreeTuple ofsort Bool
First(x) Ie First (у). Second (x) le Second(y), Third(x) le Third (y) => x le y=true;
not (First (x> le First (y)) => x le y = false;
not (Second(x) le Second (y)) = > x le у— false;
not (Third (x) le Third (y)) ->x ley-false;
x ne у = > x It y-x le y;
x ge y=y le x;
x ne у = > x gt y = x ge y;
endtype (* POThreeTuple *)
type BasicPOFonrTuple
is FourTuple actualizedby POEIement, POElement2, POElement3, POElemenU using
endtype (• BasicPOFourTuple *)
type POFourTuple
is BasicPOFourTuple opns
_le_, -It-, -ge_,
-gt- : FourTuple, FourTuple —> Bool af* forall
x, у : FourTuple ofsort Bool
First(x) le First(y), Second(x) le Second(y). Third(x) le Third(y), Fourth(x) le Fourth (y) "> * le у—true;
not (First (x) le First (y)> => x le у— false;
not(Second(x) le.Second(y)) —> x le у— false;
not (Third (x) le Third(y)) = > x le у = false;
not (Fourth (x) le Fourth (y)) => x le у— false;
x ne у — > ж It y-x le y;
x 2е у—у ie x;
X ne у => x gt y-x ge y;
endtype (* POFourTuple *)
9 ГЛОБАЛЬНЫЕ ОГРАНИЧЕНИЯ
Определение поведений поставщика услуг разделено на две независимые части: поставщик услуг и режиме-с-установленнеи-соединения и поставщик услуг в режимебез-установления-соедн-исния. Определение поставщика услуг в режиме-с-установлснием-соединения представлено в сочетании с отдельными ограничения-
30
ГОСТ Р ИСО/МЭК ТО I0023-W
ми. TConnections описывается как способный поддерживать потенциально бесконечное число независимых ТС. Каждое ГС представляется отдельным экземпляром TConnection. Получаемая в результате структура показана на рисунке J. TConnectionkss описано н разделе 16. В разделе 10—15 описаны ограничения, относящиеся к транспортным услугам в режлме-с-установленисм-сосди-нения.
Рисунок 1 — Структура услуг транспортного уровня
Примечания
I Каждый экземпляр ТСояпесНоп может закончиться. Общий TConnections никогда яс может закончиться, поскольку всегда существует вероятность того, что будет вызван новый экземпляр его компонента TConnection.
2 В любой момент времени может быть активно любое число ТС. Недетер-мннизм поставщика услуг в ограничении этой потенциально бесконечной параллельности специфицируется как отдельное ограничение (см. раздел 14).
behaviour
TSConnectionless [t]
HI
TConnections [tj || TCIdeniification (t] ||
TCAcceptance |t]
TBackpressure[t]
where
process TConnections [t] : noexit : =
31
ГОСТ Р ИСО/МЭК ТО 10023-93
TConnection [t] >> stop
III
TCon nations [l] endproc (* TConnections *1 (*________________________________________________
10 ОБЕСПЕЧЕНИЕ ТРАНСПОРТНОГО СОЕДИНЕНИЯ
Требования к поведению поставщика услуг, связанные с обеспеченней одного ТС, распадаются на два класса, а именно ограничения, которые являются локальными для оконечной точки ТС, и межоконечные ограничения. Ограничения первого класса связаны с поведением в оконечной точке ТС в зависимости от истории примитивов, выполненных в этой же оконечной точке ТС. Ограничения второго классе связаны с поведением в оконечной точке ТС в зависимости от истории примитивов, выполненных в другой оконечной точке ТС.
Следует формально определить подходящее понятие «история». В частности, удобно принимать во внимание только те события, которые могут влиять на будущее поведение поставщика услуг, не учитывая, таким образом, те события, которые ни на что больше не влияют: такое понятие известно как «влияющая история». Для локальных ограничении влияющая история представлена состоянием процесса в соответствии с диаграммой переходов состояний, представленной на рисунке 5 ГОСТ 34.960. Для межоконечных ограничений влияющая история представлена параметрами процесса, чья структура и операции формулируются при помощи специально созданного определения типа данных (см. 12.3.2). Эти операции позволяют формулировать требования, соответствующие таблице 1 и рисунку 4 ГОСТ 34.960, способом, не зависящим ог модели.
Локальные органнчения представлены двумя независимыми параллельными процессами, представляющими собой два разных экземпляра процесса ТАЕР (см. раздел 11) м соответственно'ограничивают взаимодействия с вызывающим и вызываемым пользователями транспортных услуг. TSUserRole определяет роли вызывающего и вызываемого пользователя транспортных услуг, Межоканеч-лые ограничения представлены процессом TCEPAssociation (см. раздел 12). который соотносит индикации, возникающие на каждом конце ТС. с соответствующими запросами, возникающими на другом конце ТС. TSPDirection определяет направления примитивов запроса и индикации в полном соответствии с разделом 5.
32-
ГОСТ Р ИСО МЭИ ТО 10023-93
Этим процессом специфицируется недетерминированность поставщика, которая влияет на данную взаимосвязь. Кроме того, TCEPAssooiation определяет лелетерминнзм, связанный с выполнением примитивов, генерированных поставщиком.
Примечание — Техническое замечание о завершении: завершение обоях процессов, представляющие концы соединения — явно достаточное представление конца времени жизни этого соединения Вот почему параллельный хамке-цент, содержащий TCEPAssocia tion. описан (с использованием конструкции [> exit) как способный завершиться в любой момент времени, тогда как TCEPAwociation — бесконечный процесс.
----------------------------------------------- Ч type TSUserRole
is TwoTuplet renamedby sori names
TSUserRole for Triplet
opnnames
CaJiingRolc for TheOne
CalledRole for TheOther
endtype (* TSUserRole *)
type TSPDirection
is TwoTuplet renamedby .sortnames
TSDirection for Tuplet
opnnames
Request for ThcOne
Indication for TheOther
endtype (♦ TSPDirection *)
process TConnection ft} : exit: —
(TCEP [(] (CallingRole) ||| TCEP [t] (CalledRole))
II
(TCEPAssaciation [t] [> exit)
endproc (* TConnection *)
Il ЛОКАЛЬНЫЕ ОГРАНИЧЕНИЯ ДЛЯ ОКОНЕЧНОГО ПУНКТА ТС
11.1 Общее описание
Первые три промесса следующей декомпозиции локальных ограничений на взаимодействия одного ТС в каждой оконечной точке отражают структуру события: это делается с целью отделения ограничений, применяемых к каждому компоненту структуры события,.от ограничений, применяемых к другим компонентам. Четвертый процесс специфицирует ограничение, упомянутое в приме нанки к $.4.1.
33
ГОСТ Р ИСОМЭК ТО 10023-93
process TCEP ft] (role : TSUserRoJe) : exit : —
TCEPAddress ft]
11 TGEPIdentilication It)
( | TCEPSPOrdering [t] (role)
1 | TCEPUserData [t] endoroc (* TCEP *)
‘______________________________________
11.2 Адрес и идентификация оконечной точки Т С
Локальные ограничения на адресную и иденгификаторную части событий в оконечноГт точке ТС имеют сходную форму: значение определяется при первом событии совместно с пользователем транспортных услуг, а затем остается постоянным.
Примечание — Завершение обоих процессов допускается в любой момент времени: конек локального (т е. в оконечной точке ТС) времени жизни ТС: на самом деле определяете и локальным упорядочением сервисных примитивов (см 1Г.З I).
process TCEPAddress [t] : exit: =
Pia : TAddress ?tcei : TCEI ?tsp : TSP ; ConstantTA [t] (ta)
[> exit
endpr-oc (* TCEPAddress *)
process ConstantTA (t] (ta : TAddress) : noexit: =
Uta ?tcei : TCEI ?tsp : TSP ; ConstantTA [t] (ta)
endproc (* ConstantTA *)
process TCEP Identification [t] : exit : =
(?ta : TAddress ?tcei : TCEI ?tsp : TSP ; ConstantTCEl [t] (tcei) |> exit
endproc (* TCEPIdentification •)
process ConstantTCEl [t] (tcei : TCEI) : noexif: = t?ta : TAddress Itcei ?tsp : TSP ; ConstantTCEl [t] (tcei) endproc (“ ConstantTCEl *)
I*______________________________________________________
11.3 Локальное упорядочение сервисных примитивов и оконечном пункте ТС
11.3 I Ованес описание
TCEPSPOrdering определяет ограничения на возможные последовательности примитивов в одном оконечном пункте ТС (см. рисунок 5 и таблицу 4 ГОСТ 34 960), применяемые к одному ТС.
34
ГОСТ Р ИСО/МЭК то 10023—03
Поскольку задала спецификация локальных ограничений, постольку и любой момент времени примитивы транспортных услуг, которые могут быть выполнены, зависят только от истории примитивов, выполненных в этом оконечном пункте ТС. Влияющие аспекты этой истории в основном представлены ниже в именах процессов из компонентов TCEPOrdering вместе с некоторыми параметрами.
Фаза установления ТС в оконечном пункте ТС представлена в виде последовательности TCEPConnectl и TCEPConnect2. Это сделано для возможного освобождения ТС даже до успешного установления ТС (предотвращая его таким образом), во только после начала времени жизни ТС. Примитив Т-СОЕДИНЕНИЕ, выполненный в TCEPConnectl, является влияющей историей для TCEPConnect2, поскольку к Т-СОЕДИНЕНИЕ ответ/подтвержде-ние применимы ограничения согласования, которые зависят от Т-СОЕДИНЕНИЕ индикацня/запрос.
Успешное установление ТС позволяет войти в фазу передачи информации, которая в каждом оконечном пункте ТС представлена TCEPDataTransfer. Поведение в этой фазе не зависит от роли оконечного пункта ТС. Значение х сообщает результат согласования варианта срочных дал них.
Освобождение ТС в оконечной точке ТС состоит из выполнения примитива Т РАЗЪЕДИНЕНИЕ, как представлено в TCEPRelease. Это может произойти в любой момент времени после первого примитива Т-СОЕДИНЕНИЕ.
Примечание — Последняя альтернатива в определении TCEPSPOrdc ring введена для обеспечения возможности завершении установления ТС путем освобождения ТС локально в вызывающем оконечном пункте ТС, без выполнения каких-либо примитивов на другом (.потенциально, ио в действительности никогда же наблюдаемом) конце этого ТС.
• а«аа^»*а а аа»»а а амаааа^аах а • ч I — — ■ ч а а **а.а«аа ааа а .а»»»а»а»»ааа«»«»»ааа»а«» ■ ааа а о ।
process TCEPSPOrdering [t] (role : TSUserRole) : exit : = (TCEPConnecti [t] (role) » accept tsp : TSP in
(TCEPConncct2 [tj (tsp) » accept x : TEXOption in TCEPDataTransfer [tl (x))
[> TCEPRelease [t])
[ ] [role—CaltedRole] —> exit endproc (* TCEPSPOrdering *) (*
EI.32 Физа установления соединения в оконечном пункте ТС
В 8.4.3.4 дано определение булевой функции lsValidTCON2For,
35
ГОСТ Р И СО, МЭК ТО IM23-93
которая представляет требования согласования транспортных услуг. Определение TSL’serRole дано в разделе 10
-------------------------------------------.)
process TCEPConnecl! [t] (role : TSUserRole) : exit(TSP) : — [role—CallingRok]
t?ta : TAddress ?tcei : TCEI ?tcr : TSP [IsTCONreq(tcr) and (ta IsCallingOf ter)] ; exit (ter)
{role-= Called Role]
t ?ta : TAddress ?tcei : TCEI ?tci : TSP (IsTCONind(tci) and
(ta IsCalledOf tci)| ; exit (tci)
endproc (* TCEPConnecti *)
process TCEPConnect2 [t| (tel : TSP) : exit(TEXOption) :-
t ?ta : TAddress ?tcei : TCEI ?tc2 : TSP [tc2 IsValidTCON2For tel]; (choice x : TEXOption [ | [x IsTEXOptionOf tc2] -> exit (x))
endproc (* TCEPConnect2 *)
11 3.3 Фаза передачи данных в оконечном пункте ТС
----------------------------------------------ж)
process TCEPDataTransfer [t] (ж : TEXOption): noexit : = TCEPNormalDataTransfer ft]
h = UseTEX] -> TCEPExpeditedDataTransfer ft]
endproc (♦ TCEPDataTransfer *)
process TCEPNormalDataTransfer ft) : noexit : —
t ?ta:TAddress ?tcei : TCEI ?tsp : TSP [IsTDT(tsp)] ;
TCEPNormalDataTransfer [t]
endproc (* TCEPNormalDataTransfer *)
process TCEPExpeditedDataTransfer ft] : noexit : =
t ?ta : TAddress ?tcei : TCEI ?tsp : TSP [IsTEX(tsp)] ;
TCEPExpeditedDataTransfer ft]
endpfoc (" TCEPExpeditedDataTransfer *)
_________________________
11.3.4 Фаза освобождение в оконечном пункте ТС -------------------------ж)
process TCEPRelease [t] : exit : =
t ?ta : TAddress ?tcei : TCEI ?tsp : TSP (IsTDIS(tsp)] ; exit.
36
ГОСТ Р ИСО МЭК ТО 10023—93
tndproc (* TCEPRelease *)
С________________________________________________________________
11.4 Ограничения на данные пользователя
Длина параметра данных пользователя в примитивах транс* портных услуг ограничивается TCEPUserData, что изложено в 12.2.7; 13.1.13; 13.2.3 и 14.2.2 ГОСТ 34.960. отражаемых здесь.
..... ) process TCEPUserData ft] : exit : —
t ?ta : TAddress ?tcei : TCEI ?tsp : TSP [IsValidUserData (tsp)] ;
TSEPUserData [t] [ ] exit
endproc (* TCEPUserData •)
type ValidUserData
is TranspartServicePrimitive opns
IsValidUserData : TSP -> Bool
eq ns forali t : TSP ofsort Bool
IsTCON(t) => IsValidUserData (t) — Length(UserData(t)) le NatNum(34-Dec(2));
IsTDT(t) => IsValidUserData (I) - Length (UserData(t)) gt 0; IsTDlS(t) -> IsValidUserData(t) — Length (UserData (t)) le NatNum(6 + Dec(4));
IsTEX(t)
= > IsValidUserData (t)
-Length(UserData(t) gt 0) and (Length(UserData it)) le NutNum (llDec(6)));
endtype (• ValidUserData *)
(*__________
t2 МЕЖОКОНЕЧНЫЕ ОГРАНИЧЕНИЯ ДЛЯ ОДНОГО ТС
12.1 Общее описание
После выполнения первого запроса TCEPAssociation расщепляется на два экземпляра TAssocI — по одному экземпляру на каждое направление передачи. Эти два экземпляра могут быть созданы независимо и параллельно, поскольку они образуют отдельные части поведения. В самом: деле, когда бы один из них ни вызывал взаимодействие, другой не будет вовлечен в это взаимодействие.
37
ГОСТ Р ИС0.М9К ТО 10023—И
Примечание2 — Начальных взаимодействием по ограничениям может быть только запрос. Это должен быть Т-СОЕДИНЕНИЕ запрос в силу дополнительных локальных ограничений (см 1132г Разделение между двумя экземплярами корректно только в том случае, если гарантируется, что оконечный пункт, где одни нз них обрабатывает запросы, является оконечным «ункгри. где другой обрабатывает индикации, По этой причине введены параметры адреса. идентификации и направления примитивов з TAssocI (см. 12.2). при помощи которых TAssocI обрабатывает запросы на одном конце ТС и индикации на другом конце.
process TCEPAssociation [ij : noexit : —
t ?ta : TAddress ?tcei : TCEI ?tcr : TSP f IsTReq (tcr)J ;
(TAssocI [t] (ta, tcei, Request, Indication, Append (ter, NoTReqs))
III
TAssocI [t] (ta. tcei. Indication, Request. NoTReqs)) endproc (* TCEPAssociation ") (*___________________________________________________________
12.2 Однонаправленность
TAssocI соотносит индикации, которые могут выполняться на одном конце ТС, с историей запросов, выполненных на другом его копие, учитывая недетерминизм поставщика, влияющий на эту взаимосвязь. Самым сложным подпроцессом TAssocI является TCRecToInd (см. 12.3.1), который представляет межоконечные ограничения, указывающие взаимодействия в t, связанные с примитивами. Параметр TCRecToInd представляет историю запросов, которые соотносятся с возможными будущими индикациями. Определение TCEPHalf. видимо, требует небольшого дальнейшего пояснения: см. в 31.2 ConstantTA и ConstantTCEI, в $.4.2.1 IsTReq и IsTlnd. в 8.3 ТЫ.
--------------------------------------------------*) process TAssocI [tj (ta : TAddress, tcei : TCEI, dJ, d2, :
TSPDirection, rh : TReqHistory) : noexit : «
( (TCEPHalf [tj (dl) H ConstantTA [t] (ta) || ConstantTCEI [t] (tcei>)
III
TCEPHalf ft] (d2)
t?lal : TAd dress? tcei : TCEI ?tsp : TSP irid(tal, tceil) neTIdtta. tcei)] ; (ConstantTA (tj (tai) || ConstantTCEI [t] (tceil))) | | TCReqToInd [t] (rh) endproc (* TAssocI *)
process TCEPHalf [t] (dir : TSPDirection) : noexit : —
38
ГОСТ Р ИСОМЭК ТО 10023—93
[di г» Request]
~>(?ta : TAddress ?tcei : TCEI ?tsp : TSP (IsTReq(tsp) J ; TCEPHalf t] (dir)
dir = Indication]
— > t?ta : TAddress ?tcei : TCEI ?tsp : TSP (JsTInd(tsp)] ; TCEPHalf
It] (dir)
endproc (* TCEPHalf *)
(*_____________________________________________
12.3 Межоконечный недете p м к н и з м
12.3.1 Общее описание
Как было сказано выше, TCReqToInd параметризуется историей запросов rh, выполненных на одном конце, которые могут влиять на возможные будущие индикации на другом конце. Значения вида TReqHi story являются основными последовательностями, на которых определены некоторые операции, позволяющие рассматривать только влияющие элементы истории (подробнее см. 12.3.2).
Непосредственная форма определения TCReqToInd — это очень простая праворекурсивная форма. В любой момент времени процесс TSPEvent специфицирует ограничения на следующее наблюдаемое событие; первый параметр TSPEvent — это основа представления недетерминизма (операция Tops- определена в 12.3.2). После выполнения этого события TCReqToInd выполняется с обновленным значением параметра.
process TCReqToInd [t] (rh : TreqHistory) : noexit :-TSPEvent ft) (Tops(rh>. rh) > accept rhl : TReqHistorv in TCReqToInd ft] (rhl) endproc (* TCReqToInd •)
12.3.2 Определение данных
Первое определение обеспечивает основную конструкцию историй примитивов запроса посредством операций NoTReqs (пустая история) и OnlopOf (для расширения истории более ранним’запросом) . Также введены еще несколько булевых функций с обычной интерпретацией.
Примечание — Ради полноты OnTopOf нужно определять также и для случаи, когда ее первый аргумент — индикация; и атом случае история остает-
26
ГОСТ ₽ ИСО,МЭК то 10023-93
ся бел изменения. Этот «безэффсктный» подход на индикации соблюдается также it во втором определении
Второе определение расширяет основной тип данных четырьмя операциями, необходимыми для формулировки межоконечных ограничений:
a) Reduce — описывает историю своего верхнего элемента (г. с. самого раннего по времени выполненного запроса)-
b) Remove — удаляет заданный запрос из заданной истории; если последний имеет далее много экземпляров, то удаляется первый экземпляр.
с) Append — добавляет запрос к истории в качестве последнего элемента. Заметим, что Append действует как OnTopOf, но с другого конца истории.
d) Tops — создает историю, состоящую из тех примитивов в аргументе истории, которые могут привести к последующей индикации.
Введены также другие функции, а именно TDISTops и TEXDJSTops, для выразительности определения. TDISTops н TEXDISTops дают непосредственные результаты для вычисления Tops.
В соответствии с таблицей 1 ГОСТ 34.960 определен следующий порядок значимости примитивов:
Т-ДАННЫЕ < Т-СРОЧНЫЕ-ДАННЫЕ
< Т-РАЗЪЕДИНЕНИЕ.
Т-СОЕДИНЕНИЕ < Т-РАЗЪЕДИНЕНИЕ, причем между примитивами одной услуги нет порядка значимости.
Tops определяется следующим образом: для любого данного значения rh. вила TReqHistory, Tops(rh) представляет собой последовательность запросов, которая:
а) содержит только запросы различных услуг, н
Ь) содержит запрос t тогда и только тогда, когда t содержится в rh и все запросы перед ним в rh (т. е. выполненные раньше по времени) являются ниже по значимости, чем t, и
с) сохраняет порядок запросов в rh.
-----------------------------......... ) type Tr ansportServiceBasicTSPRequest History
is TransportServicePrimitivc
sorts
TreqHistory opns
NoTReqs : —> TreqHistory
-OnTopOf- : TSP, TreqHistory —> TreqHistory
40
ГОСТ Р ИСО/МЭК ТО 10023-1*3
JsTopOL IsEmpty _cq,, «пе-
: TSP, TreqHistory —> Bool :. TreqHistory —> Bool : TRcqHistory. TRcqHistory —> Bool
eq n s (or all t. tl : TSP, h, hl : TRcqHistory ofsort TReqHistory
IsTlnd (t) => t OnTopOf h=h;
ofsort Bool
IsEmpty (NoTReqs) = true;
IsTReqh) => IsEmpty(t OnTopOf h)=falsc;
NoTReqs eq NoTreqs = true;
IsTReq(t) = > NoTReqs eq (t OnTopOf h)= false;
IsTReq(t) •> t OnTopOf h eq NoTReqs-3false;
IsTReq(t). IsTReq(tl)
“ > t OnTopOf h eq (tl OnTopOf hl> = (t eq tl) and (h eq hl);
n no hl = not(h eq hl);
t lsTopOfNoTReqs= false;
IsTReq(t) => t OnTopOf (tl OnTopOf hl)-t eq tl;
endtype (• TransportServiceBasicTSPRequestHistory *) type TransporiSer viceTSP Req ties! History
is TransportServiceBasicTSPRequestHistory opns
Reduce : TRcqHistory — > TRcqHistory
Remove : TSP, TRcqHistory —> TReqHistorv
Append : TSP. TRcqHistory —> TRcqHistory
Tops. TDI STops, TEXDISTops
: TReqHistory —> TRcqHistory
cons forall t, II : TSP, h. h 1 : TreqHistory ofsort TRcqHistory
Reduce (NoTReqs) = NoTReqs;
JsTReq(t) => Reduced OnTopOf h) =h;
Remove(t. NoTReqs) = NoTReqs;
t eq 11 « > Removed, tl OnTopOf hl) =h;
t ne If «> Remove(t, tl OnTopOf hl)=tl OnTopOf Remove (t. hl);
Append(t, NoTReqs) =t OnTopOf NoTReqs;
IsTReq(tl) => Append(t. tl OnTopOf hl) = tl OnTopOf Append'd, hl);
Tons < NoTReqs) = NoTReqs:
IsiReq(t), IsTDlS(t) ->Tops(t OnTopOf h)=t OnTopOf
ГОСТ Р ИСО/МЭК ТО 10023-93
NoTReqs;
IsTReq(t), bTE.X(t> or IsTCON(0 -> Tops(t OnTopOf h)-t OnTopOf TDISTops(h);
IsTReq(t), hTDTfti = >Tops(t OnTopOf h)~t OnTopOf
TEXDlSTops (h):
TDlSTops (NoTReqs) - NoTReqs;
fsTReqft)', IsTDIS(t) «>TDISTops(t OnTopOf h) = t OnTopOf NoTReqs;
IsTReq(t), nol(I$TDIS(t)) => TDI STops(t OnTopOf h)-
TDlSTops(h);
TEXDlSTops (NoTReqs) = NoTReqs:
IsTReq(l), UTDlS(t) = > TEXDlSTops(T OnTopOf h)-TDrSTops(t
OnTopOf h):
IsTReq(t), IsTEX(t) -> TEXDlSTops(t OnTopOf h)=t OnTopOf TDlSTops (h);
IsTReq(t). not(IsTEX(t)). not(lsTDIS(t))
= > TEXDISTops(t OnTopOf h) =TEXDlSTops (h);
endtype (• TransportServiceTSPRequestHistory *)
12.3.5 Определения процессов
Для заданной истории запросов rh TSPEveni специфицирует ограничения ла возможное следующее событие. Параметр erh — это последовательность выполненных запросов, достаточная для определения следующей возможной индикации.
Следующие четыре требования формулируются для обслуживания не детерминизма поставщика в плане его участия в следующем событии.
а) Поставщик никогда нс отказывается участвовать в событии запроса (см. также определение TSPReqEycnt ниже).
Примечание- — Возможное отклонение запросов определяется процессами TCAoccptance и TBackpreasure (см. соответственно разделы 14 и J5).
Ь) Может быть выполнена только та индикация, которая относится к верхнему запросу непустой erh, соответствующей fslndicationOf (см. 8.4.3.4), Если такая индикация возникает, соответствующий ей запрос удаляется из rh.
Примечание — Для заданного запроса поставщик озаглавливается, чтобы автономно определить значения парамстр-ов индикации, при условии, что пня удовлетворяют этому требованию.
с) Для любого заданного верхнего запроса непустого erh поставщик может представить не связанную с ним пиликанию только в том случае, если это вызывает участие:
42
ГОСТ Р ИСО/МЭК ТО 10023-93
1) в индикации, связанной с запросом следующей более высокой значимости в erh, если таковой существует, или
2) в генерированной поставщиком индикации (см. 8.4.3.4).
В случае 1) требования Ь), с) и d) применяются к erh, без его верхнего запроса.
ci) Если пользователь отклоняет индикацию, то должна быть представлена индикация, соответствующая случаям I) или 2) требования с)
process TSPReqEvent [t] (rh : TReqHistory) : exit (TReqHistory) : = t?ta : TAddress ?tcei : TCEI ?tsp : TSP [IsTReq (tsp) ] : exit (Append(tsp. rh))
endproc (* TSPReqEvent *)
process TSPEvent [t] (erh, rh : TReqHistory) : exit(TReqHistory) : = TSPReqEvent [t] (rh)
[not (IsEmpty(erh)) ]
— >
(choice tspr. tspi : TSP
J(tspr IsTopOf erh) and (tspi IsIndlcationOf tspr)]
—>
(t ?ta : TAddress ?tcei 'TCEI Itspi : exit (Remove(tspr, rh)) I 1 i ; TSPEvent [t] (Reduce(erh). rh)))
I J
[Isb-mpty(erh)]
—>
(choice tdi : TSP
[Provide rGenera ted I nd (tdi)]
—>
l ;
(t?ta : TAddress ?(cei : TCEI Itdi ; exit (rh) [ ] TSPReqEvent It] (rh)))
end proc (* TSPEvent *)
Г____________________
13 ИДЕНТИФИКАЦИЯ ТРАНСПОРТНЫХ СОЕДИНЕНИИ
Любые два разных экземпляра TConnection, которые одновременно имеют доступ к одному ПДУТ, должны быть различимы
43
ГОСТ Р НСО/МЭК ТО (0023-93
для пользователя транспортных услуг. Это достигается при помощи идентификатора оконечного пункта ТС — tcei. который передается с каждым сервисным примитивом на каждый ИДУТ. Следовательно, требуется, чтобы:
а) на любом ИДУТ в любой момент времени никакой tcei не мог быть назначен более чем одному TConnection и
Ь) каждый TConnfection использовал один и тот же tcei на каждом ПДУТ в течение всего времени существования ТС, который он представляет
Если последнее ограничение можно специфицировать внутри определения TConnection (см. 31.2), то первое ограничение имеет более глобальный характер и ниже представлено процессом TCIdentification.
Для каждого ПДУТ хранится след используемых идентификаторов оконечного пункта ТС при помощи параметра Use. который является множеством пар вида TId TAddressXTCE! (см ТСЕIdentification в 8.3). Определение TCEIdentifications представляет эти множества Use вначале пустыми. Пара (ta. tcei) находится в Use тогда и только тогда, когда tcei назначается некоторому ТС. имеющему доступ к ПДУТ с адресом (а
TCIdent позволяет передавать любой запрос или индикацию Т-СОЕДИНЕНИЕ любому заданному ПДУТ с адресом ta только с таким tcei, чтобы пара (ta. tcei) не присутствовала в Use. На другие примитивы это ограничение не налагается, но при выполнении примитива Т-РАЗЪЕДИНЕНИЕ соответствующая пара (ta. tcei) удаляется из Use.
Примечание — Необходимо учитывать следующую техническую деталь: Insert (е. s)-(e) U S- Следовательно, insert (с, $)—$ всякий раз, когда е С S. --------------------------------------------^ type TCEIdentifications
is Set actualizedby TCEfdentification using sortnames
TId for Element
Bool for FBool
Tlds for Set
endtype (* TCEIdentifications *)
process TCIdentification Ft] : noexit : =
TCIdent ft] ({ ) of Tlds)
endproc (* TCIdentification •)
process TCIdent ft] (Use : Tlds) : noexit :• t ?ta : TAddress ?tcei : TCEI ?tsp : TSP (IsTCONI (Isp) implies (TId (ta, tcei) Notin Use)];
44
ГОСТ ₽ ИСО/МЭК ТО 10023—93
(let ti : Tld = Tld(ta. tcei) in
fnot(l$TDlS (ispj)]—> TCldent ft] (Insert(ti. Use))
[IsTDlS(bp) ]-> TCldent ft] (Remove(«, Use))) endproc (* TCldent *)
<*_________________________________________
14 ПРИНЯТИЕ ТРАНСПОРТНЫХ СОЕДИНЕНИЯ
В любой момент времени поставщик услуг способен принять установление новых соединений только в конечном множестве пунктов доступа к услугам и в.оконечных пунктах соединения. Это определяется процессом TCAcceptance, который внутренне выбирает конечное множество пар (ta. tcei) перед участием в каком-либо взаимодействии Если взаимодействие образует новое ТС, то оконечный пункт, где произошло это взаимодействие, должен быть среди тех, которые представлены AcceptTC.
Однако при каждом выборе AcceptTC множество оконечных пунктов, где могут быть образованы новые соединения, является в действительности подмножеством AcceptTC. вследствие ограничения разделении на идентификацию ТС (см. раздел 3). Более точно новое соединение может быть образовано только с парой (ta, tcei), которая находится в AcceptTC. а не в Use. Следовательно, при каждом выборе AcceptTC множество оконечных пунктов, где могут быть образованы новые соединения, представлено разностью AcceptTC — Use.
Поставщику транспортных услуг присущ внутренний недетер-мкнязм при динамическом выборе того, сколько и какие оконечные пункты можно выделить для новых соединений, при условии выполнения минимальных функциональных требований — если нет активных ТС, поставщик услуг должен быть способен принять хотя бы одно ТС. т. е. подмножество AcceptTC, где могут быть действительно приняты новые ТС. должно быть в этом случае непустым.
Примечание — В самом деле, требование минимальной функциональности ЖВММлентио более простону требованию, чтобы AcceptTC было непустым в лю<5ом случае, если принимать во вникание ограничения, наложенные TCtcientification.
Это действительно так, поскольку:
а) если нет активных ТС, то Use пустое, таким образом подмножество AcceptTC, где могут быть приняты новые ТС. является самим AcceptTC, в то время как
45
ГОСТ Р ИСОМЭК ТО 10023-93
Ь) если активно несколько ТС, выбор непустого AcceptTC еще допускает, что подмножество, где могут быть приняты новые ТС. может быть пустым, а именно как только AcceptTC включено в Use.
process TCAcceplanceft] : noexit :—
choice AcceptTC : TIds
(AcceptTC ne { } ] — >
t?ta : TAddress ?tcei : TCEI ?tsp : TSP [IsTCON I9t$p) implies (Tld(ta, tcei) Isln AcceptTC)] ;
TCAcceptance(tj
endproc (• TCAcceptance *)
IS УПРАВЛЕНИЕ ПОТОКОМ ПРИ ПОМОЩИ ОБРАТНОЙ СВЯЗИ
Допускается любой недетермнннзм поставщика услуг в отношении приема запросов на передачу данных, но одна зависимость между ограничениями управления потоком для нормальных и срочных данных задана. Эта зависимость вытекает из утверждения 9 2 ГОСТ 34.960. что «нормальные данные... нельзя добавлять в очередь, если их добавление может помешать добавлению срочных ПБДТ...».
Для поддержки абстрактного- представления этого требования, и именно только в терминах взаимодействий услуг, вводится параметр MustAcceptTEX, который хранит трассу оконечных пунктов ТС. в которых последним выполненным запросом был запрос Т-ДАННЫЕ. В любой момент времени поставщик может произвольно выбрать конечные множества AcceptTDT и AcceptTEX, представляющие два множества оконечных пунктов- ТС. где поставщик может принять нормальные я срочные СБДТ соответственно.
Вышеупомянутая зависимость представлена требованием, что AcceptTEX должен включать Must Accept ТЕХ. Никакие другие за-внсдмостн, которые могут существовать в реализациях услуг транспортного уровня, не описан^.
Примечание — В любой момент времени при динамическом произвольном выборе множества AcceptTDT множество оконечных пунктов, где запросы Т-ДАННЫЕ могут быть действительно приняты, входят в пересечение множеств
46
ГОСТ Р ИСО, МЭК ТО 10023-93
AcccplTPT it Use; это точное подмножество AcccptTDT. представляющее оконечные пункты, находящиеся в фазе передачи данных (см. 11.3 I) Аналогичное замечание применимо и при обратной связи срочных данных.
process TBackpressure [t] : noexit :*■
TBackp ft] <{ } of Tlds) 11 | RunButTDTreqTEXreqTDIS (t] endproc (’ TBackpressure *) process TBackpft] (MustAcceptTEX : Tlds) : noexit : = choice AcceptTDT, AcceptTEX : Tlds
[MustAcceptTEX IsSubsetOf AcceptTEX] — >
(t?ta : TAddress ?tcei : TCEI ?tdr: TSP [IsTDTreq (tdr) and (TId(ta, tcei) Ishi AcccptTDT)] ;
TBackp [t] (Insert (TId (ta, tcei), MustAcceptTEX))
t?ta ; TAddress ?tcei : TCEL ?ter : TSP [IsTEXreq (ter) and (TJd(ta, tcei) Isin AcceptTEX)] ;
TBackp (t) (Remove(TID(ta. Tcei), MustAcceptTEX)) t?ta : TAddress ?tcei ; TCEI ?td ; TSP [IsTDlS(td)] ;
TBackp |t] (Remove(TId(ta. Tcei), MustAcceptTEX))) endproc (*TBackp *) process RunButTDTreqTEXreqTDlSft] : noexit : = t?ta : TAddress ?tcei : TCEI ?tsp : TSP [not (IsTDTreq (tsp) or IsTEXrcq(tsp) or IsTDJS(tsp))] ;
RunButTDTreqTEXrcqTDIS [t] endproc (* RunButTDTreqTEXreqTDIS *) (•_________________________________________________
16 ПЕРЕДАЧА В РЕЖИМЕ-БЕЗ-УСТАНОВЛЕНИЯ-СОЕДИНЕННЯ
16.1 Определения процесса
TSConnectionless основан на индикациях, которые могут выполняться в ответ на ранее выданные запросы. Для описания истории индикаций используется множество.
process TSConnectionless[E] : noexit : =
Connectionless ft] (NoTCIRcq)
endproc (* TSConnectionless *)
process Connectionlessft] (rh : TCIReqHistory) : noexit : =
47
ГОСТ Р ИСОМЭК ГО 10023—93
t?ia : TAddress ?tsp : TSP (IsTUDTreq(tsp) and
(Lenght (UserData (tsp))
le MaxTUDTLength) J ; Connectionless [1] (Insert(tsp, rh))
[rh ne NoTCIReq]
—>
(choice tspr, tspi .: TSP
[tspr Isln rh and (tspi IsIndicationOf tspr)]
—>
t?la : TAddress Itspi [ta IsCallingOf tspi] ;
(Connectionless [t] (Remove (tsor, rh))
i ; Connectionless [t] (rh))
i ; Connectionless [t] (Remove(tspr, rh))
endproc (* Connectionless *)
(*____________________
16.2 Определения данных
-----_-------------------------•)
type Basic FransporlServiceConnect ion less RecHisiory
is Set actualizedby Transport Serviceprimitive using sort names
TSP for Element
Boo] for FBooi
TCIRcqHistory for Set
opnnames
NoTCIReq for { }
endtype (* BasicTransportServiceConnectioniessRecHistory *)
type MaxTUDTLength
is DecNatRepr
opns
MaxTUDTLength —> nat
eqns
ofsort Nat
MaxTUDTLength-NatNum (6 + (3+ (4+ (^+Dec(3))))):
endtype (* MaxTUDTLength *)
endspec (* Transportservice *)
48
ГОСТ Р ИСО/МЭК ТО 10023-93
Библиографические данные
УДК 681.324:006.354
П85
Ключевые слова: передача данных, обмен информацией между системами, формализованное описание, услуги транспортного уровня, язык LOTOS, эталонная модель, взаимосвязь открытых систем, типы данных, процессы
ОКСТУ 4002
49
Редактор В. М. Лысенкика Технический редактор О. И. Никитина
Корректор Я И. Кануркина
Сдаго в илб. tl 02 9ч riosn. ■ пет 29.019». Уел п л 3.20. Усл кр «”■ ЗЖ Уч им я -W Т-р »Я ШЭ С ИЗО.
Орсеи* «Зям Почет»» Издательство стандартов. IWWti. Моски. Колодези мА вер . 14
Калумска» нмграфия стандарте», ул. Модаоасхая, 35«- За» 303
