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

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

Таким образом, в результате верификации будет получено некоторое количество множеств Д₀… Д_b. Каждое из этих множеств показывает те модули y₀…y_m, в которые не попали данные a_i. Таким образом, анализ показывает, какие требования спецификации, отраженные в таблице требований, не выполнены. На основе этого делаются выводы о необходимых изменениях в архитектурной диаграмме.

Например, возьмем сетевой уровень протокола, который должен проверять сетевой адрес пакета. Для этого по спецификации он должен получить примитив, говорящий о пришедшем пакете, из канального уровня через SAP, затем проверить адрес пакета. Если адрес верный, то в пакете отбрасывается заголовок сетевого уровня и передается в SAP транспортного уровня. Если адрес неверный, то пакет отбрасывается. Таким образом, нужно 4 модуля: SAP сетевого и транспортного уровня (y₀ и y₃), модуль проверки адреса (y₁), модуль отбрасывания сетевого заголовка пакета (y₂). Отсюда видно, что пакет проходит по пути y₀> y₁> y₂. Допустим, что при составлении архитектурной диаграммы была допущена ошибка, и не был предусмотрен C++ метод, передающий данные типа «пакет» из y₁ в y₂. Следовательно, анализ архитектурной диаграммы покажет, что данные типа «пакет» прошли по маршруту y₀> y₁ и не попали в модуль y₂. Из этого разработчик увидит несоответствие между архитектурной диаграммой и спецификацией протокола.

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

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

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

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

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

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

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

· программная модель уровня PHY Adapter стека протоколов UniPro;

· программная модель уровня PHY стека протоколов UniPro;

· программная модель Символьного уровня протокола SpaceWire;

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

Рисунок 10. Внешний вид программы ESPMS.

Также в четвертой главе приведено описание инструментально-программного комплекса ESPMS (Embedded Systems Protocols Modelling Software), разработанного с использованием разработанных методов и алгоритмов, предложенных в диссертационной работе (рис.10). Система ESPMS описана на языке С++ с помощью Qt. Она выполняет следующие функции:

· построение архитектурных диаграмм при помощи встроенного редактора;

· анализ архитектурной диаграммы сетями Петри в соответствии с методом, изложенным в главе 3.

Разработанная в данной диссертационной работе методика позволила уменьшить время написания программной модели и снизить трудозатраты на реализацию. В качестве примера в работе приведены результаты проекта по написанию программной модели протокола передачи данных для встроенных систем UniPro. Методика, представленная в данной диссертации, уменьшила трудозатраты на написание программной модели на 40%.

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

Основные результаты работы

1. Разработан метод проектирования и анализа программных моделей протоколов передачи данных при помощи построения и верификации архитектурных диаграмм;

2. Разработан и обоснован набор типовых модулей для построения архитектурных диаграмм программных моделей протоколов передачи данных для встроенных систем;

3. Разработан метод организации межмодульных взаимодействий в архитектурной диаграмме;

4. Разработан метод перехода от архитектурной диаграммы программной модели к формальной модели в терминах раскрашенной сети Петри;

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

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

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

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

Основные публикации по теме диссертации

1. Оленев В.Л. Моделирование на языке SystemC в процессе разработки протоколов передачи данных// Известия высших учебных заведений. Поволжский регион. Технические науки. Пенза, 2009. №4 (12). C. 61-69.

2. Оленев В.Л. Исследование и разработка системы для создания моделей протоколов передачи данных и их верификации// Ползуновский вестник. Барнаул, 2010. №2. C. 36-42.

3. Valentin Olenev, Alexey Rabin, Alexander Stepanov, Irina Lavrovskaya, Sergey Balandin, Michel Gillet. Co-Modeling of Embedded Networks Using SystemC and SDL // International Journal of Embedded and Real-Time Communication Systems (JERTCS), 2011. #2(1). C. 24-49.

4. Оленев В.Л., Онищенко Л.В., Еганян А.В. Методы межмодульного взаимодействия при моделирования протоколов встроенных систем// Научная сессия ГУАП: Сб. докл./ СПбГУАП. СПб., 2008. С. 119-122.

5. Valentin Olenev, Sergey Balandin, Michel Gillet, Elena Suvorova, Ludmila Onishenko, Artur Eganyan. Efficient Inter-module Interaction in SystemC Models of Large Embedded Systems// Cadence Designer Network, CDNLive, 2008. 5 стр.

6. Valentin Olenev. Different approaches for the stacks of protocols SystemC modelling// 4th Seminar of Finnish-Russian University Cooperation in Telecommunications (FRUCT) Program, 2008. 4 стр.

7. Оленев В.Л. Анализ подходов к моделированию стеков протоколов передачи данных// Научная сессия ГУАП. Часть 1: Сб. докл./ СПбГУАП. СПб., 2009. C. 112-114.

8. Valentin Olenev, Alexander Stepanov. Comparative Analysis of SDL and SystemC languages for Real-Time Systems Modelling// 5th Seminar of Finnish-Russian University Cooperation in Telecommunications (FRUCT) Program, 2009. 5 стр.

9. Оленев В.Л., Степанов А.С., Лавровская И.Я., Рабин А.В. SystemC and SDL Co-Modeling Methods// 6th Seminar of Finnish-Russian University Cooperation in Telecommunications (FRUCT) Program / Proceedings printed by Saint-Petersburg State University of Aerospace Instrumentation (SUAI). 2009. С. 136 - 140.

10. Оленев В.Л., Шейнин Ю.Е., Суворова Е.А., Баландин С., Gillet M. SystemC Modelling of the Embedded Networks// 6th Seminar of Finnish-Russian University Cooperation in Telecommunications (FRUCT) Program/ Proceedings printed by Saint-Petersburg State University of Aerospace Instrumentation (SUAI). 2009. С. 85 - 95.

11. Оленев В.Л., Коробков И., Коблякова Л., Шутенко Ф. Remote Memory Access in Embedded Networked Systems// 6th Seminar of Finnish-Russian University Cooperation in Telecommunications (FRUCT) Program/ Proceedings printed by Saint-Petersburg State University of Aerospace Instrumentation (SUAI). 2009. С. 77 - 84.

12. Оленев В.Л., Коробков И., Мартынов Н., Шадурский А. Modelling of the SpaceWire communication protocol// 7th Conference of Open Innovations Framework Program FRUCT/ Proceedings printed by Saint-Petersburg State University of Aerospace Instrumentation (SUAI). 2010. С. 96 - 104.

13. Оленев В.Л., Степанов А.С., Лавровская И.Я., Рабин А.В. SystemC and SDL Co-modelling implementation// 7th Conference of Open Innovations Framework Program FRUCT/ Proceedings printed by Saint-Petersburg State University of Aerospace Instrumentation (SUAI). 2010. С. 130 - 137.

14. Оленев В.Л., Пешаков И. Исследование и разработка системы моделирования протоколов передачи данных на языке SystemC// Научная сессия ГУАП. Часть 1: Сб. докл./ СПбГУАП. СПб., 2010. C. 112-119.

15. Оленев В.Л., Степанов А.С., Лавровская И.Я., Рабин А.В. Разработка и исследование методов совместного моделирования встроенных систем на языках SDL и SystemC// Научная сессия ГУАП. Часть 1: Сб. докл./ СПбГУАП. СПб., 2010. C. 122-127.

16. Оленев В.Л., Степанов А.С., Лавровская И.Я. SDL and SystemC co-modelling: the protocol SDL models Tester// 8th Conference of Open Innovations Framework Program FRUCT/ Proceedings printed by Saint-Petersburg State University of Aerospace Instrumentation (SUAI). 2010. С. 198 - 207.

17. Оленев В.Л., Коробков И.Л., Шадурский А.В., Мартынов Н.А. RMAP and STP protocols modelling over the SpaceWire SystemC model// 8th Conference of Open Innovations Framework Program FRUCT/ Proceedings printed by Saint-Petersburg State University of Aerospace Instrumentation (SUAI). 2010. С. 111 - 121.

Размещено на Allbest.ru