Моделирование сети автоматов

Введение

1 Описание взаимодействия автоматов

2 Описание программного продукта

2.1 База данных

2.1.1 Представление автоматов в БД

2.1.2 Представление очередей в БД

2.1.3 Представление графа достижимости в БД

2.2 Назначение основных модулей программы

2.3 Работа с файлами

3 Описание основных алгоритмов и методов

3.1 Построение дерева достижимости

3.2 Просмотр дерева и определение особых состояний сети

3.3 Работа с очередями

3.4 Контроль параметров автомата при вводе

Перечень ссылок

ВВЕДЕНИЕ

1 ОПИСАНИЕ ВЗАИМОДЕЙСТВИЯ АВТОМАТОВ

Автоматом будем называть объект А = (S, X, Y, D , s ), где S – конечное непустое множество состояний, s  - начальное состояние, X - конечное непустое множество входных символов, Y - конечное непустое множество выходных символов, D Н Sx(XИY)xS - множество переходов.    

Введем множество Z =XИY, z О Z – входной либо выходной символ.

Автомат удобно представить в виде конечного ориентированного графа, где состояния автомата – вершины графа, D - множество переходов – множество дуг графа, где каждый переход (s  , z, s  ) понимается как дуга, помеченная входным или выходным символом z , исходящая из s  и входящая в s  .

Автомат функционирует в дискретном времени {1, 2, 3, 4, 5,..}.

Функционирование автомата заключается в том, что он осуществляет переходы: если на его входе есть символ x и он находится в состоянии s  , то он может прочесть x и перейти в s  , где (s  , x, s ) О D ; автомат может выдать на выход символ y и перейти в s  где (s , y, s ) О D .В каждый момент времени автомат осуществляет только один переход.

Сетью из двух автоматов назовем четверку (A, B, a, b) , где A, B – автоматы, a, b – очереди типа FIFO, причем Y  ОX  , Y ОX  . Сеть автоматов изображена на рис. 2.1.

Pиc. 2.1 - Сеть автоматов

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

Конфигурацией или состоянием сети назовем четверку (s, t, a , b ), где s и t – текущие состояния автоматов А и В соответственно, а a и b - слова, находящиеся в очередях a и b соответственно.

Функционирование сети описывается (возможно, бесконечным) графом, который называется графом достижимости сети G(A, B). Его вершинами являются всевозможные конфигурации (состояния сети), а дугами – четверки (K , z, f,K ) где K  = (s , t , a  , b  ), i=1, 2 – конфигурации, a   -слово в алфавите X , b   - слово в алфавите X , f О {A,B}, для которых :

1. если z О X и f = A, то слово a =za и (s, z, s) О D , t=t, b =b
2. если z О X и f = B, то слово a =a z и (t, z, t) О D , s=s b =b
3. если z О X и f = A, то слово b =b z и (s, z, s) О D , t=t a =a
4. если z О X и f = B, то слово b =zb и (t, z, t) О D , t=t, a =a

Начальным состоянием графа G(A,B) объявляется состояние (s , t , e, e), где s ,t  - начальные состояния автоматов A и B соответственно, е – пустое слово (в любом алфавите).

Состояние сети (s, t, a , b ), где из состояния s автомата А и из состояния t автомата B выходят только принимающие дуги, и a = b = e, назовем тупиковым состоянием сети. Состояние сети (s, t, a , b ), где из состояния s автомата А выходят только принимающие дуги, и a = xg , где символ x не является отметкой ни одной принимающей дуги, исходящей из состояния s  , называется состоянием несанкционированного приема. Аналогичное определение строится для автомата B.

Взаимодействие пары автоматов A и B назовем ограниченным, если существует k такое, что для каждой вершины графа достижимости G(A, B) длина слов в очередях Ј k.

Одной из основных проблем логического анализа корректности протоколов является следующая проблема : определить для произвольных A, B , существуют ли в G(A, B) :

1. тупики ( проблема тупиков);
2. несанкционированное чтение (проблема несанкционированного чтения);
3. является ли взаимодействие ограниченным (проблема ограниченного взаимодействия).

2 ОПИСАНИЕ ПРОГРАММНОГО ПРОДУКТА

2.1 База данных

• A, B – автоматы;
• a, b – очереди типа FIFO.

2.1.1 Представление автоматов в БД

Оба автомата A и B, хранящиеся в памяти, имеют тип TAutomate, который представляет собой структуру, показанную в таблице 2.1.

Таблица 2.1 – структура типа TAutomate

Максималное количество состояний автомата, задается константой MNS (MaxNumStates).

2.1.2 Представление очередей в БД

Обе очереди a и b, хранящиеся в памяти, имеют тип TQue, который представляет собой массив символов.

В БД имеются две переменные, связанные с очередями:

• MaxQLen (целое) – максимальная длина очереди, может изменятся пользователем;
• QueOverflow (логическое) – индикатор переполнения очереди.

2.1.3 Представление графа достижимости в БД

Граф достижимости представляется в БД в виде динамической структуры – дерева. Каждый узел этого дерева имеет тип TNode, который представляет собой структуру, показанную в таблице 2.2.

Таблица 2.2 – структура типа TNode

Максималное количество выходящих дуг, задается константой MNC (MaxNumCrosses).

Конфигурация сети (тип TСross), представляет собой следующую структуру:

• s,t (целые) - текущие состояния автоматов А и В соответственно,
• Qa,Qb (TQue) - слова, находящиеся в очередях a и b соответственно.

• Z (символ) – символ, по которому осуществляется переход;

• Io (логическое) – true, если Z – входной символ;

false, если выходной.

• q (символ) – ‘A’ или ‘B’, в зависимости от того, с какой очередью взаимодействует автомат.

2.2 Назначение основных модулей программы

• Main – это основной модуль программы, содержащий описание главного окна программы, и связывающий между собой все остальные модули;

• Tree – содержит функции создания и удаления дерева достижимости и записи его в файл;
• Automate - содержит описание типа ТАutomate и процедуры сохранения в файле и загрузки из него параметров автоматов;
• AutoEdit - содержит описание окна редактирования автоматов и функции контроля параметров автомата при вводе;
• Queues, QueLen - содержит описание типа ТQue и функции для работы с очередью (добавление, удаление, чтение).

2.3 Работа с файлами

Информация об автомате заносится в текстовый файл, поэтому имеется возможность редактирования его с помощью текстового редактора. Файл автомата имеет расширение aut.

Если при запуске программы в текущей директории обнаружены файлы с именами “a.aut” и “b.aut”, то они загружаются по умолчанию.

Параметры автомата заносятся в файл в следующей последовательности:

• NumStates
• BegState
• NumX,NumY
• X,Y – через пробелы
• Все переходы Cr[i,j] в виде: i j [-]Cr[i,j].z ( ‘-‘ ставится, если сигнал выходной)

3 ОПИСАНИЕ ОСНОВНЫХ АЛГОРИТМОВ И МЕТОДОВ

3.1 Построение дерева достижимости

Для построения дерева достижимости в программе используется процедура MakeTree (иодуль Tree). Процедура является рекурсивной и имеет следующие аргументы:

• Node: указатель на ТNode;
• Cross: TCross;
• Conf: TConf.

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

При каждом вызове MakeTree динамически выделяется память для узла дерева Node, заполняется конфигурация сети и входящяя дуга для этого узла:

а все выходящие дуги обнуляются:

Дальнейшее создание узлов, выходящих из Node, осуществляется по следующему алгоритму:

n:=1; // № узла в ANode

Если A.Cr[i,j].io=false то

Если QueOverflow то

QueOverflow:=false; выход;

иначе Если A.Cr[i,j].z=ReadFromQue(Conf.Qa) то

…………. // те же действия для автомата B

3.2 Просмотр дерева иопределение особых состояний сети

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

Процедура является рекурсивной и имеет один аргумент:

Node: указатель на ТNode.

При первоначальном вызове в PrintTree в качестве аргумента передается указатель на вершину дерева достижимости.

Дальнейший просмотр узлов, выходящих из Node, с определением особых состояний осуществляется по следующему алгоритму:

Запись в файл конфигурации сети и входящей дуги для узла Node:

// Определение тупиков и несанкц. чтения

Если A.Cr[i,j].io=false то fl:=false;

Если B.Cr[i,j].io=false то fl:=false;

Если fl то

Если (Node^.Conf.Qa='') и (Node^.Conf.Qb='') то

Запись(' - Тупик')

иначе fl:=false; fl2:=false;

Если Node^.Conf.Qa<>'' то

Если A.Cr[i,j].z=ReadFromQue(Node^.Conf.Qa)

то fl:=false;

Если Node^.Conf.Qb<>'' то

Если B.Cr[i,j].z=ReadFromQue(Node^.Conf.Qb)

то fl2:=false;

Если fl или fl2 то Запись(' - несанкц. чтение в ');

Если not fl2 то Запись(f,'A') иначе

Если not fl то Запись(f,'B') иначе Запись(f,'A и B')

3.3 Работа с очередями

В программе используются очереди с дисциплиной обслуживания FIFO. В модуле Queues содержатся некоторые функции для работы с очередями, приведенные в таблице 3.1.

Таблица 3.1 - Функции для работы с очередями

3.4 Контроль параметров автомата при вводе

1. Количество состояний автомата не должно превышать значение константы MNS.
2. Начальное состояние не должно превышать количество состояний автомата.
3. Соответствие входных и выходных сигналов автоматов A и B ( должно выполняться: Y ОX , YОX ).
4. Соответствие между входным или выходным множеством сигналов автомата и сигналами, используемыми в переходах (в переходах могут использоваться только сигналы из входного или выходного множества автомата, при этом, если сигнал – выходной, то перед ним ставится '-').
5. Правильность указания начальных и конечных состояний переходов (все состояния в переходах должны лежать в интервале от 1 до количества состояний автомата).
6. Соответствие между количеством состояний и состояниями, используемыми в переходах.

Ситуации 1 и 2 контролируются непосредственно при изменении параметров, а ситуации 3 – 6 - при нажатии кнопки ‘Ok’ или ‘Trim’.

ПЕРЕЧЕНЬ ССЫЛОК

1. Диксон Г. Дж., Шадаль П. Э. Состояние рассматриваемых МККТТ методов описания и их применение для спецификации протокола //ТИИЭР. – М.: Мир, 1983. –№71. – С. 23 – 23.
2. Пранявичус Г. И. Модели и методы исследования вычислительных систем. – Вильнюс: Монслас, 1982. –228 с.
3. West C. H. General Technique for Communications Protocol Validation // IBM J. Res. Develop. – 1978. – Vol. 22. – P. – 393 – 404.
4. Потапов И. Г. О классе определимых циклических протоколов. // проблемы теор. кибернетики. Тезисы докл. XII межд. конф. часть II.– М. –изд-во ММФ МГУ, 1999 г.–С. 190.
5. Грунский И. С. Контроль неисправностей автомата, заданных оценочной функцией. // Тр. ИПММ НАНУ. Т. 1. "Идентификация и моделирование управляющих систем", 1997 г. – С.38–43.
6. Q. M. Tan, A. Petrenko. Test generation for specifications modeled by input-output automata. // Testing of communicating systems Proc. of the IFIP tc. 6 IWTTS`98, 1998. – P. 83 – 99.