Введение к работе
Актуальность темы. Встроенные системы стали использоваться повсеместно: в автомобилестроении, мобильной индустрии и других вещах, без которых жизнь современного человека уже сложно представить. Многие встроенные системы состоят не только из одного процессора, а могут содержать целые сети-на-кристалле. Составляющие элементы таких сетей должны взаимодействовать между собой, руководствуясь жесткими правилами для достижения требований энергопотребления, физических размеров и стоимости, выдвигаемых к встроенной системе. Такие правила называют протоколами для встроенных систем. Разработка протоколов передачи данных для таких систем является очень трудоемкой задачей, состоящей из нескольких этапов: она начинается с концептуального проектирования системы и заканчивается сбором устройства, работающего по заданному протоколу. Однако в процессе разработки спецификации протокола зачастую возникают моменты, когда необходимо выбирать тот или иной путь решения проблемы, анализировать различные подходы к реализации и проверять спецификацию на ошибки разработчиков. Именно поэтому программное моделирование становится все более необходимым элементом проектирования протоколов передачи данных для встроенных систем. Оно позволяет обнаружить ошибки на ранних этапах разработки спецификаций, значительно уменьшить само время разработки, а так же в дальнейшем использовать полученные программные модели для тестирования реальных плат. Программное моделирование протоколов ведется во многих крупных компаниях, таких как Nokia, STErricsson, Qualcomm, в работах, курируемых Европейским Космическим Агентством (ESA), в разработках авиационных компаний и т.д. Однако каждая компания ведет разработку своими путями. Методы проверки на программных моделях широко используются и описаны в работах таких авторов как Э. М. Кларк, О. Грамберг и Д. Пелед, Ю.Г. Карпов, в результатах исследований компании Cadence. Однако на данный момент не существует четко сформулированных и описанных формальных методов организации программного обеспечения для моделирования стеков протоколов встроенных систем, что осложняет их разработку и реализацию. Поэтому, разработка методики построения программного обеспечения для написания программных моделей протоколов передачи данных для встроенных систем и верификации этих программных моделей является актуальной проблемой.
В данной диссертации предлагается использовать широко используемый в последнее время подход компонентного проектирования, описанный в работах Э. Дж. Брауде, Кулямина В.В., Э. Ванга и К. Квана, для разработки набора стандартных модулей, предназначенного для построения архитектурных диаграмм программных моделей протоколов встроенных систем. А также предлагается разработать методику, позволяющую строить архитектурные диаграммы на основе этого набора модулей, что позволит значительно упростить процесс проектирования программной модели. Кроме того, предлагается осуществлять верификацию полученных архитектурных диаграмм на предмет ошибок построения и организации взаимодействий между модулями, пользуясь теорией сетей Петри и в частности, теорией раскрашенных сетей Петри, развитой и доработанной К. Енсеном. Результатом такой работы может быть сгенерированный из полученной архитектурной диаграммы скелет программной модели на языке SystemC.
Целью работы является разработка методов и алгоритмов проектирования программных моделей сетевых протоколов для встроенных систем. Разработка методики проектирования программного обеспечения для реализации и верификации архитектурных диаграмм программных моделей стеков протоколов передачи данных, обеспечивающей повышение эффективности разработки и корректности программных моделей.
Для достижения поставленной цели в работе решались следующие задачи:
разработка метода проектирования и анализа программных моделей протоколов передачи данных;
разработка набора типовых модулей для построения архитектурных диаграмм программных моделей протоколов встроенных систем;
разработка метода организации межмодульных взаимодействий в программных моделях сетевых протоколов;
разработка метода перехода от архитектурной диаграммы программной модели к интерпретирующей ее раскрашенной сети Петри;
разработка алгоритма разметки раскрашенной сети Петри для осуществления верификации архитектурных диаграмм программных моделей;
исследование и разработка метода перехода от раскрашенной сети Петри к эквивалентной ей классической сети Петри в целях применения методов анализа классических сетей Петри к раскрашенным сетям;
разработка методики верификации архитектурной диаграммы на основе данных, полученных при анализе набора классических сетей Петри.
Методы исследования. Для решения поставленных задач использовались методы теории имитационного моделирования, теорий сетей Петри и раскрашенных сетей Петри, методы теории программирования и принципы объектно-ориентированного и компонентного программирования, методы теории множеств, теории комплектов.
Научной новизной обладают следующие результаты работы:
-
метод проектирования архитектурной диаграммы программной модели протокола передачи данных для встроенных систем по его спецификации;
-
набор модулей для проектирования архитектурных диаграмм программных моделей протоколов передачи данных для встроенных систем;
-
метод построения раскрашенной сети Петри на основе архитектурной диаграммы программной модели;
-
алгоритм разметки раскрашенной сети Петри для осуществления анализа движения фишек при помощи деревьев достижимости;
-
метод верификации архитектурной диаграммы программной модели протокола на основе результатов анализа сетей Петри.
Практическая значимость диссертации заключается в том, что в ней предложена методика построения программного обеспечения для разработки программных моделей протоколов и стеков протоколов передачи данных во встроенных системах, обеспечивающая упрощение и ускорение этого процесса разработки. Для апробации результатов работы был разработан программный комплекс ESPMS, реализующий методы и алгоритмы, описанные в данной диссертационной работе.
Внедрение и реализация результатов работы. Основные исследования и результаты диссертационной работы использованы в Институте высокопроизводительных компьютерных и сетевых технологий Государственного Университета Аэрокосмического Приборостроения для разработки программных моделей протоколов передачи данных для таких компаний как Nokia и ОАО «НИИ Авиационного оборудования». Результаты внедрения подтверждены соответствующими актами.
Апробация результатов работы. Основные положения и результаты диссертации докладывались и обсуждались на конференции Cadence CDNLife (2008 г.), Научных сессиях ГУАП (2008, 2009, 2010 гг.), а также международных конференциях FRUCT в 2009 и 2010 гг.
Публикации. По теме диссертации опубликовано семнадцать печатных работ, в том числе две статьи в рецензируемых журналах по перечню ВАК.
Основные положения, выносимые на защиту:
-
Метод перехода от спецификаций протоколов передачи данных к архитектурным диаграммам программных моделей этих протоколов, составленных из набора типовых модулей;
-
Метод формального описания архитектурных диаграмм программных моделей раскрашенными сетями Петри;
-
Алгоритм разметки раскрашенных сетей Петри для осуществления анализа движения фишек по сети Петри методом построения деревьев достижимости;
-
Метод верификации архитектурной диаграммы программной модели на основе результатов анализа достижимости набора классических сетей Петри, эквивалентных раскрашенной сети Петри по поведению.
Объем и структура работы. Диссертационная работа состоит из введения, списка используемых сокращений, четырех глав, заключения, списка использованных источников и трёх приложений. Диссертация содержит 144 страницы машинописного текста, 56 рисунков и 16 таблиц, а также приложения объемом 38 страниц, включая 10 рисунков и 3 таблицы. В списке использованной литературы 119 наименований.
