ГОСТ 34.960-91 Система обработки информации. Взаимосвязь открытых систем. Услуги транспортного уровня

ГОСТ Р ИСО/МЭК ТО 10023-93

государственный стандарт российской федерации

ИНФОРМАЦИОННАЯ ТЕХНОЛОГИЯ ПЕРЕДАЧА ДАННЫХ И ОБМЕН ИНФОРМАЦИЕЙ МЕЖДУ СИСТЕМАМИ. ФОРМАЛИЗОВАННОЕ ОПИСАНИЕ УСЛУГ ТРАНСПОРТНОГО УРОВНЯ (ГОСТ 34.960—91) НА ЯЗЫКЕ

LOTOS

Издание официальное

ГОССТАНДАРТ РОССИИ Москва

ГОСТ Р ИСО/МЭК ТО 10023—93

Предисловие

• 1 ПОДГОТОВЛЕН И ВНЕСЕН Техническим комитетом по стандартизации ТК 22 «Информационная технология»

• 2 УТВЕРЖДЕН И ВВЕДЕН В ДЕЙСТВИЕ Постановлением Гос

стандарта России от 29.12.93 № 293

Настоящий стандарт подготовлен на основе применения аутентичного текста международного стандарта ИСО МЭК ТО 10023— 92 «Информационная технология. Передача данных и обмен информацией между системами. Формализованное описание ИСО 8072 на LOTOS»

• 3 ВВЕДЕН ВПЕРВЫЕ

© Издательство стандартов, 1994

Настоящий стандарт не может быть полностью или частично воспроизведен, тиражирован и распространен в качестве официального издания без разрешения Госстандарта России

СОДЕРЖАНИЕ

Область применения . . .'.........

Нормативные ссылки ............

Определения ..............

Символы и сокращения...........

Соглашения

Требования ..............

Введение в формализованное описание .......

Типы данных на интерфейсе

Глобальные ограничения ...........

Обеспечение транспортного соединения

Локальные ограничения для оконечного пункта ТС . . .

Межоконечные ограничения для одного ТС......

Идентификация транспортных соединений......

Принятие транспортных соединений . ■.....

Управление потоком при помощи обратной связи . . .

Передача в режиме-без-установления-соединения ....

Библиографические данные..........

ГОСУДАРСТВЕННЫЙ СТАНДАРТ РОССИЙСКОЙ ФЕДЕРАЦИИ

Информационная технологии

ПЕРЕДАЧА ДАННЫХ И ОБМЕН ИНФОРМАЦИЕЙ МЕЖДУ СИСТЕМАМИ. ФОРМАЛИЗОВАННОЕ ОПИСАНИЕ УСЛУГ ТРАНСПОРТНОГО УРОВНЯ (ГОСТ 34.960—91) НА ЯЗЫКЕ LOTOS

Information Technology Telecommunications and Information Exchange Between Systems. Formal Description of 8072 in LOTOS

Дата введения 1994—07—01

• 1 ОБЛАСТЬ ПРИМЕНЕНИЯ

Настоящий стандарт распространяется на транспортный уровень эталонной модели взаимосвязи открытых систем (ВОС) и определяет услуги транспортного уровня ВОС, определенные в ГОСТ 34.960, при помощи метода формализованного описания LOTOS, определенного в ИСО 8807.

Примечание — Формальное определение типов данных и процессы, представленные в настоящем стандарте, могут использоваться для формализованного описания протоколов транспортного и сеансового уровней ВОС на языке LOTOS

• 2 НОРМАТИВНЫЕ ССЫЛКИ

Нижеперечисленные стандарты содержат положения, которые путем ссылок на них по тексту образуют положения настоящего стандарта. Все ссылки предполагают последнее издание указанных стандартов.

Национальные комитеты — члены МЭК и ИСО имеют списки международных стандартов, действующих на текущий момент.

ГОСТ 28906—91 (ИСО 7498—84, ИСО 7498—84 Доп. 1—84) Системы обработки информации. Взаимосвязь открытых систем. Базовая эталонная модель

ГОСТ 34.960—91 (ИСО 8072—86, Доп. 1—86 ИСО 8072—86) Системы обработки информации. Взаимосвязь открытых систем. Определение услуг транспортного уровня

Издание официальное

ИСО 8072—86/Поп. 1 Системы обработки информации. Взаимосвязь открытых систем. Определение услуг транспортного уровня. Техническая поправка 1¹.

ИСО/ТО 8509—87 Системы обработки информации. Взаимосвязь открытых систем. Соглашения по услугам ¹.

ИСО 8807—89 Системы обработки информации. Взаимосвязь открытых систем. LOTOS — метод формализованного описания, основанный на упорядочении во времени наблюдаемого поведения ¹.

ИСО/МЭК ТО 10024—92 Информационная технология. Передача данных и обмен информацией между системами. Формализованное описание ИСО 8073 (разделы 0, 1, 2 и 3) на языке

LOTOS ¹.

• 3 ОПРЕДЕЛЕНИЯ

В настоящем стандарте используются определения, приведенные в ГОСТ 34.960.

• 4 СИМВОЛЫ И СОКРАЩЕНИЯ

В настоящем стандарте используются символы, определенные в разделе 6 (формальный синтаксис) и приложении А (библиотека типов данных) ИСО 8807,

В настоящем стандарте используются сокращения, содержащиеся в разделе 4 ГОСТ 34.960. Использование других символов и сокращений поясняется при первом их появлении.

• 5 СОГЛАШЕНИЯ

Неформальные пояснения, предшествующие формальным определениям, к которым они относятся, отделяются от последних показанной ниже верхней линией. Отделение формальных определений от последующих неформальных пояснений обозначается показанной нижней линией.

Примечание — Это соглашение соответствует правилам ограничения комментариев, определенным для LOTOS в ИСО 8807 Формальный текст представлен курсивом, а ключевые слова и операторы LOTOS — полужирным шрифтом. Идентификаторы из форматированного текста в неформатированном тексте набраны курсивом.

Соблюдаются соглашения, определенные в ИСО/ТО 8509, по с учетом следующего: термин «запрос* означает как запросные, так и ответные сервисные примитивы, а термин «индикация» означает сервисные примитивы как индикации, так и подтверждения.

• 6 ТРЕБОВАНИЯ

Настоящий стандарт отвечает требованиям, изложенным в разделе 3 ИСО 8807 (более подробную информацию см. в приложении С к указанному стандарту). Настоящий стандарт не содержит каких-либо требований к соответствию.

• 7 ВВЕДЕНИЕ В ФОРМАЛИЗОВАННОЕ ОПИСАНИЕ

Вся граница услуг формально представлена в виде единственного шлюза t. Структура события в t представляет собой тройку значений типа TAddress, TCEI, TSP (см. раздел 8). Первое значение идентифицирует TSAP, в котором происходит взаимодействие. Второе значение идентифицирует ТСЕР внутри TSAP, в котором происходит взаимодействие. Третье значение — это выполняемый при взаимодействии примитив транспортного уровня (TSP). Конкретные значения зависят от многих аспектов услуги.

Описывается поведение поставщика услуг бесконечного вида. Спецификация не содержит параметров.

Используется стиль спецификации, ориентированный на ограничения, поскольку он наиболее подходит для определительного характера стандарта па услугам. Описание ориентировано на характеристики модальностей поведения поставщика услуг исключительно в терминах последовательности выполняемых TSP, т. е. без каких-либо предположений о внутренней структуре самого поставщика.

В основе первой декомпозиции специфицируемого поведения лежат следующие отдельные ограничения:

• a) поставщик услуг может допускать множество, возможно, одновременных соединений (представленных процессом TConnections, см. раздел 9), вместе со

• b) средством выбора среди одновременных соединений нужного (представленным процессом TCIdentification, см. раздел 13), но при

• c) возможности внутреннего недетермннизма при установлений любого дополнительного соединения, если, по меньшей мере, одно соединение уже поддерживается (представленной процессом TCAcceptance, см. раздел 14), и

• d) возможности внутреннего недетермннизма при передаче данные (представленной процессом TBacnpressure, см. раздел 15); при помощи этого принимающий пользователь вызывает эффект управления потоком, сообщая об этом передающему пользователю.

Спецификация динамического поведения предьаряется спецификацией типов данных на интерфейсе (см. раздел 8). Такие определения являются общими для формализованных описаний, которые могут взаимодействовать, а именно для протоколов транспортного и сеансового уровней.

Порядок представления остальных определений обоснован желанием следовать порядку, установленному ГОСТ 34.960, который в основном связан с обеспечением единственного ТС. Описание требований, являющихся локальными для обеспечения одного ТС (представлены в разделах 10, 11 и 12), предшествуют описаниям глобальных требований, упомянутых выше в Ь), с) и d) соответственно.

Типы данных, определенные конструкцией library, импортируются из библиотеки типов данных LOTOS.

specification TransportServiceft]: noexit

library Set, Element, Octetstring, NatRepresentation, NaturalNum-ber, Boolean, FBoolean, DecNatRepr

endlib

(*._.............................................................................................

• 8 ТИПЫ ДАННЫХ НА ИНТЕРФЕЙСЕ

  • 8.1 Общее описание

В соответствии с представлением взаимодействий на границе транспортных услуг (см. раздел 7) типы данных на интерфейсе состоят из трех основных определений, которые соответственно составляют виды TAddress (см. 8.2), TCEI (см. 8.3) и TSP (см. 8.4). Параметр TSP — качество услуги — определяется в 8.5, а остальные параметры — в 8.6. В 8.7 представлены вспомогательные определения.

• 8.2 Транспортный адрес

В ГОСТ 34.960 не определена структура транспортного адреса. Следующее определение использует определение Generalidentifier (см. 8.7) и позволяет представлять бесконечное число транспортных адресов.

----------------- *) type TransportAddress is Generalidentifier renamedby sortnames

TAddress for identifier

opnnames

SomeTAddress for Someldentifier AnotherTAddress for Anotherldentifier endtype (* TransportAddress *)

(* ____________________________________________________________________________________________________

• 8.3 Идентификатор оконечного пункта транспортного соединения

В ГОСТ 34.960 не определена структура идентификатора оконечного пункта транспортного соединения. Приводимое ниже первое определение позволяет представить бесконечное их число. Второе определение представляет идентификаторы оконечного пункта транспортного соединения, которые являются глобальными для всей границы транспортных услуг. Каждый из них представляет собой пару TAddressxTCEI (общее определение Pair и General-Identifier см. в 8.7).

type TCEndpointldentifier is Generalidentifier renamedby sortnames

TCEI for identifier opnnames

SomeTCEI for Someldentifier AnotherTCEI for Anotherldentifier endtype (* TCEndpointldentifier *) type TCEIdentification is Pair actualizedby TransportAddress, TCEndpointldentifier using sortnames

TAddress for Efement TCEI for Element2 Bool for Fbool TId for Pair

opnnames

TId for Pair

ТА for First

TCEI for Second

endtype (* TCEIdentification *)

(*____________________________________________________________________________________________________

• 8.4 Сервисный примитив транспортного уровня (TSP)

  • 8.4.1 Общее описание

Тип данных TCP представлен, начиная с базовой конструкции значений вида TCP (см. ниже). Эта конструкция является прямой формулировкой определения, приведенного в таблице 3 ГОСТ 34.960. Функции, генерирующие значения TCP, называются <кон-структорами ТСР». Это определение заимствует определения, связанные с параметрами TCP (см. 8.6).

Примечание — В некоторых TCP параметр UserData представляет собой OctetString, имеющий фиксированные границы, как определено в ГОСТ 34.960. По техническим соображениям это требование формально представлено процессом ограничения (см. 11.1 и 11.4), а не ограничивающим типом.

В 8.4.2 приведена классификация TCP, которая позволяет, с одной стороны, простым путем расширить базовую конструкцию дополнительными функциями (см. 8.4.3), а с другой — консервативно расширить тип данных в формализованном описании транспортного протокола.

--- --- ---*) type BasicTSP

is TransportAddress, TEXOption, TSQuality, OctetString, TDlSRea-son, TsCIQuality

sorts

TSP

Octetstring —> TSP endtype (* BasicTSP *)

• 8.4.2 Классификация сервисных примитивов транспортного уровня

  • 8.4.2.1 Базовая классификация

Базовая классификация TCP определена при помощи TCPSub-sort, состоящего из набора констант, каждая из которых задает имя TCP в соответствии с таблицей 3 ГОСТ 34.960.

Тип TCPBasicClassifiers — это функциональное расширение базовой конструкции в 8 4.1, где:

• a) функция Subsort генерирует имя TCP;

• b) булевы функции на TCP, названные «определителями подвида ТСР», определяются в соответствии с базовой классификацией, введенной при помощи TCPSubsort.

Примечание — Вспомогательная функция h, отображающая имена TCP на натуральные числа, определяется для упрощения спецификации булевых операций равенств на именах TCP (так же, как на TCP в 84 3 3) Определение IsRequesl, Islndication (на именах TCP) и IsTreq, JsTind (на TCP) отражает соглашение, введенное в раздел 5

type TSPSubsort is NaturalNumber sorts

TSPSubsort

opns

TCONNECTrequest, TCONNECTindication, TCONNECTres-ponse, TCONNECTconfirm, TDATArequest, TDATAindica-tion, TEXDATArequest, TEXDATAindication, TD1SCONN-request, TDISCONNindication, TUDATArequest, TUDATA-indication : —> TSPSubsort

h : TSPSubsort —> Nat

Even, Odd : Nat — > Bool

IsRequest, Islndication : TSPSubsort —> Bool

_eq_,_ne_ : TSPSubsort, TSPSubsort

— > Bool

eqns forall

s, si : TSPSubsort, n : Nat

ofsort Nat

h (TCONNECTrequest) =0;

h (TCONNECTindication) = Succ (h (TCONNECTrequest)); h (TCONNECTresponse) = Succ (h (TCONNECTindication)); h (TCONNECTconfirm) = Succ (h (TCONNECTresponse));

h (TDATArequest) = Succ (h (TCONNECTconfirm));

h (TDATAindication) = Succ (h (TDATArequest));

h (TEXDATArequest) = Succ (h (TDATAindication));

h (TEXDATAindication) = Succ (h (TEXDATArequest));

h (TDISCONNrequest) = Succ (h (TEXDATAindication));

h (TDISCONNindication) = Succ (h (TDISCONNrequest)); ofsort Bool

Even (0) =true;

Even (Succ(0)) = false.

Even (Succ (Succ (n))) =Even(n);

Odd (n) = not (Even (n));

IsRequest (s) = Even (h (s));

Vindication (s) =Odd (h (s));

s eq si = h (s) eq h (si);

s ne sl = not(s eq si);

endtype (* TSPSubsort *)

type TSPBasicClassifiers

is BasicTSP, TSPSubsort

opns

Subsort : TSP —> TSPSubsort

IsTCON, IsTCONl, VTCON2, IsTDT, IsTEX, IsTDIS, IsTCONreq, VTCONind, IsTCONresp, IsTCONconf, IsTDTreq, IsTDISind, IsTReq, IsTInd : TSP —> Bool eqns for al 1

a, al, a2 : TAddress, x : TEXOption, q : TQOS, d : Octetstring, r : TDISReason, t : TSP, clq : CLQOS ofsort TSPSubsort

Subsort(TCONreq(al, a2, x, q, d))= TCONNECTrequest;

Subsort (TCONind (a 1, a2, x, q, d)) =TCONNECT-indication;

Subsort (TCONresp (a, x, q, d) )= TCONNECTresponse;

Subsort (TCONconf (a, x, q, d)) =TCONNECTconfirm;

Subsort (TDTreq (d)) =TDATArequest;

Subsort (TDTind (d)) =TDATAindication;

Subsort (TEXreq (d)) =TEXDATArequest;

Subsort (TEXind (d)) = TEXDATAindication;

Subsort (TDISreq (d)) =TDISCONNrequest;

Subsort (TDISind (r, d)) =TDISCONNindication;

Subsort(TUDTrcq(al, а2, clq, d)) — TUDATArequest; Subsort(TUDTind(al, a2, clq, d)) =TUDATAindication; ofsort Boo!

IsTCON (t) = IsTCON 1 (t) or IsTCOi\’2(t); IsTCONl (t) = IsTCONreq (t) or IsTCONind (t); IsTCON2(t) = IsTCONresp (t) or IsTCONconf (t); IsTDT(t) = IsTDTreq(t) or IsTDTind(t); IsTEX(t) = IsTEXreq(t) or IsTEXind(t); IsTDIS (t) = IsTDISr'eq (t) or IsTDISind (t); IsTCONreq(t) = Subsort (t) eq TCONNEC1 request; IsTCONind (t) = Subsort (t) eq TCONNECTindication; IsTCONresp(t) =Subsort(t) eq TCONNECTresponse; IsTCONconf (t) = Subsort (t) eq TCONNECTconfirrn; IsTDTreq(t) = Subsort (t) eq TDATArequest; IsTDTind (t) = Subsort (t) eq TDATAindication; IsTEXreq (t) = Subsort (t) eq TEXDATArequest;

IsTEXind (t) — Subsort (t) eq TEXDATAindication; IsTDISreq(t) = Subsort (t) eq TDISCONNr'equcst; IsTDISind (t) =Subsort(t) eq TDISCONNindication; IsTUDT(t) = IsTUDTreq(t) or IsTUDTind (t); IsTUDTreq (t) = Subsort (t) eq TUDATArequest; IsTUDTind (t) = Subsort (t) eq TUDATAindication; IsTReq (t) — IsRequest (Subsort (t));

IsTIndft) = vindication (Subsort (t));

endtype (*TSPBasicClassifiers *)

• 8.4.2.2 Вспомогательная классификация

TDATAAtomSubsort вводит дальнейшую классификацию элементарных составляющих примитивов данных, а именно октеты данных пользователя и ограничители СБДТ. Однако в данной спецификации эти составляющие не специфицированы.

Примечание — Единственная причина представления TDATAAtomSubsort в этом описании состоит в том, что таким способом тип данных TransportServicePrimitive допускает консервативное расширение, при котором можно ввести более изящное неэлементарное представление примитивов данных. Такое расширение необходимо в формализованном описании транспортного протокола для правильной формулировки требований, связанных с сегментацией и управлением потоком.

Булева функция Terminates, определенная в TSPClassifiers, связывает элементарное выполнение примитивов данных, что характерно для определения услуг, с неэлементарным их выполнением, присутствующим в формализованном описании протокола.

” *)

type TDATAAtomSubsort is FourTuplet renamedby sortnames

TDATASubsort for Tuplet opnnames

TDATAOCTrequest for TheOne TDATAOCTindication for TheOther TEOTrequest for TheThird TEOTindication for TheFourth endtype (* TDATAAtomSubsort *) type TSPClassifiers is TSPBasicClassifiers, TDATAAtomSubsort opns

Terminates : TDTASubsort, TSP —> Bool

eqns forall

d : Octetstring, s : TDTASubsort, t : TSP ofsort Bool

TEOTrequest Terminates TDTreq (d) =true; TEOTindication Terminates TDTind(d) = true; TEOTrequest Terminates TDTind (d) = false; TEOTindication Terminates TDTreq (d) = false; TDATAOCTrequest Terminates t = false; TDATAOCTindication Terminates t = false; not(IsTDT(t)) => Terminates t = false;

endtype (* TSPClassifiers *)

(*___________________________________________________________________________________________

8.4.3 Функции сервисных примитивов транспортного уровня

• 8.4.3.1 Общее описание

В 8.4.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 определены булевы функции. Причина для такого непрямого представления — неполнота определения при помощи равенств.

Единственное исключение имеется в прямом представлении параметра данных пользователя при помощи функции UserData, так как этот параметр можно определить во всех TSP.

type TSPParameterSelectors is TSPClassifiers

_lsCalledOf_, -IsCallingOf-, -IsRespondingOf- : TAddress, TSP — >Bool

TEXOption, TSP

: TQOS, TSP

: TDISReason, TSP

: TSP

eqns forall

a, al, a2 : TAddress, x, xl, : TEXOption, q, ql : TQOS, d Octetstring, r, rl : TDISReason, t : TSP, clq, clql : C1QOS

ofsort Bool

a IsCalledOf TCONreq(al, a2, x, q, d)=a eq al; a IsCalledOf TCONind(al, a2, x, q, d)=a eq al; a IsCalledOf TUDTreqfal, a2, clq, d)=a eq al; a IsCalledOf TUDTindfal, a2, clq, d) =a eq al; not(IsTCONl (t)) => a IsCalledOf t = false;

a IsCallingOf TCONreq(al, a2, x, q, d)=a eq al; a IsCallingOf TCONind(al, a2, x, q, d)=a eq al; a IsCallingOf TUDTreqfal, a2, clq, d) =a eq al; a IsCallingOf TUDTind(al, a2, clq, d)=a eq al; not(IsTCONl (t)) => a IsCallingOf t = false; a IsRespondingOf TCONresp(al, x, q, d)=a eq al; a IsRespondingOf TCONconf(al, x, q, d)=a eq al; not (IsTCON2(t))) => a IsRespondingOf t = false; x IsTEXOptionOf TCONreq(al, a2, xl, q, d)=x eq xl x IsTEXOptionOf TCONindfal, a2, xl, q, d)=x eq xl x IsTEXOptionOf TCONresp(a, xl, q, d)=x eq xl x IsTEXOptionOf TCONconffa, xl, q, d)=x eq xl not(IsTCON(t)) => x IsTEXOptionOf t = false; q IsTQOSOf TCONreq(al, a2, x, ql, d)=q eq ql q IsTQOSOf TCONind(al, a2, x, ql, d)=q eq ql q IsTQOSOf TCONresp(a, x, ql, d)=q eq ql q IsTQOSOf TCONconf(a, x, ql, d)=q eq ql not(IsTCON(t)) => q IsTQOSOf t = false;

г IsReasonOf TDlSind(rl, d)=r eq rl;

not(IsTDISind(t)) = > r IsReasonOf t = false;

clq IsCIQOSOf TUDTreq(al, a2, clql, d)=clq eq clql clq IsCIQOSOf TUDTind(al, a2, clql, d)=clq eq clql ofsort Octetstring

UserData (TCONreq (al, a2, x, q, d))=d;

UserData (TCONind (al, a2, x, q, d))=d;

UserData (TCONresp (a, x, q, d))=d;

UserData (TCONconf (a, x, q, d))=d;

UserData (TDTreq(d)) = d;

UserData (TDTind (d)) =d

UserData (TEXreq (d)) =d;

UserData (TEXind (d)) =d;

UserData (TDISreq (d)) =d UserData(TDISind(r, d))=d;

UserData(TUDTreq(al, a2, clq, d))=d;

UserData(TUDTind(al, a2, clq, d))=d; endtype (* TSPParameterSelectors *) (*........-..................-..............

• 8.4.3.3 Равенство сервисных примитивов транспортного уровня

Булево равенство на TSP определяется как конъюнкция равенства имени TSP (см. 8.4.2.1) и попарного равенства параметров TSP. Кроме того, для примитивов данных требуется равенство ограничителя (см. 8.4.2.2).

type TSPEquality

is TSPParameterSelectors

opns

_eq_,-ne-,-eqTerm_: TSP, TSP —> Bool eqns forail

a, al, a2, a3 : TAddress, x, xl : TEXOption, q, ql : TQOS, d, dl : Octetstring, r, rl : TDISReason, t, tl : TSP, clq, clql : C1QOS

ofsort Bool

Subsort(t) ne Subsort(tl) => t eq tl=false;

TCONreq(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 (d eq dl);

TCONind(a, a2, x, q, d) eq TCONind(al, a3, xl, ql, dl) = (a eq al) and (а2 eq аЗ) and (х eq xl) and (q eq ql) and (d eq dl);

TCONresp(a, x, q, d) eq TCONresp(al, xl, ql, dl) = (a eq al) and (x eq xl) and (q eq ql) and (d eq dl);

TCONconf (a, x, q, d) eq TCONconf (al. xl, ql, dl) = (a eq al) and (x eq xl) and (q eq ql) and (d eq dl);

TDISind (r, d) eq TDISind (г 1, dl) = (r eq rl) and (d eq 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); TUDTind(a, a2, clq, d) eq TUDTind(al, a3, clql, dl) = (a eq al) and (a2 eq a3) and (clq eq clql) and (d eq dl); not(IsTCON(t) or IsTDIS(t))

= > t eq tl

— (Subsort (t) eq Subsort (tl)) and (UsSrData(t) eq UserData (tl)) and (IsTDT(t) implies (t eqTerm tl); t ne tl =not(t eq tl);

t eqTerm tl

= TEOTrequest Terminates t iff (TEOTrequest Tepminates tl) and (TEOTindication terminates t iff (TEOTindication Terminates tl));

endtype (* TSPEquality *)

(*__________________________________________________________________________________________

• 8.4.3.4 Прочие функции сервисных примитивов транспортного уровня

Функция ProviderGeneratedlnd характеризует TSP, генерируемые исключительно поставщиком услуг. Эта функция используется для описания возможного недетерминизма поставщика услуг (см. 12.3.3).

Функция IsIndicationOf связывает выполнение TSP в каждом оконечном пункте транспортного соединения с предварительным выполнением соответствующего примитива в другом пункте того же самого транспортного соединения (см. 12.3.3). Эта функция также представляет требования по согласованию в отношении возможного недетерминизма поставщика услуг (см. раздел 10 и 14.2 ИСО 8072).

type TransportServicePrimitive

is TSPEquality

opns

ProviderGeneratedlnd : TSP —> Bool

-IsIndicationOf___IsValidTCON2For_ : TSP, TSP —> Bool

eqns

forall

t, tl : TSP, a, al, a2, a3 : TAddress, x, xl : TEXOption, q, ql : TQOS, d, di : Octetstring, clq, clql : C1QOS ofsort Bool

PrividerGeneratedlnd (t)

= IsTDlSind(i) and (Provider IsReasonOf (t) and (UserData(t) eq <>);

TCONconf(al, xl, ql, dl) IsValidTCON2For 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) IsValidTCON2For TCONind(a, a2, x, q, d) = (al eq a) and (ql eq q) and ((xl eq UseTex) implies (x eq UseTEX));

not ((IsTCONconf (tl) and IsTCONreq(t)) or ((IsTCON-resp(tl) and IsTCONind (t))) => tl IsValidTCON2For t = false;

TCONind(al, a3, xl, ql, dl) IsIndicationOf TCONreq (a, a2, x, q, d) = (al eq a) and (a3 eq a2) and (xl eq x) and (ql к q) and (dl eq d);

TCONconf(al, xl, ql, dl) IsIndicationOfTCONresp(a, x, q, d) = (al eq a) ?nd (xl eq x) and (ql eq q ) and (d 1 eq d); IsTCON(t), not(IsTReq(t)) =>tl IsIndicationOf t = false; IsTCON(t), IsTReq(t), h (Subsort(tl)) ne Succ(h(Sub-sorl(t))) =>tl IsIndicationOf t = false;

TUDTind(al, a3, clql, dl) IsIndicationOf TUDTreq(a, a2, clq, d) = (al eq a) and (a3 eq a2) and (clql le clq) and (dl eq d);

not(IsTCON(t) or IsTUDT(t)) = > tl IsIndicationOf t = IsTReq(t) and IsTInd(tl) and (h (Subsort (tl)) eq Succ (h (Subsort (t)))) and ((TEOTindication Terminates tl) iff (TEOTrequest Terminates t)) and (UserData(tl) eq UserData (t));

endtype (* TransportServicePrimitive *)

(*___________________________________________________________________________________________________

8.5 Качество услуг (КУ)

• 8.5.1 Общее описание

Структура параметра КУ подразделяется в соответствии с определением, приведенным в разделе 10 ГОСТ 34.960.

Первая декомпозиция выделяет параметры КУ: производительность ТС, приоритет ТС и защита ТС. Эти структуры определяются в 8.5.2—8.5.4 соответственно и ссылаются на вспомогательные определения КУ. приведенные в 8.5.5.

Как конструкция TQOS, так и конструкция TCPerformance, а также их подструктуры в основном состоят из декартова произведения, образованного функциями проекции, каждая из которых дает один множитель значения произведения и булевых функций, специфицирующих равенство и частичное упорядочение КУ, как определено в разделе 10 ГОСТ 34.960.

В 8.5.2 в виде пояснения представлены видовые произведения, относящиеся к производительности ТС.

Примечания

• 1 Порядок, в котором представлены определения КУ. отличается от порядка, представленного в разделе 10 ГОСТ 34.960. что обеспечивает группирование (в формальном контексте) сходных определений, что облегчает чтение.

• 2 Представление значений TQOS формально полное только для той области, которая оказывается необходимой, чтобы обеспечить абстрактную спецификацию таких значений, как параметры TSP, и соответствующих требований по согласованию КУ (см. четвертый абзац раздела 10 ГОСТ 34 960) Дополнительные функции, позволяющие оценивать КУ при тестировании, и примеры измерений не определены. Оценка каким-либо образом КУ не связана с динамическими требованиями, представленными настоящим формализованным описанием, так как семантика LOTOS абстрагируется от количественных аспектов, таких как время и вероятности.

• 3 В настоящем описании не указано, является ли значение КУ абсолютным требованием пользователя или приемлемо также пониженное значение.

Структура параметров КУ режима-без-установления-соедине-ния представлена в виде декартова произведения параметров TCTransitDelay, TCProtection, NCProbability и TCPriority.

type TSQuality

is POThreeTuple actualizedby TCPerformance, TCPriority, TCProtection using sortnames

TQOS for ThreeTuple TCPerformance for Element TCPriority for Element2 TCProtection for Element3 Bool for FBool

opnnames

TQOSPerformance for First TQOSPriority for Second TQOSProtection for Third TQOS for Tuple endtype (* TSQuality *)

ГОСТ Р ИСО/МЭК ТО 10023—98

type TSCIQuality

is POFourTuple actualizcdby CLTransitDelay, TCProtection, Probability, TCPriority using sortnaines

Bool for FBool

CLQOS for FourTuple

CLTransDelay for Element TCProtection for Eletnent2 Prob for Element3 TCPriority for Element4 opnnames

CLQOSTransDelay for First CLQOSProtection for Second CLQOSProbability for Third CLQOSPriority for Fourth CLQOS for Tuple endtype {* TSCIQuality *)

• 8.5.2 Параметры производительности

8.5.2.1 Общее описание

Параметры производительности, составляющие компонент параметров КУ, имеют следующую структуру четверки:

TCPerformance = Del ays X Fail uresX Throughput XRER, что представлено в данном ниже определении. Определения компонентов даны в 8.5.2.2—8.5.2.5.

Примечание — Вспомогательные определения КУ (см 8 5.5) полезны для понимания определений параметра производительности, содержащегося в 85 22—8 5.2.5 При первом чтении настоящего стандарта рекомендуется сначала ознакомиться с 8.5.5.

type TCPerformance is BasicTCPerformance opns

-It., _le_, _gt_,

-ge- : TCPerformance, TCPerformance —> Bool

eqns forall

d, dl : Delays, f, fl : failures, t, tl : Throughput, r, rl : TPRER, pf, pfl : TCPerformance

ofsort Bool

Performance (d, f, t, r) le Performance(dl, fl, tl, rl) = (d ge dl) and (f ge fl) and (t le tl) and (r ge rl);

pf It pfl = (pf le pfl) and not(pfl le pf);

pf eq pfl= (pf le pfl) and (pfl le pt);

pf ne pfl=not(pf eq pfl);

pf ge pfl = pf 1 le pf;

pf gt pfl= (pf ge pfl) and not(pfl ge pf); endtype (* TCPerformance *) type BasicTCPerformance is FourTuple actualizedby TCDelays, TCThroughput TCResidualErrorRate, TCFailureProbabilities using sortnames

TCPerformance for FourTuple

Delays for Element

Failures for Element2

Throughput for EIement3

TPRER for Element4

Bool for FBool

opnnames

Performence for Tuple

Delays for First

Throughput for Second

RER for Third

Failures for Fourth

gndtype (* BasicTCPerformance *)

• 8.5.2.2 Параметры задержки

Параметры задержки имеют следующую структуру тройки: Delays = EstDelayXTransDelayxRelDelay, где:

EstDelay=Nat

TransDelay = Nat⁴

RelDelay=Nat²

EstDelay — вид параметра задержки установления ТС, который имеет линейную структуру (таким образом определена единственная взаимно однозначная проекция).

TransDelay — вид параметра транзитной задержки, который имеет структуру четверки. Каждая проекция представляет транзитную задержку для отдельного направления передачи и скорости (а именно «максимальная» и «средняя», см. 10.3 ГОСТ 34.960). Это определение представлено как переименование вспомогательного определения, приведенного в 8.5.5.

RelDelay — вид параметра задержки освобождения, который имеет структуру двойки. Каждая проекция представляет задержку освобождения ТС для отдельного пользователя ТС (которому

ГОСТ Р ИСО/МЭК ТО 10023—93

сигнализируется об успешном освобождении, см. 10.7 ГОСТ 34.960). Форма этого определения —экземпляр общего определения (приведенного в 8.5.5), полученный использованием в качестве актуального типа параметра NatRepresentations, который определен в библиотеке типов данных LOTOS.

:-------------- *)

type TCDelays

is POThreeTuple actualizedby TCEstablishmentDelay, TransitDelay, TCReleaseDelay using

sortnames

Delays for ThreeTuple

EstDelay for Element

TransDelay for Element2

RelDelay for Element3

Bool for FBool

opnnames

TCEstablishment for First

Transit for Second

TCRelease for Third

Delay for Tuple

endtype (* TCDelays *)

type TCEstablishmentDelay

is NatRepresentations sorts

EstDelay

opns

EstDelay : Nat —>EstDelay

Time : EstDelay —> Nat

_eq_, _ne_, _le_, -It-, -ge_, _gt_ : EstDelay, EstDelay

— > Bool

eqns

forall

n, nl : Nat, e, el : EstDelay

ofsort Nat

Time (EstDelay (n)) =n;

ofsort Bool

EstDelay(n) le EstDelay (nl) =n le nl;

e It el = (e le el) and not(el le e);

e eq el = (e le el) and (el le e);

e ne el =not(e eq el);

e ge el =el le e;

e gt el = (e ge el) and not(el ge e);

endtype (* TCEstablishmentDelay *)

type TransitDelay

is DTRateDirecitonQOSParameter renamedby sortnames

TransDelay for DQOSP

opnnames

TransDelay for RDQOSP endtype (* TransitDelay *) type TCReleaseDelay is PODoubleParameter actualizedby NatRepresentations using sortnames

Nat for Element

Nat for Element2

RelDelay for Pair

Bool for FBool

opnnam'es

AtCalling for First

AtCalled for Second

RelDelay for Pair endtype (* TCReleaseDelay *) type CLTransitDelay is NaturalNumber renamedby sortnames

CLTransDelay for Nat endtype (*CLTransitDelay *)

• 8.5.2.3 Пропускная способность

Параметры пропускной способности имеют следующую структуру четверки:

Throughput = Nat⁴

type TCThroughput

is DTRateDirectionQOSParameter renamedby sortnames

Throughput for RDQOSP

opnnames

Throughput for RDQOSP

endtype (* TCThrouhput *)

• 8.5.2.4 Вероятность отказа

Параметры вероятности отказа имеют следующую структуру четверки:

Failures = Prob⁴

type TCFailureProbabilities

is POFourTuple actualizedby Probability using sortnames

Prob for Element

Prob for Element2 Prob for Element3 Prob for Element4 Bool for FBool Failure for FourTuple opnnames

TCEstablishment for First Transfer for Second TCResilience for Third TCRelease for Fourth Failures for Tuple

endtype (* TCFailureProbabilites *)

• 8.5.2.5 Коэффициент необнаруженных ошибок Параметры коэффициента необнаруженных ошибок (КНО) имеют следующую структуру двойки: КНО = Prob²

Каждая проекция представляет КНО для отдельного направления передачи. Форма этого определения аналогична той, которая использована для задержки освобождения ТС (см. 8.5.2.2), но с другим типом актуального параметра, а именно Probability (см. 8.5.5). На самом деле, КНО определен в ГОСТ 34.960 как отношение измеренных значений, а не как вероятность. Однако это не имеет значения для образования типа, поскольку значения КНО (любая из двух проекций) и операции на КНО совпадают со значениями и операциями вероятности соответственно.

type TCResidualErrorRate

is POPair actualizedby NaturalNumber using sortnames

TPRER for Pair

Nat for Element

Nat for Element2

Bool for FBool opnnamfes

RER for Pair

Target for First Minimum for Second endtype (* TCResidualErrorRate *) (*...................................................—.................................-

8.5.3 Приоритет TC

При помощи переименования натуральных чисел уровни приоритета представлены как полностью упорядоченное множество. В ГОСТ 34.960 указано, что число уровней приоритета ограничено. Это также применимо к реализации типа данных NaturalNumber.

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 TCProtection is OrderedFourTupIet renamedby sortnames

TCProtection for Tuplet

opnnames

NoProtection for TheOne

Monitoring for TheOther

Manipulation for TheThird

FullProtection for TheFourth endtype (* TCProtection *)

• 8.5.5 Вспомогательные определения КУ

В типе Probability вид Prob задает интервал действительных чисел [0, 1] вместе с элементом Undefined, который представляет отношения, нс входящие в этот интервал.

DTRateDirectionQOSPararneter поддерживает определение па раметра КУ в виде натурального числа, который имеет четыре компонента (или проекции), каждый из которых индексируется скоростью передачи данных и направлением передачи. Виды DTRate и DTDirection обеспечивают эти индексы. Компоненты генерируются функцией Proj. Конструкция этого типа представлена снизу вверх, используя определения типов DTDirectionQOSPar и DTDirectionQOSParameter для построения структуры четверки из двух двоек. Общее определение параметра PODoubleParameter см. в 8.7.

Примечание — Определение в 8.7 необходимо для понимания приведенных ниже определений. При первом чтении рекомендуется сначала прочесть 8.7.

type Probability is NaturalNumber sorts

Prob

opns

eqns

forall

m, n, j, k : Nat, p, q : Prob

ofsort Prob

m gt n or (n eq 0) => m/n = Undefined;

m le n, n ne 0, j ne 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);

m le n, n ne 0=> Undefined le (m/n) = false;

p le Undefined = true;

p It q=(p le q) and not(q le p);

p eq q= (p le q) and (q le p);

p ne q = not(p eq q);

p ge q = q le p;

p gt q= (p ge q) and not (q ge p);

endtype (* Probability *)

type DTDirectionQOSPar

is POPair actualizedby NaturaiNumber using sortnames

Nat for Element

Nat for Element2

DQOSP for Pair

Bool for FBool

opnnames

FromCalling for First

FromCalled for Second

DQP for Pair

endtype (* DTDirectionQOSPar *)

type DTRateDirectionQOSParameter

is POPair actualizedby DTDirectionQOSPar using sortnames

Nat for Element

Nat for Element2

DQOSP for Pair

Bool for FBool

opnnames

FromCalling for First

FromCalled for Second

DQP for Pair

endtype (* DTDirectionQOSPar *)

type DTRateDirectionQOSParameter

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 (* DTRateDirectionQOSParameter *)

(*______________________________________________________________________________________

8.6 Параметры сервисных примитивов транспортного уровня

Вариант срочных данных и параметры причины разъединения в 1SP определяются типами TEXOption и TDISReason соответственно. Структура параметра КУ определена в 8.5 посредством TSQuality. Другими типами параметров TSP являются TAddress (см. 8.2) и Octetstring (данные пользователя), которые импортируются из библиотеки типов данных LOTOS (см. раздел 7).

Примечание — Представление значений TDTSeason соответствует определению в 14 2.1 ГОСТ 34.960, но без представления дополнительной информации и примеров, приведенных в примечаниях (см. 8 7 для определения TwoTuplet).

*) type TEXOption

is TwoTuplet renamedby sortnames

TEXOption for Tuplet

opnnames

UseTEX for TheOne NoTEX for TheOther endtype (* TEXOption *) type TDISReason is TwoTuplet renamedby sortnames

TDISReason for Tuplet opnnames

User for TheOne Provider for TheOther endtype (* TDISReason *)

8.7 Вспомогательные определения

General Identifier определяет бесконечное множество идентификаторов вместе с равенством на нем.

Element определен в библиотеке типов данных LOTOS, тогда как Element2, Element3 и Element4 являются его отдельными изоморфными копиями. Эти типы используются в определениях Pair, ThreeTuple и FourTuple, которые определяют кортежи общего вида из двух, трех или четырех значений, возможно разных видов, с равенством и проекциями. TwoTuplet и FourTuplet определяют множества. состоящие соответственно из двух и четырех элементов, наделенных булевым равенством. OrderedFourTuplet является расширением FourTuplet с общим упорядочением.

POElement — это общий тип Element с добавлением частичной упорядоченности, тогда как POElement2, POElement3 и POElement4 являются его отдельными изоморфными копиями. Эти типы используются при построении POPair, POThreeTuple и POFourTuple, которые являются кортежами общего вида, расширенными частичной упорядоченностью.

type Generalldentifier

is Boolean

sorts

Identifier

opns

Som'eldentifier : —> Identifier

Anotherldentifier : Identifier —> Identifier

_eq_,_ne- : Identifier, Identifier

—> Bool

eqns

forall

a, al : Identifier

ofsort Bool

Someldentifier eq Someldentifier = true;

Anotherldentifier (a) eq Someldentifier = false;

Someldentifier eq Anotherldentifier(a) =false;

Anotherldentifier(a) eq Anotherldentifier(al) = a eq al; a ne al = not(a eq al);

endtype (* General Identifier *)

type Element2

is Element renamedby

sortnames

Element2 for Element

endtype (* Element2 *)

type Element3

is Element renamedby sortnames

Element3 for Element

endtype (* Element3 *)

type Element4

is Element renamedby

sortnames

Element4 for Element

endtype (* Element4 *)

type Pair

is Boolean, Element, Element2

sorts

Pair

opns

eqns forall

el : Element, e2 : Element2, p, pl : Pair

ofsort Element

First (Pair (el, e2)=el:

ofsort Element2

Second(Pair(el, e2))=e2;

ofsort Bool

p = pl => p eq pl=true;

First (p) ne First (pl) => p eq pl=false;

Second(p) ne Second (pl) => p eq pl=false, p ne pl =not(p eq pl);

endtype (*Pair *) fype ThreeTuple* is Element, Element2, Element3, Boolean sorts

ThreeTuple

opns

Tuple : Element, Element2, Element3 —> ThreeTuple

First : ThreeTuple —> Element

Second : ThreeTuple —> Element2

Third : ThreeTuple —> Element3

_eq_, _ne_ : ThreeTuple, ThreeTuple —> Bool

eqns forall

x, у : ThreeTuple, xl, yl : Element, x2, y2 : Element2, x3, y3 : Element3

ofsort Element

First(Tuple(xl, x2, x3))=xl;

ofsort Element2

Second (Tuple(xl, x2, x3))=x2;

ofsort Element3

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 y=False;

not (Third (x) eq Third (y)) => x eq у = False;

endtype (* ThreeTuple *)

type FourTuple

is Element, Element2, EIement3, Elements Boolean sorts

FourTuple

eqns

forall

xl, yl : Element, x2, y2 : EIement2, x3, y3 : Element3, x4, y4 : EIement4

ofsort Element

First(Tuple(xl, x2, x3, x4))=xl;

ofsort Element2

Second(Tuplefxl, x2, x3, x4))=x2;

ofsort Element3

Third (Tuple(xl, x2, x3, x4))=x3;

ofsort Element3

Fourth (Tuple (xl, x2, x3, x4))=x4;

ofsort Bool

Tuple(xl, x2, x3, x4) eq Tuple (xl, x2, x3, x4)=True;

xl ne yl => Tuple(xl, x2, x3, x4) eq Tuple(yl, y2, y3, y4) p а)

x2 ne y2 => Tuple(xl, x2, x3, x4) eq Tuple(yl, y2, y3, y4)

—

x3 ne y3 => Tuplefxl, x2, x3, x4) eq Tuple(yl, y2, y3, y4) = False;

x4 ne y4 => Tuple(xl, x2, x3, x4) eq Tuple(yl, y2, y3, y4) = False;

Tuplet

opns

TheOne, TheOther

_eq_, _ne_ h

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 OrderedFourTuplet

is FourTuplet

opns

_lt~, —1в—, -ge-,

-gt- : Tuplet, Tuplet —> Bool

eqns

forall

x, у : Tuplet

ofsort Bool

x It y = h(x) It h(y);

x le y = h (x) le h (y);

x ge y = h(x) ge h(y);

x gt y = h(x) gt h(y);

endtype (* OrderedFourTuplet *)

type POElement

is Element

formalopns

_le_, _lt_, -ge_,

_gt_ : Element, Element —> FBool

endtype (* POElement *)

type POElement2

is POElement rfenamedby

sortnames

Element2 for Element

endtype (* POElement2 *)

type POElement3 is POElement renamedby sortnames

Element3 for Element endtype (* POElement3 *) type POElement4 is POElement renamedby sortnames

Element4 for Element endtype (* POElement4 *) type BasicPOPair is Pair actualizedby POElement, POEIement2 using endtype (* BasicPOPair *) type POPair is BasicPOPair

opns

-le,-, _lt-, -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 (y)) => x le у=false;

not (Second (x) le Second (y)) => x le у = false;

x ne у => x It y=x le y;

x eq у => x It у = false;

x ge y = y le x;

xney = >xgty=xgey;

x eq у = >x gt у — false; endtype (* POPair *) type BasicPOThreeTuple is ThreeTuple actualizedby POElement, POElement2, POElement3 using endtype (* BasicPOThreeTuple *) type POThreeTuple is BasicPOThreeTuple opns

_le_, -It-, -ge_, _gt_ : ThreeTuple, ThreeTuple —> Bool eqns

forall

х, у : ThreeTuple ofsort Bool

First (х) le First (у), Second (x) le Second (y), Third (x) le Third (y) = > x le у = 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 le y= false; x n'e у = > x It y = x le y;

x ge y=y le x;

x ne у = > x gt y = x ge y ;

endtype (* POThreeTuple *)

type BasicPOFourTuple

is FourTuple actualizedby POElement, POElement2, POElement3, POElement4 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) => x le у=true; not (First (x) le First (y)) = > x le у=false; not (Second (x) le,Second (y)) =>x le y = false; not (Third (x' le Third (y)) => x le у = false; not (Fourth (x) le Fourth (y)) —> x le y= false;

x ne у = > x It y = x le y;

x ge y = y le x;

x ne у = > x gt y=x ge y; endtype (* POFourTuple *)

• 9 ГЛОБАЛЬНЫЕ ОГРАНИЧЕНИЯ

Определение поведения поставщика услуг разделено на две независимые части: поставщик услуг в режиме-с-установлением-соединения и поставщик услуг в режиме-без-установления-соеди-нения. Определение поставщика услуг в режиме-с-установлением-соединения представлено в сочетании с отдельными ограничениями. TConnections описывается как способный поддерживать потенциально бесконечное число независимых ТС. Каждое ТС представляется отдельным экземпляром TConnection. Получаемая в результате структура показана на рисунке 1. TConnectionless описано в разделе 16. В разделе 10—15 описаны ограничения, относящиеся к транспортным услугам в режиме-с-установлением-соеди-Нений.

Рисунок 1 — Структура услуг транспортного уровня

Примечания

• 1 Каждый экземпляр TConnection может закончиться. Общий TConnections никогда не может закончиться, поскольку всегда существует вероятность того, что будет вызван новый экземпляр его компонента TConnection.

• 2 В любой момент времени может быть активно любое число ТС. Недетер-мннизм поставщика услуг в ограничении этой потенциально бесконечной параллельности специфицируется как отдельное ограничение (см. раздел 14).

behaviour

TSConnectionless [t]

I

TConnections [t] 11 TCIdentification [t] 11

TCAcceptance [t]

II

TBackpressureft]

where process TConnections [t] : noexit : =

TConnection [t] >> stop

III

TConnections [tj endproc (* TConnections *)

• 10 ОБЕСПЕЧЕНИЕ ТРАНСПОРТНОГО СОЕДИНЕНИЯ

Требования к поведению поставщика услуг, связанные с обеспечением одного ТС, распадаются на два класса, а именно ограничения, которые являются локальными для оконечной точки ТС, и межоконечные ограничения. Ограничения первого класса связаны с поведением в оконечной точке ТС в зависимости от истории примитивов, выполненных в этой же оконечной точке ТС. Ограничения второго классе связаны с поведением в оконечной точке ТС в зависимости от истории примитивов, выполненных в другой оконечной точке ТС.

Следует формально определить подходящее понятие «история». В частности, удобно принимать во внимание только те события, которые могут влиять на будущее поведение поставщика услуг, не учитывая, таким образом, те события, которые ни на что больше не влияют: такое понятие известно как «влияющая история». Для локальных ограничений влияющая история представлена состоянием процесса в соответствии с диаграммой переходов состояний, представленной на рисунке 5 ГОСТ 34.960. Для межоконечных ограничений влияющая история представлена параметрами процесса, чья структура и операции формулируются при помощи специально созданного определения типа данных (см. 12.3.2). Эти операции позволяют формулировать требования, соответствующие таблице 1 и рисунку 4 ГОСТ 34.960, способом, не зависящим ог модели.

Локальные органичения представлены двумя независимыми параллельными процессами, представляющими собой два разных экземпляра процесса ТАЕР (см. раздел 11) и соответственно ограничивают взаимодействия с вызывающим и вызываемым пользователями транспортных услуг. TSUserRole определяет роли вызывающего и вызываемого пользователя транспортных услуг. Межоконечные ограничения представлены процессом TCEPAssociation (см. раздел 12), который соотносит индикации, возникающие на каждом конце ТС, с соответствующими запросами, возникающими на другом конце ТС. TSPDirection определяет направления примитивов запроса и индикации в полном соответствии с разделом 5.

Этим процессом специфицируется недетерминированность поставщика, которая влияет на данную взаимосвязь. Кроме того, TCEPAssociation определяет недетерминизм, связанный с выполнением примитивов, генерированных поставщиком.

Примечание — Техническое замечание о завершении: завершение обоих процессов, представляющих концы соединения — явно достаточное представление конца времени жизни этого соединения Вот почему параллельный компонент. содержащий TCEPAssociation. описан (с использованием конструкции [> exit) как способный завершиться в любой момент времени, тогда как TCEPAssociation — бесконечный процесс.

type TSUserRole

is TwoTuplet renamedby

sortnames

TSUserRole for Tuple!

opnnames

CallingRole for TheOne CalledRole for TheOther endtype (* TSUserRole *) type TSPDirection is TwoTuplet renamedby sortnames

TSDirection for Tuplet opnnames

Request for TheOne

Indication for TheOther endtype (* TSPDirection *) process TConnection [t] : exit : =

(TCEP [t] (CallingRole) 111 TCEP [t] (CalledRole))

II

(TCEPAssociation [t] [> exit) endproc (* TConnection *)

(* ..............................................................................................

• 11 ЛОКАЛЬНЫЕ ОГРАНИЧЕНИЯ ДЛЯ ОКОНЕЧНОГО ПУНКТА ТС

  • 11.1 Общее описание

Первые три процесса следующей декомпозиции локальных ограничений на взаимодействия одного ТС в каждой оконечной точке отражают структуру события: это делается с целью отделения ограничений, применяемых к каждому компоненту структуры события,, от ограничений, применяемых к другим компонентам. Четвертый процесс специфицирует ограничение, упомянутое в приме чании к 8.4.1,

process ТСЕР ft] (role : TSUserRole) : exit: = TCEPAddress ft]

TCEPIdentification [t] TCEPSPOrdering [t] (role) TCEPUserData [t] endproc (* TCEP *)

(* _______________________________________________________________________________________________

• 11.2 Адрес и идентификация оконечной точки ТС

Локальные ограничения на адресную и идентификаторную части событий в оконечной точке ТС имеют сходную форму: значение определяется при первом событии совместно с пользователем транспортных услуг, а затем остается постоянным.

Примечание — Завершение обоих процессов допускается в любой момент времени: конец локального (т. е. в оконечной точке ТС) времени жизни ТС на самом деле определяется локальным упорядочением сервисных примитивов (см. 11.3.1).

process TCEPAddress [t] : exit: = t?ta : TAddress ?tcei : TCEI ?tsp : TSP ; ConstantTA [t] (ta) [> exit endproc (* TCEPAddress *)

process ConstantTA [t] (ta : TAddress) : noexit: =

tlta ?tcei : TCEI ?tsp : TSP ; ConstantTA [t] (ta) endproc (* ConstantTA *)

process TCEPIdentification ft] : exit: = t?ta : TAddress ?tcei : TCEI ?tsp : TSP ; ConstantTCEI [t] (tcei) |> exit endproc (* TCEPIdentification *)

process ConstantTCEI ft] (tcei : TCEI) : noexit: = t?ta : TAddress ’tcei ?tsp : TSP ; ConstantTCEI [t] (tcei) endproc (* ConstantTCEI *)

(* _________________________________________________________________________________________

• 11.3 Локальное упорядочение сервисных примитивов в оконечном пункте ТС

  • 11.3.1 Общее описание

TCEPSPOrdering определяет ограничения на возможные последовательности примитивов в одном оконечном пункте ТС (см. рисунок 5 и таблицу 4 ГОСТ 34.960), применяемые к одному ТС.

Поскольку задана спецификация локальных ограничений, постольку в любой момент времени примитивы транспортных услуг, которые могут быть выполнены, зависят только от истории примитивов, выполненных в этом оконечном пункте ТС. Влияющие аспекты этой истории в основном представлены ниже в именах процессов из компонентов TCEPOrdering вместе с некоторыми параметрами.

Фаза установления ТС в оконечном пункте ТС представлена в виде последовательности TCEPConnectl и TCEPConnect2. Это сделано для возможного освобождения ТС даже до успешного установления ТС (предотвращая его таким образом), но только после начала времени жизни ТС. Примитив Т-СОЕДИНЕНИЕ, выполненный в TCEPConnectl, является влияющей историей для TCEPConnect2, поскольку к Т-СОЕДИНЕНИЕ ответ/подтвержде-ние применимы ограничения согласования, которые зависят от Т-СОЕДИНЕНИЕ индикация/запрос.

Успешное установление ТС позволяет войти в фазу передачи информации, которая в каждом оконечном пункте ТС представлена TCEPDataTransfer. Поведение в этой фазе не зависит от роли оконечного пункта ТС. Значение х сообщает результат согласования варианта срочных данных.

Освобождение ТС в оконечной точке ТС состоит из выполнения примитива Т-РАЗЪЕДИНЕНИЕ, как представлено в TCEPRelease. Это может произойти в любой момент времени после первого примитива Т-СОЕДИНЕНИЕ.

Примечание — Последняя альтернатива в определении TCEPSPOrdering введена для обеспечения возможности завершения установления ТС путем освобождения ТС локально в вызывающем оконечном пункте ТС, без выполнения каких-либо примитивов на другом (потенциально но в действительности никогда не наблюдаемом) конце этого ТС.

process TCEPSPOrdering [t] (role : TSUserRole) : exit : = (TCEPConnectl [t] (role) » accept tsp : TSP in

(TCEPConnect2 [t] (tsp) accept x : TEXOption in TCEPDataTransfer [t] (x))

[> TCEPRelease [t])

[ ] [role = Call'edRole] —> exit endproc (* TCEPSPOrdering *) (*....................................................................................

• 11.3.2 Фаза установления соединения в оконечном пункте ТС В 8.4.3.4 дано определение булевой функции IsValidTCON2For, которая представляет требования согласования транспортных услуг. Определение TSUserRole дано в разделе 10.

process TCEPConnectl [t] (role : TSUserRole) : exit (TSP) :== [role = CallingRole]

— >

t?ta : TAddress ?tcei : TCEI ?tcr : TSP [IsTCONreq(tcr) and

(ta IsCallingOf ter)] ; exit (ter)

[ 1

{role = CalledRoIe]

—>

t ?ta : TAddress ?tcei : TCEI ?tci : TSP [IsTCONind (tci) and

(ta IsCalledOf tci)] ; exit (tci) endproc (* TCEPConnectl *)

process TCEPConnect2 [t] (tci : TSP) : exit (TEXOption) : =

t ?ta : TAddress ?tcei : TCEI ?tc2 : TSP [tc2 IsValidTCON2For tci]; (choice x : TEXOption [ ] [x IsTEXOptionOf tc2] —> exit (x)) endproc (* TCEPConnectl *)

(* ..................................................................................

• 11.3.3 Фаза передачи данных в оконечном пункте ТС

process TCEPDataTransfer ft] (х : TEXOption): noexit : = TCEPNormalDataTransfer ft]

III

fx = UseTEX] —> TCEPExpeditedDataTransfer [t]

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 R] endpfoc (* TCEPExpeditedDataTransfer *)

(*_____________________________________________________________________________

• 11.3.4 Фаза освобождения в оконечном пункте ТС

process TCEPRelease ft] : exit : =

t ?ta : TAddress ?tcei : TCEI ?tsp : TSP [IsTDIS (tsp)] ; exit endproc (* TCEPRelease *)

(’..........................................................................................

• 11.4 Ограничения на данные пользователя

Длина параметра данных пользователя в примитивах транспортных услуг ограничивается TCEPUserData, что изложено в 12.2.7; 13.1.13; 13.2.3 и 14.2.2 ГОСТ 34.960, отражаемых здесь.

process TCEPUserData [t] ; exit : =

t ?ta : TAddress ?tcei : TCEI ?tsp : TSP [IsValidUserData(tsp)] ; TSEPUserData [t] [ ] exit

endproc (* TCEPUserData *) type ValidUserData is TransportServicePrimitive opns

IsValidUserData : TSP —> Bool

eqns torall t : TSP ofsort Bool

IsTCON(t) => IsValidUserData (t) = Length (UserData (t)) le NatNum (3 + Dec (2));

IsTDT(t) ==> IsValidUserData (t) = Length (UserData (t)) gt 0; IsTDIS(t) -=> IsValidUserData(t) = Length(UserData(t)) le NatNum (6 +Dec (4));

IsTEX(t)

= > IsValidUserData (t)

= Length (UserData (t) gt 0) and (Length (UserData (t)) le NutNum (1 +Dec(6)));

endtype (* ValidUserData *)

(*...............................................................................

• 12 МЕЖОКОНЕЧНЫЕ ОГРАНИЧЕНИЯ ДЛЯ ОДНОГО ТС

12.1 Общее описание

После выполнения первого запроса TCEPAssociation расщепляется на два экземпляра TAssocl — по одному экземпляру на каждое направление передачи. Эти два экземпляра могут быть созданы независимо и параллельно, поскольку они образуют отдельные части поведения. В самом деле, когда бы один из них ни вызывал взаимодействие, другой не будет вовлечен в это взаимодействие.

ГОСТ Р ИСО/МЭК то 10023—93

Примечание — Начальным взаимодействием по ограничениям может быть только запрос. Это должен быть Т-СОЕДИНЕНИЕ запрос в силу дополнительных локальных ограничений (см. 1132). Разделение между двумя экземплярами корректно только в том случае, если гарантируется, что оконечный пункт, где один из них обрабатывает запросы, является оконечным пунктам, где другой обрабатывает индикации. По этой причине введены параметры адреса, идентификации и направления примитивов в TAssocl (см. 12.2), при помощи которых TAssocl обрабатывает запросы на одном конце ТС и индикации на другом конце.

process TCEPAssociation [t] : noexit : = t ?ta : TAddress ?tcei : TCEI ?tcr : TSP (IsTReq(tcr)J ;

(TAssocl [t] (ta, tcei, Request, Indication, Append (ter, NoTReqs))

III

TAssocl [t] (ta, tcei, Indication, Request, NoTReqs)) endproc (* TCEPAssociation *)

(*_________________________________________________________________________________________

• 12.2 Однонаправленность

TAssocl соотносит индикации, которые могут выполняться на одном конце ТС, с историей запросов, выполненных на другом его конце, учитывая недетерминизм поставщика, влияющий на эту взаимосвязь. Самым сложным подпроцессом TAssocl является TCRecToInd (см. 12.3.1), который представляет межоконечные ограничения, указывающие взаимодействия в t, связанные с примитивами. Параметр TCRecToInd представляет историю запросов, которые соотносятся с возможными будущими индикациями. Определение TCEPHalf, видимо, требует небольшого дальнейшего пояснения: см. в 11.2 ConstantTA и ConstantTCEI, в 8.4.2.1 IsTReq и IsTInd, в 8.3 Tld.

process TAssocl [t] (ta : TAddress, tcei : TCEI, dl, d2, : TSPDirection, rh : TReqHistory) : noexit : = ((TCEPHalf [t] (dl) || ConstantTA [t] (ta) || ConstantTCEI [t] (tcei))

III

TCEPHalf [t] (d2)

II

t?tal .'TAddress ?tcei : TCEI ?tsp : TSP (fid (tai, tceil) ne Tld (ta, tcei)J ; (ConstantTA [t] (tai) || ConstantTCEI [t] (tceil))) || TCReqToInd [t] (rh) endproc (* TAssocl *) process TCEPHalf [t] (dir ; TSPDirection) : noexit : =

[dir = Request]

— > t?ta : TAddress ?tcei : TCEI ?tsp : TSP [IsTReq(tsp)] ; TCEPHalf

Л (dir)

dir = Indication]

—> t?ta : TAddress ?tcei : TCEI ?tsp : TSP (IsTInd(tsp)] ; TCEPHalf

[t] (dir) endproc (* TCEPHalf *)

12.3 Межоконечный недетерминизм

• 12.3.1 Общее описание

Как было сказано выше, TCReqToInd параметризуется историей запросов rh, выполненных на одном конце, которые могут влиять на возможные будущие индикации на другом конце. Значения вида TReqHistory являются основными последовательностями, на которых определены некоторые операции, позволяющие рассматривать только влияющие элементы истории (подробнее см. 12.3.2).

Непосредственная форма определения TCReqToInd — это очень простая праворекурсивная форма. В любой момент времени процесс TSPEvent специфицирует ограничения на следующее наблюдаемое событие; первый параметр TSPEvent — это основа представления недетерминизма (операция Tops определена в 12.3.2). После выполнения этого события TCReqToInd выполняется с обновленным значением параметра.

process TCReqToInd [t] (rh : TreqHistory) : noexit : = TSPEvent [t] (Tops(rh), rh) 5> accept rhl : TReqHistory in TCReqToInd [t] (rhl) endproc (* TCReqToInd *)

• 12.3.2 Определение данных

Первое определение обеспечивает основную конструкцию историй примитивов запроса посредством операций NoTReqs (пустая история) и OnTopOf (для расширения истории более ранним запросом). Также введены еще несколько булевых функций с обычной интерпретацией.

Примечание — Ради полноты OnTopOf нужно определять также и для случая, когда ее первый аргумент — индикация; в этом случае история остает-

ГОСТ Р WCO/МЭК ТО 10023—93

ся без изменения. Этот «безэффектный» подход на индикации соблюдается также и во втором определении

Второе определение расширяет основной тип данных четырьмя операциями, необходимыми для формулировки межоконечных ограничений:

• a) Reduce— описывает историю своего верхнего элемента (т. е. самого раннего по времени выполненного запроса).

• b) Remove — удаляет заданный запрос из заданной истории; если последний имеет далее много экземпляров, то удаляется первый экземпляр.

• c) Append — добавляет запрос к истории в качестве последнего элемента. Заметим, что Append действует как OnTopOf, но с другого конца истории.

• d) Tops — создает историю, состоящую из тех примитивов в аргументе истории, которые могут привести к последующей индикации.

Введены также другие функции, а именно TDISTops и TEXDISTops, для выразительности определения. TDISTops и TEXDISTops дают непосредственные результаты для вычисления Tops.

В соответствии с таблицей 1 ГОСТ 34.960 определен следующий порядок значимости примитивов:

Т-ДАННЫЕ < Т-СРОЧНЫЕ-ДАННЫЕ

< Т-РАЗЪЕДИНЕНИЕ, Т-СОЕДИНЕНИЕ < Т-РАЗЪЕДИНЕНИЕ, причем между примитивами одной услуги нет порядка значимости.

Tops определяется следующим образом: для любого данного значения rh вида TReqHistory, Tops(rh) представляет собой последовательность запросов, которая:

• a) содержит только запросы различных услуг, и

• b) содержит запрос t тогда и только тогда, когда t содержится в rh и все запросы перед ним в rh (т. е. выполненные раньше по времени) являются ниже по значимости, чем t, и

• c) сохраняет порядок запросов в rh.

type TransportServiceBasicTSPRequestHistory

is TransportServicePrimitivc

sorts

TreqHistory

opns

NoTReqs : —> TreqHistory

-OnTopOf- : TSP, TreqHistory —> TreqHistory

: TSP, TreqHistory

: TreqHistory

: TReqHistory, TReqHistory eqns forall t, tl : TSP, h, hl : TReqHistory ofsort TReqHistory

IsTInd(t) = > t OnTopOf h = h;

ofsort Bool

IsEmpty (NoTReqs) =true;

IsTReqft) => IsEmptyft OnTopOf h)=false;

NoTReqs eq NoTreqs = true;

IsTReq (t) => NoTReqs eq (t OnTopOf h) = false;

IsTReq (t) => t OnTopOf h eq NoTReqs = false;

IsTReq (t), IsTReq(tl)

= > t OnTopOf h eq (tl OnTopOf hl) = (t eq tl) and (h eq hl); h ne hl = not(h eq hl);

t IsTopOfNoTReqs = false;

IsTReq(t) = >t OnTopOf (tl OnTopOf hl)=«=teq tl; endtype (* TransportServiceBasicTSPRequestHistory *) type TransportServiceTSPRequestHistory is TransportServiceBasicTSPRequestHistory opns

Reduce : TReqHistory —> TReqHistorv

Remove ; TSP, TReqHistory —> TReqHistorv

Append : TSP, TReqHistory —> TReqHistory

Tops, TDlSTops, TEXDlSTops eqns

forall

t, tl : TSP, h, hl : TreqHistory

ofsort TReqHistory

Reduce (NoTReqs) = NoTReqs;

IsTReq (t) => Reduce(t OnTopOf h)=h;

Remove (t, NoTReqs) = NoTReqs;

t eq tl => Remove(t, tl OnTopOf hl)=h;

t ne tl => 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(t, hl);

Tods (NoTReqs) = NoTReqs;

IsTReq (t), IsTDIS(t) => Tops(t OnTopOf h)=t OnTopOf

ГОСТ Р ИСО/МЭК ТО 10023—93

NoTReqs;

IsTReq(t), IsTEX(t) or IsTCON (t) = > Tops (t OnTopOf h) = t OnTopOf TDISTops(h);

IsTReq(t), TsTDT(t) =>Tops(t OnTopOf h)=t OnTopOf TEXDISTops(h);

TDISTops (NoTReqs) = NoTReqs;

IsTReq(t), IsTDIS (t) =>TDISTops(t OnTopOf h)=t OnTopOf NoTReqs;

IsTReq(t), not (IsTDIS (t)) => TDISTops (t OnTopOf h) = TDISTops (h);

TEXDlSTops (NoTReqs) =NoTReqs;

IsTReq(t), IsTDIS (t) = > TEXDlSTops(T OnTopOf h) =TDISTops(t OnTopOf h);

IsTReq(t), IsTEX(t) => TEXDlSTops(t OnTopOf h)=t OnTopOf TDISTops (h);

IsTReq(t), not(IsTEX(t)), not(IsTDIS(t))

= > TEXDlSTops(t OnTopOf h) =TEXDISTops(h); endtype (* TransportServiceTSPRequestHistory *)

• 12.3.3 Определения процессов

Для заданной истории запросов rh TSPEvent специфицирует ограничения на возможное следующее событие. Параметр erh — это последовательность выполненных запросов, достаточная для определения следующей возможной индикации.

Следующие четыре требования формулируются для обслуживания недетерминизма поставщика в плане его участия в следующем событии.

• a) Поставщик никогда не отказывается участвовать в событии запроса (см. также определение TSPReqEvent ниже).

Примечание — Возможное отклонение запросов определяется процессами TCAcceptance и TBackpressure (см. соответственно разделы 14 и 15).

• b) Может быть выполнена только та индикация, которая относится к верхнему запросу непустой erh, соответствующей IsIndicafionOf (см. 8.4.3.4). Если такая индикация возникает, соответствующий ей запрос удаляется из rh.

Примечание — Для заданного запроса поставщик озаглавливается, чтобы автономно определить значения параметров индикации, при условии, что они удовлетворяют этому требованию.

• c) Для любого заданного верхнего запроса непустого erh поставщик может представить не связанную с ним индикацию только в том случае, если это вызывает участие:

• 1) в индикации, связанной с запросом следующей болей высокой значимости в erh, если таковой существует, или

• 2) в генерированной поставщиком индикации (см. 8.4.3.4).

В случае 1) требования Ь), с) и d) применяются к erh, без его верхнего запроса.

• d) Если пользователь отклоняет индикацию, то должна быть представлена индикация, соответствующая случаям 1) или 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)

[ 1

[not (IsEmpty (erh)) ]

— >

(choice tspr, tspi : TSP

[ 1

[(tspr IsTopOf erh) and (tspi IsIndicationOf tspr)]

—>

*

i ;

(t ?ta : TAddress ?tcei : TCEI itspi ; exit (Remove(tspr, rh)) { 1 i ; TSPEvent [t] (Reduce(erh), rh)))

[ J

[IsEmpty (erh)]

— >

(choice tdi : TSP

[ J

[ProviderGeneratedlnd (tdi)]

—>

i ;

(t?ta : TAddress ?tcei : TCEI !tdi ; exit (rh) [ ] TSPReqEvent [t] (rh)))

endproc (* TSPEvent *)

• 13 ИДЕНТИФИКАЦИЯ ТРАНСПОРТНЫХ СОЕДИНЕНИИ

Любые два разных экземпляра TConnection, которые одновременно имеют доступ к одному ПДУТ, должны быть различимы

ГОСТ Р ИСО/МЭК ТО 10023-93

для пользователя транспортных услуг. Это достигается при помощи идентификатора оконечного пункта ТС — tcei, который передается с каждым сервисным примитивом на каждый ПДУТ. Следовательно, требуется, чтобы:

• a) на любом ПДУТ в любой момент времени никакой tcei не мог быть назначен более чем одному TConnection и

• b) каждый TConnection использовал один и тот же tcei на каждом ПДУТ в течение всего времени существования ТС, который он представляет.

Если последнее ограничение можно специфицировать внутри определения TConnection (см. 11.2), то первое ограничение имеет более глобальный характер и ниже представлено процессом ТС Identification.

Для каждого ПДУТ хранится след используемых идентификаторов оконечного пункта ТС при помощи параметра Use, который является множеством пар вида TId- TAddressxTCEI (см. TCEIdentification в 8.3). Определение TCEIdentifications представляет эти множества Use вначале пустыми. Пара (ta, tcei) находится в Use тогда и только тогда, когда tcei назначается некоторому ТС, имеющему доступ к ПДУТ с адресом ta.

TCIdent позволяет передавать любой запрос или индикацию Т-СОЕДИНЕНИЕ любому заданному ПДУТ с адресом ta только с таким tcei, чтобы пара (ta, tcei) не присутствовала в Use. На другие примитивы это ограничение не налагается, но при выполнении примитива Т-РАЗЪЕДИНЕНИЕ соответствующая пара (ta, tcei) удаляется из Use.

Примечание — Необходимо учитывать следующую техническую деталь Insert(e, s)=(e) U s Следовательно, Insert(e, s)=s всякий раз, когда е С s.

type TCEIdentifications is Set actualizedby TCEIdentification using sortnames

TId for Element Bool for FBool TIds for Set endtype (* TCEIdentifications *) process TCIdentification [t] : noexit : = TCIdent [t] ({ } of TIds) endproc (* TCIdentification *) process TCIdent [t] (Use : TIds) : noexit : = t ?ta : TAddress ?tcei : TCEI ?tsp : TSP (IsTCONl (tsp) implies (TId(ta, tcei) Notin Use)];

(let ti : Tld = TId(ta, tcei) in

[not(IsTDIS(isp))J—> TCIdent [t] (Insert(ti, Use))

[ ]

[IsTDIS(tsp)]—> TCIdent ft] (Remove(ti, Use))) endproc (* TCIdent *)

(*______________________________________________________________________________________________

• 14 ПРИНЯТИЕ ТРАНСПОРТНЫХ СОЕДИНЕНИЯ

В любой момент времени поставщик услуг способен принять установление новых соединений только в конечном множестве пунктов доступа к услугам и в оконечных пунктах соединения. Это определяется процессом TCAcceptance, который внутренне выбирает конечное множество пар (ta, tcei) перед участием в каком-либо взаимодействии. Если взаимодействие образует новое ТС, то оконечный пункт, где произошло это взаимодействие, должен быть среди тех, которые представлены AcceptTC.

Однако при каждом выборе AcceptTC множество оконечных пунктов, где могут быть образованы новые соединения, является в действительности подмножеством AcceptTC, вследствие ограничения разделения на идентификацию ТС (см. раздел 3). Более точно новое соединение может быть образовано только с парой (ta, tcei), которая находится в AcceptTC, а не в Use. Следовательно, при каждом выборе AcceptTC множество оконечных пунктов, где могут быть образованы новые соединения, представлено разностью AcceptTC — Use.

Поставщику транспортных услуг присущ внутренний недетер-минизм при динамическом выборе того, сколько и какие оконечные пункты можно выделить для новых соединений, при условии выполнения минимальных функциональных требований — если нет активных ТС, поставщик услуг должен быть способен принять хотя бы одно ТС, т. е. подмножество AcceptTC, где могут быть действительно приняты новые ТС, должно быть в этом случае непустым.

Примечание — В самом деле, требование минимальной функциональности эквивалентно более простому требованию* чтобы AcceptTC было непустым в любом случае, если принимать во внимание ограничения, наложенные TCIdentification.

Это действительно так, поскольку:

а) если нет активных ТС, то Use пустое, таким образом подмножество AcceptTC, где могут быть приняты новые ТС, является самим AcceptTC, в то время как

ГОСТ Р ИСО/МЭК ТО 16023—93

Ь) если активно несколько ТС, выбор непустого AcceptTC еще допускает, что подмножество, где могут быть приняты новые ТС, может быть пустым, а именно как только AcceptTC включено в Use.

process TCAcceptance[t] : noexit : = choice AcceptTC : Tlds

( 1

[AcceptTC ne { } ]

— >

L;

t?ta : TAddress ?tcei : TCEI ?tsp : TSP [IsTCON19tsp) implies (TId(ta, tcei) Isln AcceptTC)] ;

TCAcceptanceft] endproc (* TCAcceptance *)

• 15 УПРАВЛЕНИЕ ПОТОКОМ ПРИ ПОМОЩИ ОБРАТНОЙ СВЯЗИ

Допускается любой недетерминизм поставщика услуг в отношении приема запросов на передачу данных, но одна зависимость между ограничениями управления потоком для нормальных и срочных данных задана. Эта зависимость вытекает из утверждения 9.2 ГОСТ 34.960, что «нормальные данные... нельзя добавлять в очередь, если их добавление может помешать добавлению срочных ПБДТ...».

Для поддержки абстрактного представления этого требования, и именно только в терминах взаимодействий услуг, вводится параметр MustAcceptTEX, который хранит трассу оконечных пунктов ТС, в которых последним выполненным запросом был запрос Т-ДАННЫЕ. В любой момент времени поставщик может произвольно выбрать конечные множества AcceptTDT и AcceptTEX, представляющие два множества оконечных пунктов ТС, где поставщик может принять нормальные и срочные СБДТ соответственно.

Вышеупомянутая зависимость представлена требованием, что AcceptTEX должен включать MustAcceptTEX. Никакие другие зависимости, которые могут существовать в реализациях услуг транспортного уровня, не описаны.

Примечание — В любой момент времени при динамическом произвольном выборе множества AcceptTDT множество оконечных пунктов, где запросы Т-ДАННЫЕ могут бить действительно приняты, входит в пересечение множеств

AcceptTDT и Use; это точное подмножество AcceptTDT, представляющее оконечные пункты, находящиеся в фазе передачи данных (см. 11.3.1). Аналогичное замечание применимо и при обратной связи срочных данных.

------------------------------------------- _

process TBackpressure [t] : noexit : =

TBackp [t] ({ } of TIds) | 11 RunButTDTreqTEXreqTDIS [t] endproc (* TBackpressure *)

process TBackp[t] (MustAcceptTEX : TIds) : noexit : = choice AcceptTDT, AcceptTEX : TIds

11

[MustAcceptTEX IsSubsetOf AcceptTEX]

—>

i ;

(t?ta : TAddress ?tcei : TCEI ?tdr : TSP (IsTDTreq(tdr) and (TId (ta, tcei) Isln AcceptTDT)] ;

TBackp [t] (Insert(TId(ta, tcei), MustAcceptTEX))

[ J

t?ta : TAddress ?tcei : TCEI ?ter : TSP [IsTEXreq (ter) and (TId(ta, tcei) Isln AcceptTEX)] ;

TBackp [t] (Remove(TID(ta, Tcei), MustAcceptTEX))

t?ta : TAddress ?tcei : TCEI ?td : TSP [IsTDIS (td)] ;

TBackp [t] (Remove(TId(ta, Tcei), MustAcceptTEX))) endproc (*TBackp *) process RunButTDTreqTEXreqTDISft] : noexit : = t?ta : TAddress ?tcei : TCEI ?tsp : TSP (not(IsTDTreq(tsp) or IsTEXreq(tsp) or IsTDIS(tsp))] ;

RunButTDTreqTEXreqTDIS [t] endproc (* RunButTDTreqTEXreqTDIS *)

• 16 ПЕРЕДАЧА В РЕЖИМЕ-БЕЗ-УСТАНОВЛЕНИЯ-СОЕДИНЕНИЯ

16.1 Определения процесса

TSConnectionless основан на индикациях, которые могут выполняться в ответ на ранее выданные запросы. Для описания истории индикаций используется множество.

process TSConnectionless[t] : noexit : =

Connectionless [t] (NoTCIReq)

endproc (* TSConnectionless *) process Connectionless^] (rh : TCIReqHistory) : noexit : =

ГОСТ Р ИСО/МЭК ТО 10023—93

t?ta : TAddress ?tsp : TSP [IsTUDTreq (tsp) and

(Lenght (UserData (tsp))

le MaxTUDTLength)] ; Connectionless [t] (Insert(tsp, rh))

I ]

[rh ne NoTCIReq]

—>

(choice tspr, tspi : TSP

[ 1

[tspr Isln rh and (tspi JsIndicationOf tspr)]

— >

t?ta : TAddress !tspi [ta IsCallingOf tspi] ;

(Connectionless [t] (Remove (trnr, rh))

I J

i ; Connectionless [t] (rh))

[ ]

i ; Connectionless [t] (Remove(tspr, rh)) endproc (* Connectionless *)

16.2 Определения данных

type BasicTransportServiceConnectionlessRecHistory is Set actualizedby TransportServicePrimitive using sortnames

TSP for Element

Bool for FBool

TCIReqHistory for Set

opnnames

NoTCIReq for { }

endtype (* BasicTransportServiceConnectionlessRecHistory *) type MaxTUDTLength

is DecNatRepr

opns

MaxTUDTLength : —> nat

eqns ofsort Nat

MaxTUDTLength = NatNum(6+ (3+ (4+ (8 + Dec(8))))); endtype (* MaxTUDTLength *) endspec (* Transportservice *)

Библиографические данные

УДК 681.324:006.354

Ключевые слова: передача данных, обмен информацией между системами, формализованное описание, услуги транспортного уровня, язык LOTOS, эталонная модель, взаимосвязь открытых систем, типы данных, процессы

ОКСТУ 4002

Редактор В. М. Лысенкина Технический редактор О. Н. Никитина Корректор В. И. Кануркина

Сдано в наб. 1102.94 Подл, в печ 2903.94. Усл. п. л. 3.26. Усл. кр -отт. 3,26. Уч-изд л. 3.07 Тир 374 экз. С 1136.

Ордена «Знак Почегаэ Издательство стандартов. 107076. Москва. Колодезный пер., 14

Калужская типография стандартов, ул. Московская, 256. Зак. 363

¹

До прямого применения данного документа в качестве государственного стандарта его распространение осуществляет секретариат ТК 22 «Информационная технология».