Распространяется на транспортный уровень эталонной модели взаимосвязи открытых систем (ВОС) и определяет услуги транспортного уровня ВОС, определенные в ГОСТ 34.960, при помощи метода формализованного описания LOTOS, определенного в ИСО 8807. Формальное определение типов данных и процессы, представленные в настоящем стандарте, могут использоваться для формализованного описания протоколов транспортного и сеансового уровней ВОС на языке LOTOS.
1 Область применения
2 Нормативные ссылки
3 Определения
4 Символы и сокращения
5 Соглашения
6 Требования
7 Введение в формализованное описание
8 Типы данных на интерфейсе
9 Глобальные ограничения
10 Обеспечение транспортного соединения
11 Локальные ограничения для оконечного пункта ТС
12 Межоконечные ограничения для одного ТС
13 Идентификация транспортных соединений
14 Принятие транспортных соединений
15 Управление потоком при помощи обратной связи
16 Передача в режиме-без-установления-соединения
Библиографические данные
53 страницы
Дата введения | 01.07.1994 |
---|---|
Добавлен в базу | 01.09.2013 |
Актуализация | 01.01.2021 |
29.12.1993 | Утвержден | Госстандарт России | 293 |
---|---|---|---|
Разработан | ТК 22 Информационные технологии | ||
Издан | Издательство стандартов | 1994 г. |
Чтобы бесплатно скачать этот документ в формате PDF, поддержите наш сайт и нажмите кнопку:
ГОСТ Р ИСО/МЭК то 10023-93
ГОСУДАРСТВЕННЫЙ СТАНДАРТ РОССИЙСКОЙ ФЕДЕРАЦИИ
ИНФОРМАЦИОННАЯ ТЕХНОЛОГИЯ
ПЕРЕДАЧА ДАННЫХ И ОБМЕН ИНФОРМАЦИЕЙ МЕЖДУ СИСТЕМАМИ. ФОРМАЛИЗОВАННОЕ ОПИСАНИЕ УСЛУГ ТРАНСПОРТНОГО УРОВНЯ
(ГОСТ 34.960-91) НА ЯЗЫКЕ
LOTOS
БЗ 12-92/1177
Издание официальное
ГОССТАНДАРТ РОССИИ Москва
Предисловие
1 ПОДГОТОВЛЕН И ВНЕСЕН Техническим комитетом по стандартизации ТК 22 «Информационная технология»
2 УТВЕРЖДЕН И ВВЕДЕН В ДЕЙСТВИЕ Постановлением Гос
стандарта России от 29.12,93 № 293 Настоящий стандарт подготовлен на основе применения аутентичного текста международного стандарта ИСО МЭК ТО 10023— 92 «Информационная технология. Передача данных и обмен информацией между системами. Формализованное описание ИСО 8072 на LOTOS»
3 ВВЕДЕН ВПЕРВЫЕ
© Издательство стандартов, 1994 Настоящий стандарт не может быть полностью или частично воспроизведен, тиражирован и распространен в качестве официального издания без разрешения Госстандарта России
И
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));
Islndication (s) — Odd (h (s)); s eq sl = 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, IsTCON2, IsTDT, IsTEX, IsTDIS, IsTCONreq, IsTCONind, IsTCONresp, IsTCONconf, IsTDTreq, IsTDISind, IsTReq, IsTInd : TSP —> Bool
eqns
fo-rall
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(al, 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;
6
ГОСТ Р ИСО/МЭК ТО 10023—93
Subsort (TUDTreq (а 1, а2, clq, d)) —TUDATArequest; Subsort(TUDTind(al, a2, clq, d)) =TUDATAindication; Ofsort Bool
IsTCON(t) = IsTCON 1 (t) or IsTCON2(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 TCONNECT request; IsTCONind (t) = Subsort (t) eq TCONNECTindication; IsTCONresp (t) = Subsort (t) eq TCONNECTresponse; IsTCONconf (t) = Subsort (t) eq TCONNECTconfirm; 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'equest; 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, связывает элементарное выполнение примитивов данных, что характерно для определения услуг, с неэлементарным их выполнением, присутствующим в формализованном описании протокола.
9
ГОСТ Р ИСО/МЭК ТО 10023—93
................................................................................................................*)
type TDATAAtomSubsort is FourTuplet renamedby sortnames
TDATASubsort for Tuplet opnnarnes
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 определены булевы функции. Причина для такого непрямого представления — неполнота определения при помощи равенств.
ГОСТ Р ИСО/МЭК то 10023—93
Единственное исключение имеется в прямом представлении параметра данных пользователя при помощи функции UserData, так как этот параметр можно определить во всех TSP.
*)
type TSPParameterSelectors
is TSPClassifiers
opns
-IsCalledOf-, -IsCallingOf-, -IsRespondingOf- : TAddress, TSP —>Bool
-IsTEXOptionOf TEXOption, TSP —> Bool
-IsTQOSOf- : TQOS, TSP —> Bool
-IsReasonOL. : TDISReason, TSP —> Bool
UserData : TSP —> Octetstring
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 TCONindjal, a2, x, q, d)=a eq al; a IsCalledOf TUDTreq(al, a2, clq, d)=a eq al; a IsCalledOf TUDTind(al, a2, clq, d)=aeq 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 TUDTreq(al, 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 TCONind(al, a2, xl, q, d)=x eq xl x IsTEXOptionOf TCONresp(a, xl, q, d)=x Щ xl x IsTEXOptionOf TCONconf(a, 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;
11
ГОСТ Р ИСО/МЭК ТО 10023—93
г IsReasonOf TDISind(г 1, d)=r eq rl; not(IsTDISind(1)) => г 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
forall
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 11 = 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) *
12
ГОСТ Р ИСО/МЭК ТО 10023-93
(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) = (aeq 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);
TDlSind (r, d) eq TDISind (rl, 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 (Us^rData(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
13
eqns
forall
t, tl : TSP, a, al, a2, a3 : TAddress, x, xl : TEXOption, q, ql : TQOS, d, dl : Octetstring, clq, clql : C1QOS ofsort Bool
PrividerGeneratedlnd (t)
— IsTDISind(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 k q) and (dl eq d);
TCONconf(al, xl, ql, dl) IsIndicationOfTCONresp(a, x, q, d) = (al eq a) and (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 feq 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.
Первая декомпозиция выделяет параметры КУ: производительность ТС, приоритет ТС и защита ТС. Эти структуры определяют'
14
ГОСТ Р ИСО/МЭК ТО 10023—93
ся в 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 *)
15
ГОСТ Р ИСО/МЭК ТО 10023—93
type TSCIQuality
is POFourTuple aclualizedby CLTransitDelay, TCProtection,
Probability, TCPriority using
sortnames
Bool for FBool CLQOS for FourTuple CLTransDelay for Element TCProtection for Element2 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 Failures X Throughput XRER, что представлено в данном ниже определении. Определения компонентов даны в 8.5.2.2—8.5.2.5.
Примечание — Вспомогательные определения КУ (см 8 5.5) полезны для понимания определений параметра производительности, содержащегося в 8 5 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 Ie tl) and (r ge rl);
16
ГОСТ Р ИСО/МЭК ТО 10023-93
pf It pH — (pf le pfl) and not(pfl le pf); pf eq pf 1 = (pf le pfl) and (pfl le pf); pf ne pfl=not(pf eq pfl); pf ge pfl = pfl 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 Element3 TPRER for Element4 Bool for FBool opnnames
Performence for Tuple Delays for First Throughput for Second RER for Third Failures for Fourth £ndtype (* BasicTCPerformance *)
8.5.2.2 Параметры задержки
Параметры задержки имеют следующую структуру тройки:
Delays = EstDelayXTransDeIay xRelDelay, где:
EstDelay = Nat
TransDelay=Nat4
RelDelay=Nat2
EstDelay — вид параметра задержки установления ТС, который имеет линейную структуру (таким образом определена единственная взаимно однозначная проекция).
TransDelay — вид параметра транзитной задержки, который имеет структуру четверки. Каждая проекция представляет транзитную задержку для отдельного направления передачи и скорости (а именно «максимальная» и «средняя», см. 10.3 ГОСТ 34.960). Это определение представлено как переименование вспомогательного определения, приведенного в 8.5.5.
RelDelay — вид параметра задержки освобождения, который имеет структуру двойки. Каждая проекция представляет задержку освобождения ТС для отдельного пользователя ТС (которому
17
ГОСТ Р ИСО/МЭК ТО 10023-93
СОДЕРЖАНИЕ
1 Область применения . . .'.....
2 Нормативные ссылки........
3 Определения ..........
4 Символы и сокращения.......
5 Соглашения.........
6 Требования ..........
7 Введение в формализованное описание
8 Типы данных на интерфейсе.....
9 Глобальные ограничения .......
Ю Обеспечение транспортного соединения
11 Локальные ограничения для оконечного пункта ТС
12 Межоконечные ограничения для одного ТС
13 Идентификация транспортных соединений
14 Принятие транспортных соединений . . . ■
15 Управление потоком при помощи обратной связи
16 Передача в режиме-без-установлсния-соединения
Библиографические данные......
III
ГОСТ Р ИСО/МЭК ТО 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);
18
ГОСТ Р ИСО/МЭК ТО 10023—93
ГОСУДАРСТВЕННЫЙ СТАНДАРТ РОССИЙСКОЙ ФЕДЕРАЦИИ
Информационная технология
ПЕРЕДАЧА ДАННЫХ И ОБМЕН ИНФОРМАЦИЕЙ МЕЖДУ СИСТЕМАМИ. ФОРМАЛИЗОВАННОЕ ОПИСАНИЕ УСЛУГ ТРАНСПОРТНОГО УРОВНЯ
(ГОСТ 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 Системы обработки информации. Взаимосвязь открытых систем. Определение услуг транспортного уровня. Техническая поправка 11.
ИСО/ТО 8509—87 Системы обработки информации1 Взаимосвязь открытых систем. Соглашения по услугам 1.
ИСО 8807—89 Системы обработки информации. Взаимосвязь открытых систем. LOTOS — метод формализованного описания, основанный на упорядочении во времени наблюдаемого поведения 1.
ИСО/МЭК ТО 10024—92 Информационная технология. Передача данных и обмен информацией между системами. Формализованное описание ИСО 8073 (разделы О, I, 2 и 3) на языке LOTOS 1.
3 ОПРЕДЕЛЕНИЯ
В настоящем стандарте используются определения, приведенные в ГОСТ 34.960.
4 СИМВОЛЫ И СОКРАЩЕНИЯ
В настоящем стандарте используются символы, определенные в разделе 6 (формальный синтаксис) и приложении А (библиотека типов данных) ИСО 8807.
В настоящем стандарте используются сокращения, содержащиеся в разделе 4 ГОСТ 34.960. Использование других символов и сокращений поясняется при первом их появлении.
5 СОГЛАШЕНИЯ
Неформальные пояснения, предшествующие формальным определениям, к которым они относятся, отделяются от последних показанной ниже верхней линией. Отделение формальных определений от последующих неформальных пояснений обозначается показанной нижней линией.
ГОСТ Р ИСО/МЭК ТО 10023—93
Примечание — Это соглашение соответствует правилам ограничения комментариев, определенным для LOTOS в ИСО 8807 Формальный текст представлен курсивом, а ключевые слова и операторы LOTOS — полужирным шрифтом. Идентификаторы из форматированного текста в неформатированном тексте набраны курсивом.
Соблюдаются соглашения, определенные в ИСО/ТО 8509, но с учетом следующего: термин «запрос» означает как запросные, так и ответные сервисные примитивы, а термин «индикация» означает сервисные примитивы как индикации, так и подтверждения.
6 ТРЕБОВАНИЯ
Настоящий стандарт отвечает требованиям, изложенным в разделе 3 ИСО 8807 (более подробную информацию см. в приложении С к указанному стандарту). Настоящий стандарт не содержит каких-либо требований к соответствию.
7 ВВЕДЕНИЕ В ФОРМАЛИЗОВАННОЕ ОПИСАНИЕ
Вся граница услуг формально представлена в виде единственного шлюза t. Структура события в t представляет собой тройку значений типа TAddress, TCEI, TSP (см. раздел 8). Первое значение идентифицирует TSAP, в котором происходит взаимодействие. Второе значение идентифицирует ТСЕР внутри TSAP, в котором происходит взаимодействие. Третье значение — это выполняемый при взаимодействии примитив транспортного уровня (TSP). Конкретные значения зависят от многих аспектов услуги.
Описывается поведение поставщика услуг бесконечного вида. Спецификация не содержит параметров.
Используется стиль спецификации, ориентированный на ограничения, поскольку он наиболее подходит для определительного характера стандарта па услугам. Описание ориентировано на характеристики модальностей поведения поставщика услуг исключительно в терминах последовательности выполняемых TSP, т. е. без каких-либо предположений о внутренней структуре самого поставщика.
В основе первой декомпозиции специфицируемого поведения лежат следующие отдельные ограничения:
a) поставщик услуг может допускать множество, возможно, одновременных соединений (представленных процессом TConnections, см. раздел 9), вместе со
b) средством выбора среди одновременных соединений нужного (представленным процессом TCIdentification, см. раздел 13), но при
ГОСТ Р ИСО/МЭК ТО 10023—93
с) возможности внутреннего недетерминизма при установлений любого дополнительного соединения, если, по меньшей мере, одно соединение уже поддерживается (представленной процессом TCAcceptance, см. раздел 14), и
с!) возможности внутреннего недетерминизма при передаче данных (представленной процессом TBacKpressure, см. раздел 15); при помощи этого принимающий пользователь вызывает эффект управления потоком, сообщая об этом передающему пользователю.
Спецификация динамического поведения предваряется спецификацией типов данных на интерфейсе (см. раздел 8). Такие определения являются общими для формализованных описаний, которые могут взаимодействовать, а именно для протоколов транспортного и сеансового уровней.
Порядок представления остальных определений обоснован желанием следовать порядку, установленному ГОСТ 34.960, который в основном связан с обеспечением единственного ТС. Описание требований, являющихся локальными для обеспечения одного ТС (представлены в разделах 10, 11 и 12), предшествуют описаниям глобальных требований, упомянутых выше в Ь), с) и d) соответственно.
Типы данных, определенные конструкцией library, импортируются из библиотеки типов данных LOTOS.
*)
specification TransportService[t]: 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 не определена структура транспортного адреса. Следующее определение использует определение Generalldentifier
4
ГОСТ Р ИСО/МЭК ТО 10023—93
(см. 8.7) и позволяет представлять бесконечное число транспортных адресов.
*)
type TransportAddress
is General I dentifier 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 Element TCEI for Element2 Bool for Fbool TId for Pair opnnames
5
ГОСТ Р ИСО/МЭК ТО 10023—93
ТА for First TCEI for Second endtype (* TCEIdentification *) (*...................................................
8.4 Сервисный примитив транспортного уровня (TSP)
8.4.1 Общее описание
Тип данных TCP представлен, начиная с базовой конструкции значений вида TCP (см. ниже). Эта конструкция является прямой формулировкой определения, приведенного в таблице 3 ГОСТ
34.960. Функции, генерирующие значения ТОР, называются «конструкторами ТСР». Это определение заимствует определения, связанные с параметрами TCP (см. 8.6).
Примечание — В некоторых TCP параметр UserData представляет собой OcietString", имеющий фиксированные границы, как определено в ГОСТ
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
opns
TCONreq, TCONind
: TAddress, TAddress, TEX-Option, TQOS, Octetstring —> TSP
TAddress, TEXOption, TQOS, Octetstring —> TSP : Octetstring —> TSP
: OctfetString —> TSP
: Octetstring —> TSP
: TDISReason, Octetstring —> TSP : TAddress, TAddress, C1QOS,
TCONresp, TCONconf
TDTreq, TDTind TEXreq, TEXind TDISreq TDISind
TUDTreq, TUDTind
6
ГОСТ Р ИСО/МЭК ТО 10023-93
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) Определение IsRequest, vindication (на именах TCP) и IsTreq, IsTind (на TCP) отражает соглашение, введенное в раздел 5
_____________________________________________________________________________________________________________*)
type TSPSubsort is NaturalNumber sorts
TSPSubsort
opns
TCONNECTrequest, TCONNECTindication, TCONNECTres-ponse, TCONNECTconfirm, TDATArequest, TDATAindica-tion, TEXDATArequest, TEXDATAindication, TDISCONN-request, TDISCONNindication, TUDATArequest, TUDATA-indication : —> TSPSubsort
h : TSPSubsort —> Nat
Even, Odd : Nat —> Bool
IsRequest, ^Indication : TSPSubsort —> Bool
_eq_,_ne_ : TSPSubsort, TSPSubsort
—> Bool
eqns
forall
s, si : TSPSubsort, n : Nat ofsort Nat
7
1
До прямого применения данного документа в качестве государственного стандарта его распространение осуществляет секретариат ТК 22 «Информационная технология».
2