РАЗДЕЛ 2
РАЗРАБОТКА ИНСТРУМЕНТАЛЬНЫХ СРЕДСТВ СПЕЦИФИКАЦИИ ПРОТОКОЛОВ УПРАВЛЕНИЯ ИНФОРМАЦИОННЫМ ВЗАИМОДЕЙСТВИЕМ В РТС
Предметом рассмотрения настоящего раздела диссертации являются вопросы построения конечноавтоматной модели протоколов управления распределенными техническими системами и разработки на основе языка регулярных выражений средств спецификации протоколов, обеспечивающих автоматическую реализацию формальных процедур синтеза и анализа последних. Предлагаются концептуальные основы технологии проектирования протоколов, каждый этап которой опирается на использование разработанной конечноавтоматной модели.
2.1. Модель протокола с конечным числом состояний
Рассматривая протокол как набор правил, определяющих функционирование взаимодействующих объектов при передаче данных [99], будем полагать, что система взаимодействий в нашем случае представляется множеством {O1, O2, ... , On} распределенных объектов взаимодействия и передающей средой С. При этом процессы взаимодействия P1, P2, ... , Pn осуществляются путем обмена сообщениями. Каждый из процессов имеет единственное начальное и фиксированное множество конечных состояний. Причиной перехода процесса Pi (i =1,2,...,n) из одного состояния в другое может быть прием сообщения (протокольного примитива), посланного процессом Pj (j ? i) через передающую среду С, посылка сообщения процессу Pj, либо завершение какого-либо внутреннего для Pi события, не связанного с посылкой или приемом сообщений через передающую среду.
Передающая среда С представляет собой совокупность дуплексных каналов связи, обеспечивающих передачу сообщений между парами объектов Oi и Oj (i,j=1,2,...,n; i ? j). Каналы связи Cij и Cji рассматриваются как очереди с определенной дисциплиной обслуживания. Каждая очередь представляется последовательностью сообщений обмена. Первоначально предполагается, что передающая среда идеальна, т.е. функционирует без потерь, искажений, дублирования и нарушения порядка следования сообщений. Считается, что все каналы имеют память, достаточную для того, чтобы обслуживать очереди любой длины.
Рассматриваемая система взаимодействия определяется как асинхронная система взаимодействующих процессов. Другими словами, о времени, которое любой процесс проводит в каком-либо конкретном состоянии перед тем, как послать сообщение, и о времени, которое сообщение проводит в канале перед тем, как быть доставленным тому или иному процессу, не делается никаких предположений.
2.1.1. Основные положения формальной модели протокола с конечным
числом состояний
Концептуально формальную модель протокола с конечным числом состояний представим посредством формулирования основных определений, характеризующих как протокол в отдельности, так и систему взаимодействующих протокольных объектов [10,61,90,129,132].
Определение 2.1. Протокол управления информационным обменом определяется следующей шестеркой компонент:
< S, S0, Sk, M, E, ?>,
где: 1) S = {S1, ... ,Sn } - множество конечных множеств состояний процессов P1,...,Pn; sji ? Sj (j = 1,2,...,n) - i-е состояние процесса Pj ;
2) S0 = {s10, ... ,sn0} - множество начальных состояний процессов P1, ..., Pn ; si0 ?Si;
3) Sk = {S1k, ... ,Snk} - множество конечных состояний процессов P1, ..., Pn ; Sik ? Si ;
4) M = ??Mi,j ??n x n - матрица протокольных примитивов (сообщений),
где Mi,j - множество сообщений, которые могут быть посланы от Pi к Pj (Mi,i = ? для всех i = 1,2,...,n; mki,j - сообщение mk, принадлежащее множеству Mi,j);
5) E = ??Ei,j ??n x n - матрица событий;
Ei,j - множество событий, элементом которого могут быть:
а) посылка процессом Pi сообщения mk ? Mi,j процессу Pj (обозначается
"-mk" ),
б) прием процессом Pi сообщения mk ? Mi,j от процесса Pj (обозначается
" + mk "),
в) внутреннее событие, не связанное с посылкой или приемом сообщений (обозначается ? );
6) ? : S?E ? S - функция переходов системы, ? = (?1, ?2,..., ?n),
где ?i - функция переходов конечного автомата, моделирующая процесс Pi ;
sik = ?i (sil, eri,j ) обозначает переход процесса Pi из состояния sil в состояние sik в случае наступления события eri,j .
Если eri,j =-mr то ?I характеризует посылку процессом Pi процессу Pj сообщения mr. В случае eri,j =+ mr функция ?I характеризует переход процесса Pi из состояния в состояние, вызванный приемом процессом Pi сообщения mr от процесса Pj..
Следует отметить, что определение функции ?i обобщается и на последовательность событий, т.е., если T? = e1, e2, ... ,ek последовательность событий длины k (k = 1,2,...) и T=T?е, то ?i (s,T) = ?i (?i (s,T?),е).
Определение 2.2. Каналы Ci,j и Cj,i , обеспечивающие обмен сообщениями между процессами Pi и Pj , определяются как бесконечные очереди с определенной дисциплиной обслуживания, например, FIFO (первый пришел - первый обслуживается).
Очереди ci,j и cj,i - это последовательности сообщений из Mi,j и Mj,i. Считается, что ?ci,j ? ? ?ci,j ?max, где ?ci,j ? и ?ci,j ?max - соответственно длина очереди и максимально возможная длина очереди сообщений для канала Ci,j. Величина ?ci,j ?max ограничивается пропускной способностью канала Ci,j, однако на практике для любой пропускной способности всегда можно рассчитать необходимый объем памяти, чтобы считать канал способным обслуживать очереди любой длины [98]. Кроме того предположим, что канал в некотором смысле "идеальный", т.е. такие события, как потери, искажения, повторы, нарушения порядка следования сообщений в нем невозможны. Неидеальные каналы можно промоделировать введением специальных событий для каналов. В этом случае канал также следует рассматривать как процесс с конечным числом состояний.
Определение 2.3. Глобальные состояния системы взаимодействия есть пара , где S =