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

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

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

ИНФОРМАЦИОННАЯ ТЕХНОЛОГИЯ

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

LOTOS

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

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

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

Предисловие

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

2    УТВЕРЖДЕН И ВВЕДЕН В ДЕЙСТВИЕ Постановлением Гое-стандарта России от 29.12.93 № 29!)

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

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

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

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

СОДЕРЖАНИЕ

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

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

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

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

5    Соглашения ........

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

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

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

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

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

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

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

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

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

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

16    Передача в рсжиме-бсг-устаноэлеиня-соединечия

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

III

ГОСТ Р ИСОМЭК ТО 10023—93 ГОСУДАРСТВЕННЫЙ СТАНДАРТ РОССИЙСКОЙ ФЕДЕРАЦИИ

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

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

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

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

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

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

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

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

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

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

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

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

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

I

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

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

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

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

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

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

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

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

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

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

5 СОГЛАШЕНИЯ

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

2

ГОСТ Р ИСО МЭК ТО 10023-03

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

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

в ТРЕБОВАНИЯ

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

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

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

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

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

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

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

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

3

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

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

<1) возможности внутреннего недетермннизма при передаче данных (представленной процессом ТВаскрге$йнге. см раздел 15); при помощи этого принимающий пользователь вызывает эффект управления потоком, сообшая об этом передающему пользователю.

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

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

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

specification TransportService|t]: noexit

library Set. Flemeni, OctetSlring, NatRepresenlaiion, jNatiiralNum-

ber, Boolean. FBoolean. DecNalRepr

endlib

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

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

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

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

В ГОСТ 34.960 не определена структура транспортного адреса. Следующее определение использует определение Generalldentifier

4

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

{см. 8.7) и позволяет представлять бесконечное число транспортных адресов.

type Transport Address

is GeneraHdentifier renamedby

sortnames

TAddress for ideniifier opnnames

SomeTAddress. for Someldcntifier AnotherTAddress for Anotherldentifier endtype (* Trans port Address *)

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

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

type TCEndpointIdentifier is GeneraHdentifier renamedby sortnames

TCEI for identifier opnnames

SomeTCEl for Somtldentifier AnotherTCEl for Anotherldentifier endtype (■* TCEndpointfdentifier *) type TCEIdentification

is Pair actualizedby TransportAddress, TCEndpointfdentifier using sortnames

TAddress for Element TCEI for Element2 Bool for Fbool Tld for Pair opnnames

TId for Pair

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

ТА (or First TCEI for Second endtype TCEJdentificaiion *)

♦

8.4 Сервисный примитив транспортного уров-ii я (Т S Р)

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

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

П р и w е ч а к к с — В некоторых TCP параметр L’serDala представляет совой OctetSlring, имеющий фиксированные границы, хак определено » ГОСТ М 960 По техническим соображениям это требование формально представлено процессом ограни'*енм* (см 11.1 и 114), а не ограничивающим типом.

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

б

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

endtype (* BasicTSP *)

‘ Г_____________________________________________________________

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

8.4.2.! Базовая классификация

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

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

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

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

Примечание — Вспомогательная функция h. отображающая имена TCP на натуральные числа» определяется для упрощения спецификации булевых операций равенств на именах TCP (так же, как на TCP в 8.4 3.3) Определение fsRequesf. Islndicatfon (на именах TCP) я IsTrcq. -IsTind (на TCP) отражает соглашение, введенное в раздел 5.

type TSP’Subsort is NaturalNumber sorts

TSPSubsort

opns

TCONNECTrequest. TCONNECTindication. TCONNECTres-ponse. TCONN'ECTconfirm. TDATArequest, TDATAindica-tion. TEXDATArequest, TEXDATAindication, TD1SCONN-request, TDISCONNlndicalion, TlJDATArequest, TUDATA-indication    :    —> TSPSubsort

h    :    TSPSubsort    •    ->    Nat

E\en, Odd    :    Nat    —>    Bool

(sRequest, vindication    : TSPSubsort    —>    Bool

_eq_._ne_    :    TSPSubsort,    TSPSubsort

—> Boo!

eqns

foral!

s, si ?• TSPSubsort, n : Nat ofsort Nat

h (TCONNECTrequest) =0;

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

b (TCONNECTindication) = Succ (h (TCONNECTrequest)); h (TCONNECTresponse) = Succ (h (TCONNECTindication)); h(TCONNECTconfirm)-Succ(h(TCONNECTresponsc)); h (TDATArequest) =Succ(h (TCONNECTconfirm)); h (TDATAindication) = Succ (h (TDATArequest)); h( TEXDATArequest) = Succ (h (TDATAindication)); h (TEXDATAindication) = Succ (h (TEXDATArequest));

Ji (TDISCON Nrequest) = Succ(h (TEXDATAindication)); h (TDISCONNindication) = Succ (h (TDISCONNrequest)); ofsort Bool

Even (0) =true;

Even (Succ (0)) — false.

Even (Succ (Succ (n))) — Evfcn(n);

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

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

5 eq sl = h(s) eq h(sl); s ne sl«not(s eq si); endtype (* TSPSubsort *) type TSPBasicClassifiers is BasicTSP, TSPSubsort opns

Subsort    : TSP    —> TSPSubsort

IsTCON. IsTCONl. lsTCON2. IsTDT, IsTEX. IsTDIS, IsTCONreq, IsTCONind. fsTCONresp. IsTCONconf. IsTDTreq, IsTDlSind, IsTReq. IsTInd : TSP —> Boo!

cqns

foraJI

a. al. a2 : TAddress, x : TEXOption. q : TQOS, d : OctetString. r : TDISReason, t : TSP. clq CLQOS oisort TSPSubsort

Subsort(TCONreq(aI, a2. x. q. d)) -TCONNECTrequest; Subsort (TCONind (a 1, a2. x. q. d)) «TCONNECTindication;

Subsort (TCONresp (a, x. q. d)) = TCONNECTresponse; Subsort(TCONconf(a, x, q. d)j = TCONNECTconfirm; Subsort (TDTreq (d)) *- TDATArequest;

Subsort (TDTind (d)) - TDATAindication;

Subsort (TEXreq (d))» TEXDATArequest;

Subsort (TEXind (d)) = TEXDATAindication;

Subsort (TDI Srcq (d)) = TDISCONNrequest;

Subsort (iTDISind (r, d)) =TDlSCONNindfcatioft;

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

Subsort (TUDTreq(aI, а2, clq, d)) =TUDATArequest;

Subsort (TUDTind (a I, a2. clq, d)) =TUDATAindication; ofsort Bool

IsTCON <t) -«IsTCONI (t) or lsTCON2(t);

JsTCONI(t)-IsTCONreq(t) or !sTCONind(l);

IsTCON2(<)"IsTCONresp(t) or JsTCONconf(t);

IsTDT(t) = IsTDTreq(t) or IsTDTind(t);

IsTEX(t) = IsTEXreq(t) or IsTEXiiid(t);

IsTDlS(t) = IsTDlSr'eq(t) or IsTDISind <t>;

IsTCONreq(t)-^Subsort(t) eq TCON'NECTrequest;

IsTCONind(t)-Subsort(t) eq TCONNF.CTindication;

IsTCONresp(t) =Subsort(t) eq TCONNECTresponse;

IsTCONconf(t) = Subsort (t) eq TCONNECTconfirtn;

IsTDTreq(t) =Subsort(t) eq TDATArequest;

IsTDTind(t)— Subsort (t) eq TDATAindication;

IsTEXrcq(t) - Subsort (t) eq TEXDATArequest;

IsTEXind(t)“Subsort(t) eq TEXDATAindication;

IsTDISreq(t) - Subsort (t) eq TD1 SCON N request;

IsTDISind(t) =-Subsort{t) eq TDlSCONNindication;

IsTUDT(t) — IsTUDTreq(t) or IsTUDTind(t);

IsTUDTreq(t) —Subsort(t) eq TUDATArequest;

IsTUDTind (t) - Subsort (t) eq TUDATAindication;

IsTReq (t) - IsRcquest (Subsort (t));

IsTFnd(t) - vindication (Subsort (t)); endtype (*TSPBasicCla$sifiers ⁴)

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

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

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

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

3 Зак. 363    9

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

8.5.2 4 Вероятность отказа

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

Failures - Prob*

type TCFaiJureProbabilities

is POFourTuple actualized by Probability using

sorlnanies

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 TCResiduaJErrorRate

is POPair actualizedby NaturalNurnber using

sortnames

TPRER for Pair Nat for Element Nat for Element2

20

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

Bool for FBool opnnames

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 4

С_______________________

8.5.4    Защита TC

Упорядоченное множество из четырех констант представляет варианты зашиты, определенные в 10.9 ГОСТ 34.960.

_щ)

type TCProtection

is OrderedFourTuplet renamedby

sortnames

TCProtection for Tuplet opnnames

NoProtection for TheOne Monitoring for TheOther Manipulation for TheThird FullProtection for ThfcFourth endtype (* TCProtection *)

<*__________________________

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

В типе Probability вид Prob задает интервал действительных чи*

ГОСТ Р ИСО «ЭК ТО 10023—93

сел [0, 11 вместе с элементом Undefined, который представляет отношения. не входящие в этот интервал.

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

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

type Probability

is Natural Number    ........ ....._r

sorts

Prob

opns

-I-    :    Nat. Nat    —    >    Prob

Undefined    :    >->    Prob

-eq___ne_,..le ,

-It ...ge-^gt. : Prob, Prob    —> Bool

eqns

foral!

ni, n, j, k : Nat, p. q : Prob ofsori 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 Ic k, n ne 0, k no 0 = >m/n le (j / k) = (m * k) lc (J * n);

m le n, nncO=> Undefined le (m/n)= false; p le Undefined = true: p It q= (p le q) and notfq le p); p eq q= {p le q) and (q le p); p ne q = not (p eq q); p f?e q —q le p;

p q- (p ge q) and not (q ge p); endtype (• Probability •}

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

type DTDirfcctionQOSPar

is POPair actualized^ NaluralNumbcr using

sortnames

Mat for Element Nat for Element2 DQOSP for Pair Bool for FBool opnnames

FromCalling for First FromCallcd for Second DQP for Pair endtype (* DTDirectionQOSPar •) type DTRateDirectionQOSParameter is POPair aetualizedby DTDirectionQOSPar using sortnamfes

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 aetualizedby 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 Параметры сервисных примитивов транспортного уровня

Вариант срочных данных и параметры причины разъединении в TSP определяются типами TEXOption и TDISReason соответственно. Структура параметра КУ определена в 8.5 посредством

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

TSQuality. Другими типами параметров TSP являются TAddress (см. 8.2) к OctefString (даиные пользователя), которые импортируются из библиотеки типов данных LOTOS (см. раздел 7).

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

type TEXOption

is TwoTuplet renamed by

sortnames

TEXOption for Tuplct opnnames

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

TDlSReason for Tuplet opnnames

User for TheOne Provider for TheOther endtype (♦ TDlSReason *)

(*______________________________

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

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

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

PORIement — это общий тип Element с добавлением частичной упорядоченности, тогда как POElement2, POE!emcnt3 и POEIement4 являются его отдельными изоморфными копиями. Эти типы используются при построении POPair, POThreeTuple и

24

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

POFourTuple. которые являются кортежами общего вида, расширенными частичной упорядоченностью.

type Generalldentifier

is Boolean

sorts

Identifier

opns

Someldentifier    —> Identifier

Anotherldentifier    : Identifier    —> Identifier

~eq-._ne~    : Identifier, Identifier

—> Bool

cqns for all

a, al    Identifier

ofsort Bool

Someldentifier eq SomeIdentifier=true;

Anotherldentifter(a) eq Someldentifier-false; . Someldentifier eq Anotherldentifier (a)—false; Anotherldentifier (a) eq Anotherldentifier (a 1) =a eq al; a ne al = not(a eq al); endtype (* Generalfdfcntifier *) type Element2 is Element renamedby sortnames

Element2 for Element endtype (* Element2 *) type Element3 is Elemfent renamedby sortnames

EIement3 for Element endtype (• Element3 *) type Element4 is Element renamedby sortnames

Elomcnt4 for Element    *

endtype (• Element4 *) type Pair

is Boolean. Element. Element2 sorts

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

eqns

forall

el : Element. e2 : E!ement2. p. pi : Pair ofsort Element

First (Pair(cl, e2)—el: ofsort Element2

Second (Pair <el, c2))=»c2; ofsort Bool

p = pl => p eq pl=truc;

First (p) ne First (pi) =>p eq pi = false:

Second(p) ne Second(pl) => p eq pl=falsfe; p ne pl=not(p eq pi); endtype ("Pair *) fype ThreeTuple ’

is Element, Element2, Element3. Boolean sorts    '

ThreeTuple

opns

Tuple    :    Element. E!emenf2, EIement3 —>    ThreeTuple

First    :    ThreeTuple    —>    Element

Second    :    ThreeTuple    —>    Elements

Third    :    ThreeTuple    — >    Element3

~cq-_t -ne~ : ThreeTuple. ThreeTuple    —> Bool

cqns

forall

x. у : ThreeTuple. ж 1. yl : Element. x2, y2 : E!ement2, x3. y3 : Elcment3 ofsort Element

First (Tuple(xl. x2, x3))-xl; ofsort Elemenl2

Second (Tuple (x 1. x2, x3)) = x2; ofsort Elemfcnt3

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 (у)) «»>x eq y — False;

not (Second (x) eq Second (y)) «> x eq у «False;

not (Third (x) eq Third (y)) »> x eq y-False;

26

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

endtype (* ThrecTuple *) type FourTuple

is Element, Eiement2, Element3, Element4, Boolean sorts

FourTuple

opns

Tuple : Element, Eleinent2, Elemenl3, Element-1

—> FourTuple

First    :    FourTuple

Second    :    FourTuple

Third    :    FoureTupIe

Fourth    :    FoureTupIe

_eq.. _ne_ : FourTuple, FourTuple —> Bool

eqns

forall

xl. yl : Flemfent, x2, y2 : Element2, x3. v3 : Elemenl3, x4, y4 : Elements ofsort Element

First(Tuple(xl. x2, x3, x4))—xl; ofsort Element2

Second(Tuple(xl. x2. x3. x4))—x2; ofsort Elcmfent3

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

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

x3 ne y3 *> Tuple (xl, 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; endtype (* FourTuple *) type TwoTuplet Is Boolean, NaturalNumbfcr sorts

Tuplct

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

eqns

foralt

u, v : Tuplet ofsort Nat

h(TheOne) »0;

h(TheOther) — Succ(h(ThcOne)); ofsorl 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

cqns

ofsort Nat

h (TheThird) - Succ (h (TheOthcr)); h (TheFourth) «Succ (h (TheThird)); endtype (* FourTuplet *) type OrdercdFourTuplet is FourTuplet    m

opns

_lt_, -!e-, -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_, -It-. -ge_,

_gt_ Element, Element —> FBool

endtype (• POElement ")

type POElement2

is POElement rfenamedby

sortnames

Element2 for Element

h)CT P H CO/M ЭК TO 10023—M

endtype (* POElement2 *) type P0Element3 is POElement renamedby sortnamcs

Element3 for Element endtype (* POE!ement3 •) type POEIement4 is POElement renamedby sortnames

Eiement4 for Element endtype (* POElement4 *) type BasicPOPair

is Pair actualizedby POElement, POElement2 using

endtype (*. BasicPOPair *)

type POPair

is BasicPOPair

opns

-It-, -ge-,

-gt- : Pair, Pair —> Bool

eqns

fora 11

x, у Pair ofsort Bool

First(x) le First(y), Second(x) le Second(y) = >x le y= true;

not (First (x) ie First (y)) -> x le у * false; not (Second (x) le Second (y)) «> x le y=falsfc; x ne у •«> x It y—x le y; x eq у =•> x It у=false; x ge y = y le x; x ne у = > x gt y—x ge y; x eq у = > x gt y= false: endtype (* POPair *) type BasicPOThreeTuple

is ThreeTuple actualizedby POElement. POEIement2, POElement3 using

endtype (* BasicPOThreeTuple *) type POThreeTuple is BasicPOThreeTuple opns

_le_, -It-, -ge-, _gt_ : ThreeTuple, ThreeTuple —> Bool

feqns

forall

ГОСТ Р ИСО/МЭК то 1&023-5W

х, у ThreeTuple ofsort Bool

First (x) le First (y), Second (x) le Second (y), Third (x) le Third (y) = > x le y = irue; 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; x nfc у => 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 POEIement, 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 (у)) -> x le у «false; not (Third (x) le Third (y)) — > x le у «false; not (Fourth (x) le Fourth (y)) = > x le у «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 ГЛОБАЛЬНЫЕ ОГРАНИЧЕНИЯ

Определение поведения поставщика услуг разделено на две независимые части: поставщик услуг в режиме-с-установлением-соединения и поставщик услуг в режимебез-установления-соеди-нення. Определение поставщика услуг в режнме-с-установленнем* соединения представлено в сочетании с отдельными ограничения-

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

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

СО

..... ..... -)

behaviour

TSConnectionless [t]

III

TConnections ft] 11 TCIdentification (t] 11 TCAcceptance [t]

TBackpressure[t]

where

process TConnections [t]

31

foct P ИСб/МЭК то 10023-М

TConnection [t] >> slop

III

TConnections |tj endproc (* TConnections

Г________________________________________

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

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

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

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

32

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

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

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

_г)

type TSUserRole is TwoTuplel renamedby sort names

TSUserRole for Tuplet opnnames

CallingRoIc for TheOne CaUedRole for TheOther end type (* TSUserRole *) type TSPDirection is TwoTuplet renamedby sortnames

TSDirection for Tuplet

opnnames

Request for TheOne

Indication for TheOther

endtype (• TSPDirection *)

process TConnection [t] : ex И : —

(TCEP [t] (CallingRole) |J| TCEP ft) (CaUedRole))

II '

(TCEPAssociation ft] |> exit) endproc (* TConnection *)

Г______________________________________

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

II.I Общее описание

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

33

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

process ТСЕР |t] (role : TSUserRolc) : exit: —

TCEPAddress ft]

J| TCEPIdcntification It]

11 TCEPSPOr dering [t] (role)

11 TCEPUserData [t] endproc (* TCEP *)

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

ТС

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

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

--------------------------------------------------- *)

process TCEPAddress [t] : exit: =

t³ta : TAddress ?tcei : TCEI ?tsp : TSP ; ConstantTA [t] (ta)

[> exit

endproe (* TCEPAddress *)

process ConstantTA [tj (ta : TAddress) :    noexit    :    =

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

t?ta : TAddress ?tcei : TCEI ?tsp : TSP ; ConstantTCEI [t] (tcei)

|> exit

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

(* J______________________________________________

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

II.3.1 Общее описание

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

34

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

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

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

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

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

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

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

> accept tsp : TSP in

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

. [> TCEPRelease [ф f ] [role-CalledRole] —> exit endproc (• TCEPSPOrdering *)

(* _________________________________

11.32 Фаза установления соединения в оконечном пункте ТС В 8 4.3.4 дано определение булевой функции lsValidTCON2For,

35

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

которая представляет требования согласования транспортных услуг. Определение TSUserRole дано в разделе 10.

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

t?la : TAddress ?tcei : TCEI ?tcr : TSP (IsTCONreq(tcr). and (ta IsCallingOf ter)] ; exit (ter)

lrolc«*CalledRole]

t ?ta : TAddress ?tcei : TCEI ?tci : TSP [IsTCONind(tci) and (ta IsCalledOf tci)j ; exit (tci) endproc (* TCEPConnectl *)

process TCEPConnect2ltl (tel : TSP) : exit (TEXOption) t ?ta : TAddress ?tcei : TCEI ?lc2 : TSP ftc2 IsVaIidTCON2For tell;

(choice x : TEXOption [ ] [x IsTEXOptionOf tc2] -> exit (x)) endproc (* TCEPConnect2 *)

С________________________

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

---------------------------₉₎

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

III

lx = UseTEXl —> TCEPExpeditedDataTransfer [t]

endproc (* TCEPDataTransfer *)

process TCEPNormalDataTransfer ft] : notxlt : —

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 ft] : exit : =

t ?ta : TAddress ?tcei : TCEI ?tsp : TSP [IsTDlS(tsp)] ; exit.

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

fcndproc {* TCEPRelease *)

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

process TCEPUserData Ш ; exit ; *

t ?ta : TAddress ?tcei : TCEl ?tsp : TSP [IsValidUserData (tsp)] ;

TSEPUserData [t] [ ] exit endproc TCEPUserData •) type ValidUserData is TransportServicePrimitive opns

IsValidUserData    ;    TSP    —> Bool

eqns

forall

t : TSP

oCsort Bool

IsTCON(t) *=> IsVaJidUscrData(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)) !e NatNum (6 + Dec (4));

IsTEX(t)

= > IsValidUserData (t)

~ Length (UserData(t) gt 0) and (Length(UserData(t)) le NutNum (I + Dec(6)));

endtype (• ValidUserData *)

Г_____________;_____

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

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

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

37

ГОСТ Р ИСО.'МЭК ТО !ОС23—93

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

process TCEPAssociation [tj : noexit : — t ?ta : TAddress ?tcei : TCEI ?tcr : TSP f IsTReq (ter)] ;

(TAssucI [t] (ta, tcei, Request, indication, Append (ter, NoTReqs))

I¹1 ■

TAssocl ft] (ta, tcei, Indication, Request. NoTReqs)) endproc (⁴ TCEPAssociation ")

Г__________________________________________________

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

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

----------------------------------------_Щ)

process TAssocl [t] (t3 : TAddress, tcei : TCEI, dl, d2. : TSPDirection. rh : TReqHistory) : noexit : «

((TCEPHalf ft] (dl) II ConstantTA [t] (ta) || ConstantTCEI ft] (tcei))

TCEPHalf'|t] (d2)

t?taI . JAddress ?tcci : TCEI ’tsp : TSP lfld(tal. tceil) ne Tld (ta. tcei)] ; (ConstantTA [t] (tal) || ConstantTCEI ft] (tceil))) || TCReqToInd It] (rh) endproc (* TAssocl •)

process TCEPHalf [t] (dir : TSPDirection) : noexit : —

38

ГОСТ Р ИСОМЭК ТО 10023-03

[dir-Request)

•—> t?ta : TAddress ?tcei : TCE1 ?tsp : TSP (IsTReq(tsp) J ; TCEPHalf t] (dir)

dir = Indication]

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

It] (dir)

endproc (* TCEPHalf •)

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

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

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

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

process TCReqToInd [t] (rh : TreqHistory) : noexit : —

TSPEvent (t] (Tops(rh), rh) > accept rhl : TReqHistory in TCReqToInd ft) (rhl) endproc (* TCReqToInd •)

r______________________________________________

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

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

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

¹    39

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

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

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

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

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

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

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

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

В соответствии с таблицей I ГОСТ 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

40

I

ГОСТ P ИСО/МЭК TO 10029—§3

-IsTopOf.    : TSP, TreqHistory    —> Bool

IsEmpty    : TreqHistory    —> Boo!

_cq., ,ne_    : TReqHistory. TReqHistory    —> Bool

eqns

forall

t, tl : TSP. h. hi : TRcqHistory of sort TReqHistory IsTInd(t) => t OnTopOf h=»h; ofsort Bool

IsEmpty (NoTReqs) = true;

IsTReqft) => lsEmpty(t 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 hi) —(t eq tl) and (h eq hi); h ne hi =not(h eq hi); t IsTopOfNoTReqs = false;

IsTReq(t) - > t OnTopOf (tl OnTopOf hi) —t eq tl; endtype (* TransportServiceBasicTSPRequestHistory *) type TransportServiceTSPRequestHistory is TransportServiceBasicTSPRequestHistory opns

Reduce    :    TReqHistory    ;    —> TReqHistory

Remove    : TSP, TReqHistory —> TRcqHistoi v

Append    : TSP. TReqHistory — > TReqHistory

Tops. TDISTops. TEXDISTops

; TReqHistory    —> TReqHistory

eqns    ___

forall

t, tl : TSP. h. hi : TreqHistory

ofsort TReqHistory

Reduce (NoTReqs) = NoTReqs;

IsTReq (t) — > Reduced OnTopOf h)=h;

Remove(t. NoTReqs) =* NoTReqs; t eq II —> Remove(t. tl OnTopOf hi) = h;

t ne tl -> Remove(t, tl OnTopOf hi) — tl OnTopOf Remove(t. hi); i Append (t. NoTReqs) =t OnTopOf NoTReqs;

IsTReq(t 1) => Append(t, tl OnTopOf hl)=tl OnTopOf Append(t. hi);

Tops (NoTReqs) = NoTReqs;

I$TReq(t), IsTDIS(t) Tops(t OnTopOf h)«t OnTopOf

«I

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

NoTReqs;

IsTReq (t), IsTEX(t) or IsTCON(l) *>Tops(( OnTopOf h) —• f OnTopOf TDISTopsfh);

isTReq(l). 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), nol(IsTDIS(t)) = > TDISTops(t OnTopOf h) -TDISTops(h);

TEXDISTops(NoTReqs) = NoTReqs;

IsTReq(t). UTDlS(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(lsTDIS(t))

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

* *    * /

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

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

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

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

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

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

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

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

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

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

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

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

d) Если пользователь отклоняет индикацию, то должна быть представлена индикация, соответствующая случаям 1) или 2) требования с)

process TSPReqEvent [t] (rh : TReqHistory) : exit (TReqHistory) : = t?ta : TAddress ?tce₍ : TCEI ?tsp : TSP [IsTReq(tsp) J ; exit (Append (tsp. rh)) endproc (* TSPReqEvent *)

process TSPEvent [t] (erh.rh : TReqHistory) : exit (TReqHistory) : = TSPReqEvent ft] (rh)

(not(IsEmpty(erh))]

— >

(choice tspr. tspi : TSP

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

—> i ;•

(t ?ta : TAddress ?tcei: TCEI Itspi: exit (Remove(tspr, rh)) f 1 j ; TSPEvent [t] (Reduce(erh), rh)))¹

[IsEmpty(erh)]

—>

(choice tdi : TSP    '

[ProviderGeneratedlnd (tdi)]

—>

i ;

(t?ta : TAddress ?tcei : TCEI ltdi ; exit (rh) [ ] TSPReqEvent ft] (rh))}

endproc (“ TSPEvent *)

______________________________________________

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

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

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

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

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

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

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

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

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

Примечание — Необходимо учйтывать следующую техническую деталь: lnser«(e. s>-{e} U s. Следовательно, lnsert(c. s)-s эсяхий раз, когда е С s.

— .. ,, . - *

type TCEldentifications

is Set actualizedby TCEldentification «sing

sortnames

TId for Element

Bool for FBool

TIds for Set

endtype (* TCEldentifications *) process TCIdentification [t] : noexit : =

TCIdent ft] ({ ) of TIds)

endproc (* TCIdentification *)

process TCIdent (t] (Use : TIds) : noexit

t ?ta : TAddress ?tcei : TCEI ?tsp : TSP JIsTCONl (tsp) Implies (TId(ta, tcei) Notln Use)];

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

(id ti : Tid = Tld(ta. tcei) in

(not(IsTDJS(isp>)] — > TCIdent [t] (Insert(ti. Use))

[IsTDIS(tsp) | —> TCIdent |tj (Remove(ti, Use))) endproc (* Ttldent *)

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

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

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

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

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

ТС Identification.    ¹

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

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

45

I

/

гост p исо'.мэк то 16023—da

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

Use.

---------------------------------------------_¥)

process TCAcceptanceJt] : noexit : = choice AcceptTC : TIds

(AcceptTC ne { } ]

—>

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

TC Accept ance[tj endproc (• TC Accept a nee ⁴)

15 УПРАВЛЕНИЕ ПОТОКОМ ПРИ ПОМОЩИ ОБРАТНОЙ СВ*ЦИ

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

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

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

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

Л

ГОСТ P ИСО/МЭК TO 10023—M

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

-------;-----------------------♦)

process TBackpressure {tj : noexit : —

TBackp [1] ({ } of TIds) 111 RunButTDTreqTEXreqTDIS [t] endproc (* TBackpressure **)

process TBackpItl (MustAceeptTEX : TIds) : noexit: — choice AcceptTDT, AcceptTEX : TIds

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

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

TBackp [(] (Remove(TID(la, Tcei), MustAcceptTEX))

t?ta : TAddress ?tc€i .-TCEI ?td : TSP [IsTDIS(td)] ;

TBackp [t] (Removc(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 *)

c----:______________._

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

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

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

process TSConnectionlessft] : noexit:-Connectionless ft] (NoTClReq) endproc (* TSConnectionless •)

process Connectionless^] (rh : TCIReqHistory) : noexit: —

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

t?ta : TAddress ?tsp i TSP [isTlr'DTreq (tsp) and (Lenght (UserData (tsp))

le MaxTUDTLength)] ; Connectionless [t] (Insert(tsp, rh)J 1 rh ne NoTCIReqJ —>

(choice tspr, tspi TSP

[tspr Isln rh and (tspi IsIndicationOr tspr)]

t?ta : TAddress !tspi [ta lsCallingOf tspij ;

(Connectionless [(] (Remove(tsor, rh))

I I

i ; Connectionless^] (rh))

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

r_________₇_____

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

type BasicTransportServiceConnectionlessRecHistory

Is Set actualizedby TransportServicePrimitlve 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 •)

48

ГОСТ Р НСО.МЭК ТО 10023—93

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

УДК 681.324:006.354    П85

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

ОКСТУ 4002

49

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

Сдйхо > иаб. II 09.94. Пади. • п«ч 29.0>.9». Уел. п л З.’Л. Уел кр огг. 3.2в. Уч-нха я 3.07 Тир S74 w С 113*

Ор*ем1 «Зиан Почет*» Имательетао стаиаартоа. I070?t». Москм. КолодезиыА вер . 14 Калужская лшечрафиа «иаидарто». ул. Мосдосхая, 20в- За*. 363