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

IX рукописи

ОЛЕНЕВ Валентин Леонидович

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

Специальность 05.13.11 - Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей

АВТОРЕФЕРАТ диссертации на соискание ученой степени кандидата технических наук

-1 ДЕК 2011

Санкт-Петербург - 2011

005004177

Работа выполнена на кафедре «Информационных систем» в Федеральном государственном бюджетном образовательном учреждении высшего профессионального образования «Санкт-Петербургский государственный университет аэрокосмического приборостроения» (ГУАП).

Научный руководитель:

Официальные оппоненты:

доктор технических наук Шейнин Юрий Евгеньевич доктор технических наук, профессор Водяхо Александр Иванович кандидат технических наук, доцент Щекин Сергей Валерьевич

Ведущая организация

Санкт-Петербургский институт информатики и автоматизации РАН

Защита состоится « 20 » аетМЛ. 2011 г. в /£¿#7 часов на заседании диссертационного совета Д 212.233.02 при Федеральном государственном бюджетном образовательном учреждении высшего профессионального образования «Санкт-Петербургский государственный университет аэрокосмического приборостроения» по адресу:

190000, Санкт-Петербург, ул. Б. Морская, 67, ГУАП. С диссертацией можно ознакомиться в библиотеке ГУАП. Автореферат разослан « /О » /¿Ы&Ы 2011 г.

Ученый секретарь диссертационного совета доктор технических наук, профессор

//С

Осипов Л.А

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

Актуальность темы. Встроенные системы стали использоваться повсеместно: в автомобилестроении, мобильной индустрии и других вещах, без которых жизнь современного человека уже сложно представить. Многие встроенные системы состоят не только из одного процессора, а могут содержать целые сети-на-кристалле. Составляющие элементы таких сетей должны взаимодействовать между собой, руководствуясь жесткими правилами для достижения требований энергопотребления, физических размеров и стоимости, выдвигаемых к встроенной системе. Такие правила называют протоколами для встроенных систем. Разработка протоколов передачи данных для таких систем является очень трудоемкой задачей, состоящей из нескольких этапов: она начинается с концептуального проектирования системы и заканчивается сбором устройства, работающего по заданному протоколу. Однако в процессе разработки спецификации протокола зачастую возникают моменты, когда необходимо выбирать тот или иной путь решения проблемы, анализировать различные подходы к реализации и проверять спецификацию на ошибки разработчиков. Именно поэтому программное моделирование становится все более необходимым элементом проектирования протоколов передачи данных для встроенных систем. Оно позволяет обнаружить ошибки на ранних этапах разработки спецификаций, значительно уменьшить само время разработки, а так же в дальнейшем использовать полученные программные модели для тестирования реальных плат. Программное моделирование протоколов ведется во многих крупных компаниях, таких как Nokia, STErricsson, Qualcomm, в работах, курируемых Европейским Космическим Агентством (ESA), в разработках авиационных компаний и т.д. Однако каждая компания ведет разработку своими путями. Методы проверки на программных моделях широко используются и описаны в работах таких авторов как Э. М. Кларк, О. Грамберг и Д. Пелед, Ю.Г. Карпов, в результатах исследований компании Cadence. Однако на данный момент не существует четко сформулированных и описанных формальных методов организации программного обеспечения для моделирования стеков протоколов встроенных систем, что осложняет их разработку и реализацию. Поэтому, разработка методики построения программного обеспечения для написания программных моделей протоколов передачи данных для встроенных систем и верификации этих программных моделей является актуальной проблемой.

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

и организации взаимодействий между модулями, пользуясь теорией сетей Петри и в частности, теорией раскрашенных сетей Петри, развитой и доработанной К. Енсеном. Результатом такой работы может быть сгенерированный из полученной архитектурной диаграммы скелет программной модели на языке 5уз1етС.

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

• разработка метода проектирования и анализа программных моделей протоколов передачи данных;

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

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

• разработка метода перехода от архитектурной диаграммы программной модели к интерпретирующей ее раскрашенной сети Петри;

• разработка алгоритма разметки раскрашенной сети Петри для осуществления верификации архитектурных диаграмм программных моделей;

• исследование и разработка метода перехода от раскрашенной сети Петри к эквивалентной ей классической сети Петри в целях применения методов анализа классических сетей Петри к раскрашенным сетям;

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

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

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

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

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

4. алгоритм разметки раскрашенной сети Петри для осуществления анализа движения фишек при помощи деревьев достижимости;

5. метод верификации архитектурной диаграммы программной модели протокола

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

Внедрение и реализация результатов работы. Основные исследования и результаты диссертационной работы использованы в Институте высокопроизводительных компьютерных и сетевых технологий Государственного Университета Аэрокосмического Приборостроения для разработки программных моделей протоколов передачи данных для таких компаний как Nokia и ОАО «НИИ Авиационного оборудования». Результаты внедрения подтверждены соответствующими актами.

Апробация результатов работы. Основные положения и результаты диссертации докладывались и обсуждались на конференции Cadence CDNLife (2008 г.), Научных сессиях ГУАП (2008, 2009, 2010 гг.), а также международных конференциях FRUCT в 2009 и 2010 гг.

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

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

2. Метод формального описания архитектурных диаграмм программных моделей раскрашенными сетями Петри;

3. Алгоритм разметки раскрашенных сетей Петри для осуществления анализа движения фишек по сети Петри методом построения деревьев достижимости;

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

Обье.м и структура работы. Диссертационная работа состоит из введения, списка используемых сокращений, четырех глав, заключения, списка использованных источников и трёх приложений. Диссертация содержит 144 страницы машинописного текста, 56 рисунков и 16 таблиц, а также приложения объемом 38 страниц, включая 10 рисунков и 3 таблицы. В списке использованной литературы 119 наименований.

КРАТКОЕ СОДЕРЖАНИЕ РАБОТЫ

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

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

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

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

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

В первой главе показано место программного моделирования в процессе разработки стеков протоколов передачи данных на различных этапах проектирования, показана сложность и трудоемкость этих процессов. Сформулированы требования к языку проектирования и написания программных моделей протоколов, основываясь на которых был выбран язык проектирования Зу51етС.

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

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

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

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

На основе такой архитектурной диаграммы в дальнейшем генерируется «скелет» программной модели. Скелетом программной модели называется код, полученный (возможно, автоматически) на основе архитектурной диаграммы; он включает в себя описания модулей, портов, интерфейсов и методов, отвечающих за передачу данных между модулями. Вышеописанный метод приведен в следующей главе диссертации. На основе скелета программной модели может писаться код, описывающий алгоритмы работы каждого из модулей.

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

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

1. Моделируемый протокол должен быть описан по слоям или составлять целиком один уровень;

2. Между уровнями могут быть описаны сервисные точки доступа;

3. Спецификация протокола должна описывать структуру передаваемых данных относительно каждого уровня;

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

Под данную классификацию подходит большинство стандартов для стеков протоколов передачи данных встроенных систем.

Разработан метод перехода от спецификации стандарта протокола передачи данных к архитектурной диаграмме программной модели этого протокола. Метод позволяет составить архитектурную диаграмму протокола по слоям (уровням) при помощи предложенного в работе набора типовых модулей: модуль инициализации (IM), стандартный модуль {СМ), симплексный канал (SC), дуплексный канал (DQ, сервисная точка доступа (SAP). Взаимодействие модулей осуществляется посредством портов и интерфейсов.

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

М={1М, CM, SC, DC, SAP}

Каждый модуль имеет порты () и интерфейсы ), которые представляют из себя структуры, описанные в языке SystemC (sc_port и scinterface). Каждый интерфейс описывает ряд методов, определенных в модуле, которые могут быть вызваны на исполнение через порт удаленного модуля, связанный с данным интерфейсом.

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

Рис. 1 Пример использования модуля инициализации Модуль не учавствует в процессе передачи данных по модели, не имеет входов и выходов (портов и интерфейсов).

Стандартный модуль СМ может иметь от нуля до нескольких входов и выходов (Ы портов и М интерфейсов). Особенности работы каждого СМ (функциональность) задаются разработчиком в дальнейшем написании соответствующей программы на языке 5уз1етС. Модуль показан на рис. 2.

Рис. 2 Стандартный модуль Предикат срабатывания модуля обозначим RCm-

RCM(data,, data,,..., dataj = {data, *0)v(data2 * 0) v... v (datan *0), где datai - данные, поступившие на г'-й интерфейс модуля. То есть срабатывание модуля происходит при поступлении данных на вход одного или нескольких интерфейсов.

Модуль симплексного канала SC. рис. 3, принимает и передает данные одного или нескольких типов в одном направлении. Объекты передаются через канал путем записи в очередь FIFO и чтения из нее. Используется для моделирования передачи данных между

устройствами или какими-то отдельными модулями, в которых требуется накопление данных.

Рис. 3 Симплексный канал

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

Rsc(data) = (data

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

Модуль дуплексного канала DC, рис. 4, принимает и передает данные одного или нескольких типов в обоих направлениях. Объекты передаются через канал путем записи в очередь FIFO и чтения из неё. Используется для моделирования передачи данных между устройствами или какими-то отдельными модулями, в которых требуется накопление и двунаправленная передача данных.

Рис. 4 Дуплексный канал Предикатом срабатывания модуля обозначим Roc. \

RDC(data,, dataj = (data{ *0)v(data2 ф 0), где data, - данные, поступившие на ;'-й интерфейс модуля {¡={0,1}). То есть срабатывание модуля происходит при поступлении данных на один или оба интерфейса. Каждый из интерфейсов связан с разными портами. Затем данные записываются в очередь FIFO, связанную с интерфейсом, на который эти данные пришли.

Модуль типа «Сервисная точка доступа» (SAP) является более сложной, чем канал структурой, которая способна передавать различные примитивы. Примитивами называются передаваемые аргументы в виде структур данных, в данном случае это методы с набором параметров. И очередь FIFO, расположенная в SAP, должна быть адаптирована к приему разного вида примитивов с разным количеством аргументов.

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

вынести функции создания примитивов и чтения данных из примитивов из самого модуля SAP. Графическое изображение модуля SAP показано на рис. 5. Предикатом срабатывания модуля обозначим Rsap-

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

соответствующий порт.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

выполняемых каждым уровнем, формирует количество СМ модулей, используемых для моделирования уровня. Для выполнения каждой отдельной задачи предусматривается отдельный модуль программной модели, выбранный из определенного в диссертации набора модулей. Если какая-либо задача уровня включает накопление данных в рамках одного модуля, то вместо СМ- используется DC или SC модуль. Если между уровнями в спецификации описаны сервисные точки доступа - для них используется модуль SAP.

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

Y={>'o, у,. у2.....у,}; (1)

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

d2, di.....d„} (2)

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

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

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

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

Таблица 1

Номер Данные Модули

0 Уо, У/

п а„ Уъ - Ут

, ----- -------vo^tnnfl, капле ir,i^ ц у согласно

спецификации, должны попасть в какие модули У]. Каждому данному из множества D присваивается свой номер и ставится в соответствующий столбец. Данные в столбец «Модули» ставятся в зависимости от того, входными для каких модулей эти данные являются по спецификации. Модулей для одного данного может быть указано несколько, если данные

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

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

Х0 = {у„, ... yj; (для а„) (3)

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

Ул - fro. z,.....zj (4)

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

1фа)={ .....zj; (5)

Out(yd)~{zm+l, zm+2,..„ z„+J; Данные, которые передаются или принимаются при помощи этого метода С++ класса, заносятся в третий столбец таблицы. Это делается на основе вышеопределенного множества D. Например,

А(у„ zj = {а,. а}, .... aj; (6)

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

BfyJ -= {if,. if2.....ifil;

В(Ухч) = {port,, port2.....port} ; (7)

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

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

ln(yx)r\Out(y,) = zll ^

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

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

С = {Яо, Я/.....К,,} (9)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Признак Метод Данные Порт/Интерфейс Метка

Уо

zm а0 ifi go

ап

- zm+l Я/ ifj+i Si

«ш*

Ух

- Я; port1 gi

ап+к

...

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

D={type, datahtype2 data2,type} data}, ...,typem data J (10)

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

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

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

Сеть Петри - это набор N = (Р. Т, F, W, М(1), где Р - конечное множество позиций; Г - конечное множество переходов; F- конечное множество дуг.

A W: F—> ЩО} и М0: Р —»N— две функций, называемые соответственно кратностью дуг и начальной разметкой.

Раскрашенная сеть Петри - это кортеж N ~(£,Р, Т, F,K,C, G,E,I), где Е- конечное множество цветов;

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

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

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

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

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

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

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

2) каждому вызываемому С++ методу и передаваемым с его помощью данным zx(ay) по связи порт-интерфейс сопоставляется свой переход ty (в том случае, когда метки g в таблице взаимосвязей в модулях совпадают (G(yx,zJ=G(y„zr)));

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

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

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

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

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

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

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

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

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

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

Номер Тип данных Название Цвет Пример

0 типа «0 Черный прерывистый ® ___

1 тип ¡ Серый 9

2 тип2 а2 Черный •

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

В соответствии с теорией сетей Петри примем следующие обозначения: Рт - множество позиций дня разметки (до начала выполнения алгоритма Рт=Р); Pnext ~ множество позиций, в которые осуществляется переход из текущей позиции; Ст - множество уже поставленных цветов (до начала выполнения алгоритма Ст= 0); C(ta,J - множество цветов, определенных для переходов из текущей позиции; С- полученное множество цветов фишек, которые ставятся в текущей позиции;

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

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

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

С = С(и '\ С„ (11)

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

Ст=СтПС (12)

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

(13)

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

Р^г-Рп, П Рт.,. (14)

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

a. Если Р„ех1=0, то останавливается дальнейшая разметка этой ветви;

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

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

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

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

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

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

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

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

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

ти Петри ./V;

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

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

В тексте диссертации приведено доказательство следующих теорем. Теорема 3.1: При построении классической сети Петри ¿V из раскрашенной сети Петри Л', полученной из архитектурной диаграммы программной модели протокола передачи данных по предложенному алгоритму, раскрашенная сеть Петри Й преобразуется в несколько классических сетей Петри по признаку цвета из I.

Теорема 3.2: Классические сети Петри Л'0...Л,1_;, полученные из раскрашенной сети Петри N по предложенному алгоритму, не имеют общих дуг позиций Р и переходов Т.

б)

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

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

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

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

р1/

8 ® »

/ ^ 4 % \

'4

ч 7 „ * Ру

1 » с

ч/ \

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

юсооо

I I

I

010000

оюооо

001000

000100

оооою

010000

оооюо

000001

000010

001100

000110

000011

000002

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

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

После построения дерева достижимости для каждой из классических сетей Петри, полученных по вышеописанному алгоритму, анализируются вершины этих деревьев достижимости. Каждой из вершин дерева достижимости соответствует маркировка сети Петри от Мо (начальной маркировки) до Мг Например, маркировка 00201 показывает, что две фишки находятся в позиции р2 и одна фишка в позиции р4. Для каждой из вершин дерева достижимости составляется множество позиций О, в которых находятся фишки. Таким образом, для и вершин дерева достижимости будет ..£„./ множеств. Из этих множеств для каждой ветви дерева достижимости составляется множество достижимости 2 по следующей формуле:

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

О"0 = О0иа,={ро}^{р,}4ро. Р,} (16)

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

Исходя из вышеописанных принципов построения сетей Петри на основе архитектурных диаграмм, каждая позиция р, сети Петри соответствует модулю у]- архитектурной диаграммы. Также, фишки, ходящие по каждой классической сети Петри Л^, соответствуют определенному типу данных ап. Поэтому, на основе полученных множеств О может осуществляться верификация архитектурной диаграммы программной модели протокола передачи данных.

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

0\-{у„,у,} (17)

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

Для каждого цвета с,=а, ставятся в соответствие множество X, и множества Далее для каждого маршрута/определяется множество модулей, по которым прошли и в которые не попали данные типа я, по формуле:

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

Если же Я/0, то в результате в множестве Я оказывается набор модулей, в которые данные я, не попали, пройдя маршрутом/. Если для данных л,- нет такого маршрута, идя по которому данные попали во все требуемые модули, то в построении архитектурной диаграммы допущена ошибка.

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

Таким образом, в результате верификации будет получено некоторое количество множеств 2о-.. 2h. Каждое из этих множеств показывает те модули уо—ут, в которые не попали данные а,. Таким образом, анализ показывает, какие требования спецификации, отраженные в таблице требований, не выполнены. На основе этого делаются выводы о необходимых изменениях в архитектурной диаграмме.

Например, возьмем сетевой уровень протокола, который должен проверять сетевой адрес пакета. Для этого по спецификации он должен получить примитив, говорящий о пришедшем пакете, из канального уровня через SAP, затем проверить адрес пакета. Если адрес верный, то в пакете отбрасывается заголовок сетевого уровня и передается в SAP транспортного уровня. Если адрес неверный, то пакет отбрасывается. Таким образом, нужно 4 модуля: SAP сетевого и транспортного уровня (у0 и _vj), модуль проверки адреса О'/), модуль отбрасывания сетевого заголовка пакета (у2). Отсюда видно, что пакет проходит по пути Уо ► у,—* у2. Допустим, что при составлении архитектурной диаграммы была допущена ошибка, и не был предусмотрен С++ метод, передающий данные типа «пакет» из уj в у,. Следовательно, анализ архитектурной диаграммы покажет, что данные типа «пакет» прошли по маршруту уд-* у, и не попали в модуль у2. Из этого разработчик увидит несоответствие между архитектурной диаграммой и спецификацией протокола.

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

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

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

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

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

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

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

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

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

• программная модель Символьного уровня протокола Space Wire;

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

i-1

........i

Рисунок 10. Внешний вид программы ESPMS. Также в четвертой главе приведено описание инструментально-программного комплекса ESPMS (Embedded Systems Protocols Modelling Software), разработанного с использованием разработанных методов и алгоритмов, предложенных в диссертационной работе

(рис.10). Система ЕБРМБ описана на языке С++ с помощью (¿и Она выполняет следующие функции:

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

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

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

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

ОСНОВНЫЕ РЕЗУЛЬТАТЫ РАБОТЫ

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

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

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

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

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

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

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

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

ОСНОВНЫЕ ПУБЛИКАЦИИ ПО ТЕМЕ ДИССЕРТАЦИИ

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

2. Оленев В.Л. Исследование и разработка системы для создания моделей протоколов передачи данных и их верификации// Ползуновский вестник. Барнаул, 2010. №2. С. 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. Оленев B.JI., Онищенко Л.В., Егапян A.B. Методы межмодульного взаимодействия при моделирования протоколов встроенных систем// Научная сессия ГУАП: Сб. докл./ СПбГУАП. СПб., 2008. С. 119-122.

5. Valentin Olenev, Sergey Balandin, Michel Gillet, Elena Suvorova, Ludmila Onishenko, Ar-tur 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. Оленев B.JI. Анализ подходов к моделированию стеков протоколов передачи данных// Научная сессия ГУАП. Часть I: Сб. докл./ СПбГУАП. СПб., 2009. С. 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. Оленев B.JI., Степанов A.C., Лавровская И.Я., Рабин A.B. 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. C. 136 - 140.

10. Оленев В.JI., Шейнин Ю.Е., Суворова Е.А., Баландин С., Gillet М. 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. C. 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. C. 77 - 84.

12. Оленев В.Л., Коробков И., Мартынов К, Щадурский A. 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. C. 96 - 104.

13. Оленев В.Л., Степанов A.C., Лавровская И.Я., Рабин А.В. 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. C. 130 - 137.

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

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

Формат 60x84 1/16. Бумага офсетная. Печать офсетная. Тираж ] 00 экз. Заказ № 527.

Редакционио-издательский центр ГУАП 190000, г. Санкт-Петербург, ул. Б. Морская, 67

61 12-5/1503

Министерство образования и науки Российской Федерации

Федеральное государственное бюджетное образовательное учреждение высшего

профессионального образования

САНКТ-ПЕТЕРБУРГСКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ АЭРОКОСМИЧЕСКОГО ПРИБОРОСТРОЕНИЯ

На правах рукописи

ОЛЕНЕВ Валентин Леонидович

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

05.13.11 - Математическое обеспечение вычислительных машин, комплексов и компьютерных сетей

Диссертация на соискание ученой степени кандидата технических наук Научный руководитель - доктор технических наук, Ю.Е. Шейнин

Санкт-Петербург - 2011

ОГЛАВЛЕНИЕ

СПИСОК ИСПОЛЬЗУЕМЫХ СОКРАЩЕНИЙ.....................................................................................6

ВВЕДЕНИЕ.................................................................................................................................................8

ГЛАВА 1. ПРОГРАММНОЕ МОДЕЛИРОВАНИЕ ПРОТОКОЛОВ ПЕРЕДАЧИ ДАННЫХ ДЛЯ

1Л

ВСТРОЕННЫХ СИСТЕМ.......................................................................................................................

1.1 Сетевые протоколы для межкристальных коммуникаций во встроенных системах...............14

1Я

1.2 Разработка стеков протоколов передачи данных........................................................................10

1.3 Роль программного моделирования в процессе разработки стеков протоколов встроенных систем ....................................................................................................................................................

1.3.1 Программное моделирование в процессе написания спецификации протокола для встроенных систем...........................................................................................................................^

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

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

1.3.4 Выводы.....................................................................................................................................30

1.4 Требования к языку проектирования и написания программных моделей..............................32

1.5 Язык 8уз1етС и его преимущества...............................................................................................33

1.5.1 Описание языка ...............................................................................................................

1.5.2 Обоснование выбора 8уз1етС для написания программных моделей протоколов

3 6

встроенных систем...........................................................................................................................

39

1.6 Постановка задачи..........................................................................................................................

ВЫВОДЫ ПО ГЛАВЕ 1..........................................................................................................................44

ГЛАВА 2. ПЕРЕХОД ОТ СПЕЦИФИКАЦИИ К ПРОГРАММНОЙ МОДЕЛИ ПРОТОКОЛА ПЕРЕДАЧИ ДАННЫХ............................................................................................................................45

2.1 Архитектура программных моделей протоколов передач данных встроенных систем..........45

48

2.2 Компонентное проектирование.....................................................................................................но

2.2.1 Принцип модульности............................................................................................................50

2.2.2 Выбор типа модулей для построения архитектурной диаграммы......................................52

2.2.3 Определение набора модулей для разработки архитектурных диаграмм программных моделей протоколов встроенных систем.......................................................................................56

2.3 Набор базовых модулей для построения архитектурной диаграммы протокола.....................60

2.3.1 Модуль инициализации ......................................................................................................60

2.3.2 Стандартный модуль (N портов и М интерфейсов) (СМ)...................................................61

(V)

2.3.3 Симплексный канал ............................................................................................................

/о

2.3.4 Дуплексный канал (DC)...........................................................................................................0

fsA

2.3.5 Сервисная точка доступа (SAP).............................................................................................

2.3.6 Необходимость и достаточность набора модулей................................................................65

2.4 Ошибки построения архитектурной диаграммы.........................................................................67

2 5 Метод построения архитектурных диаграмм программных моделей протоколов на основе

69

набора модулей.....................................................................................................................................

2.5.1 Определение типов данных и модулей для построения архитектурной диаграммы на основе спецификации протокола....................................................................................................69

2.5.2 Составление Таблицы требований спецификации...............................................................71

2.5.3 Составление Таблицы взаимосвязей.....................................................................................72

2.6 Генерация SystemC модели из архитектурной диаграммы........................................................80

ВЫВОДЫ ПО ГЛАВЕ 2..........................................................................................................................83

ГЛАВА 3. ВЕРИФИКАЦИЯ АРХИТЕКТУРЫ ПРОГРАММНОЙ МОДЕЛИ ПРОТОКОЛА ПЕРЕДАЧИ ДАННЫХ С ИСПОЛЬЗОВАНИЕМ РАСКРАШЕННЫХ СЕТЕЙ ПЕТРИ..................85

3.1 Верификация при помощи сетей Петри.......................................................................................85

3.2 Применение теории сетей Петри для моделирования................................................................85

3.2.1 Теория сетей Петри.................................................................................................................85

3.2.2 Формальное определение сетей Петри..................................................................................88

3.2.3 Раскрашенные сети Петри......................................................................................................89

3.2.4 Формальное определение раскрашенных сетей Петри........................................................89

3.3 Составление раскрашенной сети Петри по архитектурной диаграмме уровня программной модели стека протоколов.....................................................................................................................91

3.3.1 Метод перехода от архитектурной диаграммы к раскрашенной сети Петри....................92

3.3.2 Пример перехода от архитектурной диаграммы к раскрашенной сети Петри..................93

3.3.3 Свойства раскрашенной сети Петри, полученной из архитектурной диаграммы............94

3.3.4 Разметка раскрашенной сети Петри......................................................................................95

3.3.5 Алгоритм разметки раскрашенной сети Петри....................................................................уо

3.4 Построение набора классических сетей Петри эквивалентного раскрашенной сети..............97

3 4 1 Построение классической сети Петри эквивалентной раскрашенной сети Петри по

............................98

поведению..........................................................................................................

3.4.2 Классическая сеть Петри эквивалентная раскрашенной сети...........................................100

3.4.3 Алгоритм построения классической сети Петри эквивалентной раскрашенной............102

3.4.4 Доказательство преобразования раскрашенной сети Петри по признаку цвета в эквивалентный ей набор обычных сетей Петри..........................................................................103

3.5 Методы анализа сетей Петри......................................................................................................111

3.6 Верификация архитектурной диаграммы на основе результатов анализа Сетей Петри

11Я

деревьями достижимости..................................................................................................................110

3.7 Результат верификации................................................................................................................120

3.8 Проверка программной модели на соответствие спецификации протокола..........................121

ВЫВОДЫ ПО ГЛАВЕ 3........................................................................................................................124

ГЛАВА 4. ПРИМЕНЕНИЕ РАЗРАБОТАННЫХ МЕТОДОВ И АЛГОРИТМОВ ПРОЕКТИРОВАНИЯ И ВЕРИФИКАЦИИ АРХИТЕКТУРНЫХ ДИАГРАММ ПРОГРАММНЫХ МОДЕЛЕЙ ПРОТОКОЛОВ ВСТРОЕННЫХ СИСТЕМ....................................................................126

4.1 Программная модель стека протоколов UniPro.........................................................................126

4.1.1 Уровень адаптации к физическому уровню (PA Layer).....................................................127

4.1.2 Программная модель уровня адаптации.............................................................................129

4.1.3 Физический уровень (PHY Layer)........................................................................................141

4.1.4 Программная модель физического уровня.........................................................................142

4.2 Программная модель стека протоколов Space Wire...................................................................157

4.2.1 Символьный уровень SpaceWire..........................................................................................158

4.2.2 Программная модель символьного уровня SpaceWire.......................................................159

4.3 Система построения программных моделей сетевых протоколов для встроенных систем (Embedded Systems Protocols Modelling Software)...........................................................................169

4.4 Обоснование эффективности использования предложенной методики.................................174

ВЫВОДЫ ПО ГЛАВЕ 4........................................................................................................................181

ЗАКЛЮЧЕНИЕ......................................................................................................................................183

СПИСОК ИСПОЛЬЗОВАННОЙ ЛИТЕРАТУРЫ...............................................................................190

ПРИЛОЖЕНИЕ А. РЕАЛИЗАЦИЯ ОСНОВНЫХ АЛГОРИТМОВ МЕТОДИКИ ПОСТРОЕНИЯ МОДЕЛЕЙ И ИХ ВЕРИФИКАЦИИ НА ЯЗЫКЕ С++.......................................................................201

201

Файл petryanalyzer.cpp.................................................................................................................

207

Файл petryanalyzer.h.....................................................................................................................

ПРИЛОЖЕНИЕ Б. ПРИМЕР ПЕРЕХОДА ОТ СПЕЦИФИКАЦИИ ПРОТОКОЛА К АРХИТЕКТУРНОЙ ДИАГРАММЕ И ВЕРИФИКАЦИИ ЭТОЙ АРХИТЕКТУРНОЙ

709

ДИАГРАММЫ.......................................................................................................................................zuy

Б.1. Пример перехода от спецификации протокола к архитектурной диаграмме.......................209

- 911 В. 1.2 Определение межмодульных взаимодействии..................................................................1

Б.2 Пример составления раскрашенной сети Петри по архитектурной диаграмме и ее анализ. 216

Б.2.1 Составление раскрашенной сети Петри..............................................................................216

Б.2.2 Анализ раскрашенной сети Петри на достижимость.........................................................222

ПРИЛОЖЕНИЕ В. СОДЕРЖИМОЕ ТЕКСТОВОГО ФАЙЛА С РЕЗУЛЬТАТАМИ ВЕРИФИКАЦИИ АРХИТЕКТУРНОЙ ДИАГРАММЫ В ПРОГРАММЕ ESPMS.........................228

СПИСОК ИСПОЛЬЗУЕМЫХ СОКРАЩЕНИЙ

ESA - European Space Agency

FRUCT - Finnish-Russian University Cooperation in Telecommunications

ВАК - Высшая аттестационная комиссия

OSI - Open Systems Interconnection

API - Application Programming Interface

SDL - Specification Description Language

VHDL - VHSIC hardware description language

VHSIC - very-high-speed integrated circuit

GDSII - Graphic Data System II

HDL -Hardware Description Language

UniPro - Unified Protocol

RTL - Register transfer level

FIFO - First in first out

SCV library - SystemC Verification library

OSCI - open SystemC Initiative

SAP - Service access point

RMAP - Remote memory-access protocol

CN - Coloured Petri Net

ЭВМ - Электронная Вычислительная Машина ЕОР - End of packet PHY Layer - Physical Layer PA - Physical Adapter

DL - Data Link

PDU - Protocol Data Unit

DME - Device Management Entity

LM - Layer Management

NASA - National Aeronautics and Space Administration

JAXA - Japan Aerospace Exploration Agency

ФКА - Федеральное Космическое Агентство

ЕЕР - End of error packet

FCT - Flow control token

SUT - System under test

ВВЕДЕНИЕ

Встроенные системы стали использоваться повсеместно: в автомобилестроении, мобильной индустрии и других вещах, без которых жизнь современного человека уже сложно представить. Многие встроенные системы состоят не только из одного процессора, а могут содержать целые сети-на-кристалле. Составляющие элементы таких сетей должны взаимодействовать между собой, руководствуясь жесткими правилами для достижения требований энергопотребления, физических размеров и стоимости, выдвигаемых к встроенной системе. Такие правила называют протоколами для встроенных систем. Разработка протоколов передачи данных для таких систем является очень трудоемкой задачей, состоящей из нескольких этапов: она начинается с концептуального проектирования системы и заканчивается сбором устройства, работающего по заданному протоколу. Однако в процессе разработки спецификации протокола зачастую возникают моменты, когда необходимо выбирать тот или иной путь решения проблемы, анализировать различные подходы к реализации и проверять спецификацию на ошибки разработчиков. Именно поэтому программное моделирование становится все более необходимым элементом проектирования протоколов передачи данных для встроенных систем. Оно позволяет обнаружить ошибки на ранних этапах разработки спецификаций, значительно уменьшить само время разработки, а так же в дальнейшем использовать полученные программные модели для тестирования реальных плат. Программная модель протокола является сложным многокомпонетным параллельным программным комплексом, поэтому задачи разработки и написания такой модели также являются сложными и трудоемкими. Программное моделирование протоколов ведется во многих крупных компаниях, таких как Nokia, STErricsson, Qualcomm, в работах, курируемых Европейским Космическим Агентством (ESA), в разработках авиационных компаний и т.д. Однако каждая компания ведет разработку своими путями. Методы проверки на программных моделях широко используются и описаны в работах таких авторов как Э. М. Кларк, О. Грамберг и Д. Пелед, Ю.Г. Карпов, в результатах исследований компании Cadence. Однако на данный

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

актуальной проблемой.

В данной диссертации предлагается использовать широко

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

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

Для достижения поставленной цели в работе решались следующие задачи:

1. разработка метода проектирования и анализа программных моделей

протоколов передачи данных;

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

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

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

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

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

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

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

Научной новизной обладают следующие результаты работы:

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

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

встроенных систем;

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

4. алгоритм разметки раскрашенной сети Петри для осуществления анализа движения фишек при помощи деревьев достижимости;

5. метод верификации архитектурной диаграммы программной модели протокола на основе результатов анализа сетей Петри.

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

Основные исследования и результаты диссертационной работы внедрены в учебный процесс Государственного университета аэрокосмического приборостроения, внедрены при разработке программных моделей протоколов передачи данных для таких компании Nokia и ОАО «НИИ Авиационного оборудования», использованы в р�