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

Рис. 5 Сервисная точка доступа

Зачастую введение одного или нескольких SAP определяет использование дополнительных стандартных модулей для организации межслоевой коммуникации. Это позволяет вынести функции создания примитивов и чтения данных из примитивов из самого модуля SAP. Графическое изображение модуля SAP показано на рис. 5.

Предикатом срабатывания модуля обозначим R_SAP.

R_SAP(prim₁, prim₂) = ,

где prim_i - примитив, поступивший на i-й интерфейс модуля (i={0,1}). Срабатывание модуля происходит при поступлении примитивов на один или оба интерфейса, каждый из которых связан с разными портами. Затем примитивы со всеми содержащимися в них данными записываются в очередь FIFO, с которой связан интерфейс, на который этот примитив пришел. На следующем такте модельного времени данные передаются дальше через соответствующий порт.

Доказана необходимость и достаточность данного набора модулей для моделирования описанного класса протоколов.

Архитектурная диаграмма может быть использована для генерации «скелета» программной модели на языке SystemC. Однако для генерации программной модели недостаточно просто построить архитектурную диаграмму, необходимо также проверить эту диаграмму на наличие определенного класса ошибок, способных нарушить работу программной модели.

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

1. ошибочная постановка связи порт/интерфейс;

2. ошибочное описание вызываемого метода С++ класса;

3. ошибочное указание или отсутствие описания данных в методе;

4. отсутствие названия порта;

5. отсутствие названия интерфейса;

6. отсутствие названия метода С++ класса;

7. отсутствие названия модуля;

8. отсутствие связи порт/интерфейс;

9. повторное название интерфейса в рамках программной модели;

10. повторное название модуля в рамках программной модели;

11. повторное название порта в рамках одного модуля;

12. повторное название метода С++ класса в рамках одного модуля.

Любая спецификация протокола, соответствующая вышеописанным требованиям, содержит описание протокола по уровням. Для каждого уровня присутствует описание функциональности, которую этот уровень обеспечивает в рамках работы протокола. На основе этого описания при проектировании архитектурной диаграммы программной модели определяется количество и назначение используемых модулей. Количество моделируемых уровней протокола формирует количество IM модулей, количество описанных задач, выполняемых каждым уровнем, формирует количество CM модулей, используемых для моделирования уровня. Для выполнения каждой отдельной задачи предусматривается отдельный модуль программной модели, выбранный из определенного в диссертации набора модулей. Если какая-либо задача уровня включает накопление данных в рамках одного модуля, то вместо CM - используется DC или SC модуль. Если между уровнями в спецификации описаны сервисные точки доступа - для них используется модуль SAP.

Таким образом, для каждого уровня формируется множество модулей Y, в котором содержатся имена модулей. Каждое имя должно быть уникально в рамках программной модели.

Y={y₀, y₁, y₂,…, y_x} (1)

Спецификация протокола описывает данные, которые являются входными и выходными для уровней протокола. То есть имеется описание pdu (protocol data unit) относительно каждого из уровней (формат пакета, сегмента, кадра и т.п.). Следовательно, из спецификации можно определить формат данных, поступающих на вход модели, и получаемых на выходе. Далее, в зависимости от задач, выполняемых протоколом на том или ином уровне, определяется, меняются ли данные при прохождении через тот или иной модуль, или нет. Если данные меняются - можно выделить новый тип данных, идущий на выход модуля и, соответственно, дальше по модели. Так составляется множество данных, которые должны присутствовать в модели.

D={d₁, d₂, d₃,…,d_n} (2)

Это множество данных может быть дополнено в процессе дальнейшего проектирования архитектурной диаграммы.

На основе полученных множеств модулей и данных составляются две таблицы:

· Таблица требований спецификации, в которой отражается, в какие модули должны попасть те или иные данные;

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

Таблица 1. Таблица требований спецификации

В Таблице требований спецификации отражены сведения, какие данные a_i, согласно спецификации, должны попасть в какие модули y_j. Каждому данному из множества D присваивается свой номер и ставится в соответствующий столбец. Данные в столбец «Модули» ставятся в зависимости от того, входными для каких модулей эти данные являются по спецификации. Модулей для одного данного может быть указано несколько, если данные идут маршрутом через несколько модулей, или идут по нескольким модулям параллельно. Пример такой таблицы показан в Таблице 1.

По результатам данной таблицы составляются множества модулей X, в которых должны побывать данные. Если поле в столбце «Модули» пустое, то для этого данного a_i множество X_i также будет пустым. Например,

X₀ = {y₀, … y_n}; (для а₀) (3)

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

y_x: {z₀, z₁, …, z_n} (4)

Для каждого метода С++ класса ставится признак, говорящий о выполняемых им функциях. По признаку, поставленному в первом столбце таблицы, методы для каждого модуля делятся на два множества: входящие и исходящие. Например,

In(y₀)={ z₀, z₁,…, z_m} (5)

Out(y₀)={ z_m+1, z_m+2,…, z _m+n}

Данные, которые передаются или принимаются при помощи этого метода С++ класса, заносятся в третий столбец таблицы. Это делается на основе вышеопределенного множества D. Например,

A(y_x, z_m) = {a₁, a₂, …, a_n} (6)

Затем необходимо определить и обозначить порты и интерфейсы модулей. Например,

B(y_x) = {if₁, if₂, …, if_i}

B(y_x+1) = {port₁, port₂, …, port_i} (7)

Если порт связан с интерфейсом, то вызываемая портом и предоставляемая интерфейсом функция - это один и тот же метод. Соответственно, они будут иметь одно и то же название в таблице.

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

Если выполняется условие

 (8)

тогда для метода С++ класса z_n в модулях y_x и y_t ставится одна числовая метка g. Для портов, не связанных ни с каким интерфейсом числовые метки не ставятся; аналогично для интерфейсов, не связанных с портами. Если порт связан с несколькими интерфейсами или наоборот, интерфейс - с несколькими портами, то одинаковая числовая метка также ставится для всех портов и интерфейсов. Это описывает те случаи, когда данные параллельно отправляются в несколько модулей архитектурной диаграммы и дальше работа осуществляется в параллельных потоках.

G = {g₀, g₁, …, g_n} (9)

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

Рис. 6 Пример вида архитектурной диаграммы

Пример окончательного вида таблицы взаимодействий отображен в Таблице 2.

Подобная таблица предоставляет основные данные, необходимые для создания архитектурной диаграммы:

1) Названия модулей;

2) Методы С++ классов, отвечающие за межмодульное взаимодействие, и их названия;

3) Названия портов и интерфейсов между модулями;

4) Методы С++ классов, которые должны быть описаны в соответствующих интерфейсах;

5) Взаимосвязи между портами и интерфейсами;

6) Данные, необходимые для верификации архитектурной диаграммы.

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

· отсутствие названия порта;

· отсутствие названия интерфейса;

· отсутствие названия метода С++ класса;

· отсутствие названия модуля;

· отсутствие связи порт/интерфейс;

· повторное название интерфейса в рамках программной модели;

· повторное название модуля в рамках программной модели;

· повторное название порта в рамках одного модуля;

· повторное название метода С++ класса в рамках одного модуля.

Остальные потенциальные ошибки обнаруживаются в архитектурной диаграмме путем ее верификации. Такой метод верификации описан в третьей главе диссертации.

Таблица 2. Таблица взаимосвязей (пример)

После построения таблицы взаимосвязей добавляются данные во множество D. Данные, отсутствующие во множестве, но присутствующие в столбце «Данные» таблицы взаимосвязей, добавляются во множество D.

D={type₁ data₁,type₂ data₂,type₃ data₃,…,type_m data_n} (10)

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

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

Сеть Петри - это набор

N = (Р, Т, F, W, M₀)

где P - конечное множество позиций;

Т - конечное множество переходов;

F - конечное множество дуг.

А W: F > N\{0} и M₀: P > N -- две функции, называемые соответственно кратностью дуг и начальной разметкой.

Раскрашенная сеть Петри - это кортеж

Т =(У,P,T,F,K,C,G,E,I)

где У - конечное множество цветов;

K - функция позиций, ставит в соответствие каждой дуге пару, состоящую из связанных с ней перехода и позиции;

C - функция цвета, представляет собой список цветов, определенных для каждой позиции;

G - предохраняющая функция, представляет собой список булевых выражений, связывание перехода должно удовлетворять каждой из этих функций (может быть не определена или быть true для всех переходов)

E - функция выражений дуг, определяется по означиванию выражения дуги, определенного на множестве цветов для конкретной позиции;

I - функция инициализации позиций, ставит в соответствие каждой позиции переменную, определенную на множестве цветов (может быть определена как конкретный цвет или отсутствовать);

Предложен метод построения раскрашенной сети Петри по архитектурной диаграмме программной модели протокола. Это позволяет описать структуру модели формальными методами, а так же применить их для анализа архитектурной диаграммы и её верификации. Метод включает в себя ряд шагов для составления раскрашенной сети Петри, а так же алгоритм для ее маркировки.

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

1) каждому модулю y_n, участвующему в передаче данных, сопоставляется позиция сети Петри p_n;

2) каждому вызываемому С++ методу и передаваемым с его помощью данным z_x(a_y) по связи порт-интерфейс сопоставляется свой переход t_y (в том случае, когда метки g в таблице взаимосвязей в модулях совпадают (G(y_x,z_n)=G(y_t,z_n)));

3) порту () сопоставляется дуга к переходу;

4) интерфейсу () сопоставляется дуга из перехода;

5) комбинации (тип данных, имя переменной), которые должны быть переданы от модуля к модулю (a_y), задают цвета дуг, фишек и позиций;

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

1. Каждой дуге a сопоставляется не выражение, а одна переменная, отвечающая за цвет фишки, по которой данный переход сработает. Таким образом, по одной дуге фишки разных цветов ходить не могут;

2. Каждому переходу t сопоставляется не выражение, а так же, как и в предыдущем случае, цвет фишки;

3. Функция позиций I также будет содержать лишь данные о цвете и количестве фишек, поставленных в конкретную позицию;

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

После составления сети Петри на основе данного метода, необходимо ее разметить. В соответствии с множеством D (формула 10) и порядковым номерам таблицы требований, каждой комбинации (тип данных, имя переменной) присваивается свой цветной маркер, однозначно идентифицирующий это данное среди других. Переходу, где осуществляется только вызов метода С++ класса без передачи каких-либо данных в модуль (<вызов>), фишки не присваиваются и он не анализируется в процессе проверки. Для примера с рисунка 6 распределение цветов показано в Таблице 3.

Таблица 3. Распределение цветов

Пример построенной раскрашенной сети Петри показан на рисунке 7а.

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

P_m - множество позиций для разметки (до начала выполнения алгоритма P_m=P);

P_next - множество позиций, в которые осуществляется переход из текущей позиции;

С_m - множество уже поставленных цветов (до начала выполнения алгоритма C_m= Ш);

С(t_out) - множество цветов, определенных для переходов из текущей позиции;

С - полученное множество цветов фишек, которые ставятся в текущей позиции;

Разметка раскрашенной сети Петри производится, начиная с позиции, соответствующего модулю SAP архитектурной диаграммы или определенного разработчиком как точка начала разметки, по следующему алгоритму:

1) Определяется, в какие позиции P_next осуществляется переход из текущего p_i;

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

C = С(t_out)\ C_m (11)

3) Во множество C_m записываются новые цвета, определенные для данной позиции.

C_m = C_m?С (12)

4) Обновляется множество неразмеченных позиций

P_m=P_m\p_i (13)

5) Определяются позиции для осуществления следующего перехода:

P_next=P_m ? P_next (14)

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

a. Если P_next=Ш, то останавливается дальнейшая разметка этой ветви;

b. Если нет, то переходим к разметке позиций, определенных в P_next, начиная для каждого из них с п.1;

Алгоритм разметки останавливается, когда нет новых мест для осуществления перехода. Конечность алгоритма доказана.

После проведения разметки получим раскрашенную маркированную сеть Петри, которую можно применять для анализа архитектурной диаграммы и, следовательно, работы и поведения программной модели. Пример разметки такой сети с рисунка 7а показан на рисунке 7б. Разметка начата с позиции p₀.

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

Таким образом, с учетом вышеописанных замечаний, алгоритм построения сети Петри, эквивалентной раскрашенной, выглядит следующим образом:

1. Каждой позиции p в раскрашенной сети Петри Т сопоставляется столько позиций в эквивалентной сети Петри N, сколько цветов в C(p). После такого преобразования в сети Петри N можно различать фишки, которые в Т имеют разные цвета. Фишки в N утрачивают свой цвет, но они размещаются в разных позициях;

2. каждый переход t раскрашенной сети Петри Т без изменений становится переходом классической сети Петри N;

3. если срабатывание перехода t раскрашенной сети Петри Т удаляет хотя бы одну фишку из позиции p, то дуга из этой позиции p в переход t ставится в классической сети Петри N;

4. если срабатывание перехода t раскрашенной сети Петри добавляет хотя бы одну фишку в позицию p, то дуга из перехода t в позицию p ставится в классической сети Петри N;

5. количество фишек для каждой позиции сети Петри N ставится в соответствии с количеством фишек соответствующего цвета, определенным начальной маркировкой M₀ раскрашенной сети Петри Т.

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

Рис. 7. Пример раскрашенной сети Петри, построенной по архитектурной диаграмме с рисунка 6

В тексте диссертации приведено доказательство следующих теорем.

Теорема 3.1: При построении классической сети Петри N из раскрашенной сети Петри Т, полученной из архитектурной диаграммы программной модели протокола передачи данных по предложенному алгоритму, раскрашенная сеть Петри Т преобразуется в несколько классических сетей Петри N₀…N_x-1 по признаку цвета из У.

Теорема 3.2: Классические сети Петри N₀…N_x-1, полученные из раскрашенной сети Петри Т по предложенному алгоритму, не имеют общих дуг F, позиций P и переходов T.

Теорема 3.3: Алгоритм построения набора классических сетей Петри, дает набор сетей Петри N₀…N_x-1, который эквивалентен раскрашенной сети Петри Т.

Дальнейший анализ может проводиться для каждой полученной сети Петри в отдельности. Таким образом, к раскрашенной сети Петри, полученной из архитектурной диаграммы, можно применять методы анализа классических сетей Петри.

Пример разбиения раскрашенной сети Петри с рисунка 7б на несколько классических сетей Петри показан на рисунке 8.

Рис. 8. Пример разбиения раскрашенной сети Петри с рисунка 7б на набор классических сетей Петри

Рис. 9. Деревья достижимости, построенные для набора классических сетей Петри с рисунка 8

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

После построения дерева достижимости для каждой из классических сетей Петри, полученных по вышеописанному алгоритму, анализируются вершины этих деревьев достижимости. Каждой из вершин дерева достижимости соответствует маркировка сети Петри от M₀ (начальной маркировки) до M_j. Например, маркировка 00201 показывает, что две фишки находятся в позиции p₂ и одна фишка в позиции p₄. Для каждой из вершин дерева достижимости составляется множество позиций Щ, в которых находятся фишки. Таким образом, для n вершин дерева достижимости будет Щ₀…Щ_n-1 множеств. Из этих множеств для каждой ветви дерева достижимости составляется множество достижимости Q по следующей формуле:

(15)

Каждое множество Q ^f_i содержит данные о том, в какие позиции попала фишка цвета c, пройдя по маршруту f. Или соответственно, в терминологии архитектурных диаграмм, в какие модули попали данные, соответствующие цвету c. Например, для рис. 10:

Q⁰₀ = Щ₀Щ₁={p₀}{p₁}={p₀, p₁} (16)

Здесь возле обозначения Q нуль в верхнем индексе означает номер ветви в дереве достижимости, а нуль в нижнем индексе - номер данных в таблице требований.

Исходя из вышеописанных принципов построения сетей Петри на основе архитектурных диаграмм, каждая позиция p_i сети Петри соответствует модулю y_j архитектурной диаграммы. Также, фишки, ходящие по каждой классической сети Петри N_m, соответствуют определенному типу данных a_n. Поэтому, на основе полученных множеств Q может осуществляться верификация архитектурной диаграммы программной модели протокола передачи данных.

Каждая позиция p во множестве Q замещается связанным с ним модулем архитектурной диаграммы y. Таким образом, множество Q⁰₀ преобразуется в

Q⁰₀ = {y₀, y₁} (17)

На основе множеств Q, полученных из ветвей деревьев достижимости, и множеств X, полученных из таблицы требований, для каждого цвета c осуществляется верификация архитектурной диаграммы.

Для каждого цвета c_i=a_i ставятся в соответствие множество X_i и множества Q ^f_i. Далее для каждого маршрута f определяется множество модулей, по которым прошли и в которые не попали данные типа a_j по формуле:

Д ^f_i = X_i \ Q^f_i (18)

Если Д=Ш, то это означает, что данные определенного типа, пройдя маршрутом f, попали во все требуемые модули. Таким образом, верификация была завершена без ошибок.

Если же Д?Ш, то в результате в множестве Д оказывается набор модулей, в которые данные a_j не попали, пройдя маршрутом f. Если для данных a_j нет такого маршрута, идя по которому данные попали во все требуемые модули, то в построении архитектурной диаграммы допущена ошибка.