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

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

Худов Ким Андреевич

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

Специальность

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

Автореферат

диссертация на соискание учёной степени кандидата технических наук

Москва 2006

J

Работа выполнена в Московском государственном университете приборостроения и информатики.

Научный руководитель: доктор технических наук, профессор Ульянов М.В.

Официальные оппоненты: доктор технических наук Мальцева C.B. кандидат технических наук Рогова О. Б.

Ведущая организация: ФГУП «КБПМ»

Защита состоится «16» мая 2006 г. в 14 часов на заседании Диссертационного Совета Д 212.119.02 Московского государственного университета приборостроения и информатики по адресу: 107076, г.Москва, ул. Стромынка, 20.

С диссертацией можно ознакомиться в научно-технической библиотеке Московского государственного университета приборостроения и информатики.

Автореферат разослан «15» апреля 2006 г.

Учёный секретарь Диссертационного совета к.т.н., доцент

Никульчев Е.В.

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

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

На сегодняшний день получили большое распространение интегрированные среды проектирования (ИСП), обеспечивающие разработку и отладку программного обеспечения для микроконтроллеров, однако, как правило, ИСП имеют средства отладки, ориентированные на проведение функциональной верификации в ручном режиме. При этом отсутствуют средства верификации других характеристик ПО, в частности характеристик связанных с обработкой событий во времени. В ИСП отсутствуют как методики, так и средства разработки спецификаций ПО. Существующие средства имитации взаимодействия ПО МК с внешними устройствами поддерживают имитацию взаимодействия только со стандартными интерфейсами. Перечисленные недостатки приводят к тому, что локализация ошибок остаётся сложным и трудоёмким процессом, в особенности в части драйверов ПО МК.

В настоящее время работы в области совершенствования интегрированных сред проектирования ведутся рядом организаций, таких как: НПК "Технологический центр" МИЭТ, Учебно-методический центр "Моторола - Микропроцессорные Системы" Московского государственного инженерно-физического института (МИФИ), Фирма "Фитон" и др. Однако вопросы создания специальных средств верификации драйверов ПО МК, затрагиваются в этих работах в недостаточной мере.

Теоретические вопросы обеспечения качества программных средств и верификации программ рассмотрены в работах Липаева В.В., Захарова В.А., Царькова Д.В., Евстигнеева В.А., Круглова М.Г., Лемана М.М. и др.

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

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

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

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

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

- исследованы современные средства разработки и отладки ПО микроконтроллерных устройств;

- проведён сравнительный анализ интегрированных сред проектирования с точки зрения предоставляемых средств отладки и верификации;

- выявлены характерные особенности функционирования ПО микроконтроллерных устройств;

- разработан комплекс программно-математических средств для решения задач верификации временных характеристик драйверов ПО МК, включающий в себя методику построения спецификаций ПО драйверов МК и методику построения моделей взаимодействия ПО МК с внешними устройствами;

- разработано математическое описание требований к временным характеристикам обработки событий в компонентах драйверов ПО МК;

- разработана математическая модель взаимодействия ПО МК с внешними устройствами, ориентированная на нестандартные интерфейсы. Научная новизна:

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

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

3. Разработана математическая модель взаимодействия ПО МК с внешними устройствами в целях создания входных воздействий для верификации ПО драйверов МК.

Практическая ценность работы: Применение разработанных методов и средств для верификации временных характеристик драйверов ПО МК обеспечивает:

- разработку спецификаций драйверов ПО МК;

- построение моделей взаимодействия ПО МК с внешними устройствами в

целях создания входных воздействий для верификации ПО драйверов МК;

- интеграцию полученных входных воздействий в среду разработки.

На основе результатов диссертационного исследования разработаны программные средства, зарегистрированные в Федеральной службе по интеллектуальной собственности (свидетельство № 2004612425 от 15.10.2004).

Результаты проведённых исследований и разработок внедрены в производственный процесс ЗАО «ВИСАТ-ТЕЛ» и ООО «АРКОМТЕЛ».

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

Апробация. По основным результатам работы были сделаны доклады на VII Всероссийской научно-технической конференции «Новые информационные технологии» (г. Москва, 2004 г), VIII Международной научно-практической конференции (г. Сочи 2005 г.) и на научном семинаре кафедры «Персональные компьютеры и сети» МГАПИ.

Публикации. Основные материалы диссертации опубликованы в шести печатных работах, получено свидетельство об регистрации разработанных программных средств в Федеральной службе по интеллектуальной собственности (свидетельство № 2004612425 от 15.10.2004).

Структура работы. Диссертационная работа состоит из введения, четырёх глав, заключения, приложения и библиографического списка. Основной текст диссертации изложен на 115 страницах, содержит 64 рисунка, 10 таблиц и библиографический список из 119 наименований.

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

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

В первой главе проведён анализ современных средств разработки микроконтроллерных устройств, проанализированы работы по аналогичной про-

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

Отмечено, что в настоящее время основным инструментом создания программного обеспечения для МК являются интегрированные среды проектирования, например, такие как: АУЯ-БикЦо, 1АК-8уз1ет и др.

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

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

- средства построения спецификаций ПО микроконтроллеров;

- модели внешних устройств или средства их имитации;

- средства создания моделей внешних устройств;

- средства анализа экспериментальных данных;

- средства интеграции с ИСП других производителей.

Таблица 1.

Средства / ИСП АУЯ-вЫю МРЬАВ УМ ЬАВ 1таве С гай

Программные средства реализации + + + +

Наличие имитационной модели вычислительного устройства + + + -

Наличие имитационных моделей внешних устройств - - + -

Наличие средств создания имитационных моделей внешних устройств - - - -

Наличие ручного режима создания входных воздействий + + + -

Наличие средств анализа + + + -

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

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

Проанализирован ряд программ микроконтроллерных устройств, в результате чего выявлена структура механизма переходов, зависящих от состояния внешних устройств, в программных модулях драйверов ПО МК (рис.1).

В результате анализа структуры и особенностей функционирования ПО микроконтроллерных устройств были выявлены следующие основные особенности, связанные с функционированием ПО МК во времени:

- источниками формирования событий могут являться: внешние сигналы, внутренние прерывания, внешние прерывания.

- функционирование ПО во времени происходит в двух режимах: ожидание события и обработка события (выполнение некоторых функций из определённого множества функций).

Разработано теоретико-множественное описание процесса регистрации и контроля правильности обработки событий во времени.

Прерывание О

Прерывание 1

Прерывание 2

г

Инициализация

Цикл ожидания события

1 г 'Г

Обработка Обработка

прерывания прерывания

г г

Возврат Возврат

Прерывание п

1 г

Обработка

прерывания

1 г

Возврат

Событие j,

тип р

Событие У+У _ | тип р

Начало обработки

события 1ы

Завершен»: ( обработки I события ^

Начало обработки

обработки

события ^+1)

события Ц,+1)

У - номер события;

р - тип события;

18 - время совершения события;

1ь - время начала обработки события;

^ - время окончания обработки события.

Рис. 1. Структура механизма переходов, зависящих от состояния внешних устройств, в программных модулях драйверов ПО МК

Регистрация обработки событий во времени описана в виде упорядоченной пятёрки:

где: N = Щ х ЛГ0 х х Ы0 х ЛГ0, ЛГ0 - множество неотрицательных целых чисел, ={0,1,2,...}, ТУ,-множество положительных целых чисел, N1 ={1,2,...}, у-номер события, у е //,, р— тип события, р е время совершения собы-

тия, /г е , время начала обработки события, /А е 7У0, г,- время завершения обработки события, е ^о •

Модель процесса регистрации и контроля обработки событий во времени описана в виде четвёрки:

М = (5,^,^0,

где: $ с N - конечное подмножество упорядоченных пятёрок из N, содержательно подмножество 5 представляет собой журнал регистрации обработки событий, ^ - конечное множество функций, Я- механизм реализации, проверочная функция. Множество функций

р = {/«, Л (М4),/ДМе)Ь

где: - функция создания нового события,

содержательно добавляет в Я новый элемент, /ь(к> Ч) ~ функция установки времени начала обработки события:

[с/. р, х,',) 0\ р, *,<л ]*к]

11 1(л р. '„ с/, р, !„ 1ь,а

'«) - функция установки времени окончания обработки события:

11 \и, р' '„ р, ¡„ ь, а

Содержательно функции /ь{к, и /е (к, 1е) устанавливают времена начала и окончания обработки события с номером к. Эти функции выполняются механизмом реализации Я в момент начала и завершения обработки события к соответственно.

В момент с = 0 — время начала контроля обработки событий во времени, устанавливается 5 = {0}. Механизм реализации модели Я, выполняя функции /„«■../»ОМД/Д^Л) создаёт |5| элементов в множестве 5 и регистрирует времена начала и окончания обработки событий.

По завершению временного интервала необходимо верифицировать правильность обработки событий во времени. С этой целью введено в рассмотрение конечное множество Р с. N0, как множество определённых типов событий. С учётом, того, что каждое событие должно быть обработано, и, следовательно, tJ<tb<te для каждого события из S, модель требований имеет вид: Q-.S В = {0,1}, S = {(/,Pj ,t„,tbJ,t,¿ )\j = 1,|S| 1*1

Q(S) = *4 • P, s hj ] ih,

y-i

где [a > b\ — нотация Айверсона: [а > ¿>] = -Г' °

[0, a <, b.

Если Q(S) = 1, то верифицируемая программа соответствует спецификации.

На основе разработанного теоретико-множественного описания разработана методика построения спецификаций ПО драйверов МК, этапы которой представлены на рис.2.

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

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

]

Рис.2. Основные этапы методики построения спецификаций ПО драйверов МК.

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

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

Разработана математическая модель взаимодействия ПО МК с внешними устройствами, взаимосвязь элементов которой показана на рис. 4. Выявлены, сформулированы и описаны основные характеристики модели:

- множество выходных сигналов е Г;

- множество входных сигналов х(г) е X;

- множество внутренних состояний е 2;

- функция выходов \|/;

- функция переходов <р;

- вероятностная функция выходов Ъ.

Рис.3. Функциональная схема комплекса.

Выделены базовые элементы, набор которых позволяет описывать модель взаимодействия ПО МК с внешними устройствами.

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

Рис.4. Взаимосвязь элементов математической модели.

На этапе 2 определяется множество Р= {/>,,р2>...,рп}, где Р —множество составляющих процесса функционирования; р1— элементы множества, которые в своей совокупности отражают модель функционирования. Каждому элементу р1 ставится в соответствие один или комбинация из нескольких типов базовых элементов, представленных множеством Мь = {тм,тЬ2,т/13} (множество базовых элементов), в соответствии с их назначением и возможностью реализации соответствующей функции.

В результате каждому элементу Р, у = 1, п процесса функционирования соответствует множество Мр1 = {т^,..,т1ц}, включающее в себя базовые элементы из Мь. На этапе 3 строится схема процесса функционирования модели взаимодействия ПО МК с внешними устройствами. По полученной схеме осуществляется окончательная формализация, в результате которой формируется модель взаимодействия ПО МК с внешними устройствами.

Рис. 5. Основные этапы методики построения моделей взаимодействия ПО МК с внешними устройствами

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

В четвёртой главе дано описание реализованных программных средств, структура которых приведена на рис. 6. В состав разработанных программных средств входят: программный имитатор взаимодействия ПО МК с внешними устройствами, графический анализатор, модуль интеграции и модуль экспериментальных вычислений.

Рис. 6. Структура разработанных программных средств.

Средства создания моделей взаимодействия ПО МК с внешними устройствами состоят из редактора структурных схем, редактора логических схем, и баз данных структурных элементов и логических элементов. Редактор структурных схем обеспечивает создание и редактирование структурных схем, на основе разработанных базовых элементов (рис.7). Элементы структурных схем могут быть описаны при помощи редактора логических схем.

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

Модуль интеграции состоит из формирователя файла входных воздействий и формирователя файла выходных воздействий.

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

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

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

На этапе отладки программ микроконтроллерных устройств разработанные программные средства обеспечивают:

- создание моделей взаимодействия ПО МК с внешними устройствами;

• - проведение экспериментов с моделями взаимодействия ПО МК с внешними устройствами;

- анализ экспериментальных данных;

- интеграцию с интегрированными средами проектирования;

- поддержку процесса верификации временных характеристик обработки событий в компонентах драйверов ПО МК.

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

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

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

В диссертации получены следующие основные результаты:

1. Разработан комплекс программно-математических средств для решения задач верификации временных характеристик драйверов ПО МК, включающий в себя методику построения спецификаций ПО драйверов МК и методику построения моделей взаимодействия ПО МК с внешними устройствами, программные средства зарегистрированы в Федеральной службе по интеллектуальной собственности (свидетельство № 2004612425 от 15.10.2004).

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

3. Разработана математическая модель взаимодействия ПО МК с внешними устройствами.

4. Разработана методика построения моделей взаимодействия ПО МК с внешними устройствами по нестандартному интерфейсу.

Разработанный комплекс программно-математических средств, как результат диссертационной работы внедрён в производственный процесс ООО «ВИСАТ-ТЕЛ» и ООО «АРКОМТЕЛ». В частности, результаты исследований применены в проектах спутниковых систем связи. Применение разработанных средств позволило выявить ряд ошибок, связанных с несогласованностью обработки событий во времени и сократить время реализации данных проектов.

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

Публикации по теме диссертации

1. Худов К.А. Программная эмуляция периферийных устройств. // Программное и информационное обеспечение систем различного назначения на базе персональных ЭВМ: Межвузовский сборник научных трудов / Под редакцией д.т.н. профессора Б.М. Михайлова - М.: МГАПИ, 2002, выпуск 5. С.155-156.

2. Худов К.А. Исследование микропроцессорных систем методом эмуляци-онного моделирования. // Программное и информационное обеспечение систем различного назначения на базе персональных ЭВМ: Межвузовский сборник научных трудов / Под редакцией д.т.н. профессора Б.М. Михайлова - М.: МГАПИ, 2002, выпуск 5. С.157-158.

3. Худов К.А. Математическое моделирование периферийных устройств. // Программное и информационное обеспечение систем различного назначения на базе персональных ЭВМ: Межвузовский сборник научных трудов / Под редакцией д.т.н. профессора Б.М. Михайлова - М.: МГАПИ, 2003, выпуск 6. С.267-268.

4. Худов К.А. Возможные подходы к математическому моделированию периферийных устройств. // Программное и информационное обеспечение систем различного назначения на базе персональных ЭВМ: Межвузовский сборник научных трудов / Под редакцией д.т.н. профессора Б.М. Михайлова - М.: МГАПИ, 2003, выпуск 6. С.269-271.

5. Худов К.А. Интегрированные среды проектирования, анализ и пути их совершенствования. // Программное и информационное обеспечение систем различного назначения на базе персональных ЭВМ: Межвузовский сборник научных трудов / Под редакцией д.т.н. профессора Б.М. Михайлова - М.: МГАПИ, 2003, выпуск 6. С.272-274.

6. Худов К.А. Моделирование программной системы эмуляции периферийных устройств на основе аппарата общей теории систем // Новые информационные технологии: Сборник трудов VII Всероссийской научно-технической

конференции (Москва, 24-25 марта 2004 г). / Под общ. Ред. А.П. Хныкина. -М.: МГАПИ, 2004. С.104-107.

7. Худов К.А. Программная система эмуляции внешней среды элементов управления. // Свидетельство об официальной регистрации программы для ЭВМ (свидетельство № 2004612425 от 15.10.2004).

ЛР № 020418 от 08 октября 1997 г.

Подписано к печати 10.04.2006 г. Формат 60x84. 1/16. Объем 1,25 п.л. Тираж 100 экз. Заказ № 62

Московский государственный университет приборостроения и информатики

107996, Москва, ул. Стромынка, 20

¿ош

ГЛУГ

р- 82 45

ВВЕДЕНИЕ.

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

Введение.

1.1 Основные этапы проектирования ПО МК.

1.2 Средства отладки ПО МК.

1.2.1 Аппаратные средства отладки.

1.2.2 Программные средства отладки.

1.3 Интегрированные среды проектирования.

1.4 Структура современных МК и связь с внешними устройствами. т> 1.4.1 Структура микроконтроллера.

1.4.2 Внешние устройства.

• 2.1 Общие проблемы верификации.33

2.2 Особенности ПО МК.39

2.3 Особенности верификации программ микроконтроллерных устройств.41

2.4 Заключение.50

4 ГЛАВА 3 МАТЕМАТИЧЕСКОЕ ОПИСАНИЕ МОДЕЛИ ВЗАИМОДЕЙСТВИЯ ПО МК С ВНЕШНИМИ УСТРОЙСТВАМИ.51

• Введение.51

3.1 Имитация взаимодействия ПО МК с внешними устройствами.51

3.1.1 Построение концептуальной модели взаимодействия внешних устройств с ПО МК.52

3.2 Математические модели.54

3.2.1 Формальная модель объекта имитации.54

3.2.2 Типовые математические схемы.57

3.2.3 Предварительная формализация объекта имитации.70

3.2.4 Разработка модели взаимодействия внешних устройств с ПОМК.71

3.2.5 Математическое описание подсхем.79 ф 3.3 Заключение.84

ГЛАВА 4 ПРОГРАММНОЕ ОБЕСПЕЧЕНИЕ КОМПЛЕКСА.86

Введение.86

4.1 Программный имитатор внешних устройств.86

4.1.1 Алгоритм работы ПО комплекса программно-математических средств.88

4.2 Программная реализация компонентов комплекса.93

Ф 4.3 Заключение.113

СПИСОК ЛИТЕРАТУРЫ.116

ПРИЛОЖЕНИЕ.124

ВВЕДЕНИЕ

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

На сегодняшний день получили большое распространение интегрированные среды проектирования (ИСП), обеспечивающие разработку и отладку программного обеспечения для микроконтроллеров, однако, как правило, ИСП имеют средства отладки, ориентированные на проведение функциональной верификации в ручном режиме. При этом отсутствуют средства верификации других характеристик ПО, в частности характеристик связанных с обработкой событий во времени. В ИСП отсутствуют как методики, так и средства разработки спецификаций ПО. Существующие средства имитации взаимодействия ПО МК с внешними устройствами поддерживают имитацию взаимодействия только со стандартными интерфейсами. Перечисленные недостатки приводят к тому, что локализация ошибок остаётся сложным и трудоёмким процессом, в особенности в части драйверов ПО МК.

В настоящее время работы в области совершенствования интегрированных сред проектирования ведутся рядом организаций, таких как: НПК "Технологический центр" МИЭТ, Учебно-методический центр "Моторола - Микропроцессорные Системы" Московского государственного инженерно-физического института (МИФИ), Фирма

Фитон" и др. Однако вопросы создания специальных средств верификации драйверов ПО МК, затрагиваются в этих работах в * недостаточной мере, ф Теоретические вопросы обеспечения качества программных средств и верификации программ рассмотрены в работах Липаева В.В., Захарова В.А., Царькова Д.В., Евстигнеева В.А., Круглова М.Г., Лемана М.М. и др.

В рамках проведённого исследования был рассмотрен ряд диссертационных работ: Непомнящий О.В. «Программно аппаратный комплекс проектирования цифровых систем обработки данных, базирующихся на схемах высокой и сверх высокой степени интеграции», Гончаровский О.В. «Разработка и исследование моделей и методов синтеза тестов для однокристальных микропроцессоров», Иванов А.Г. % «Программная имитация многопроцессорных схем, входящих в состав цифровых устройств», в которых затрагиваются проблемы разработки и г отладки цифровых систем. Однако, полученные авторами результаты имеют узконаправленную область применения и не могут быть напрямую использованы для совершенствования средств верификации программ и компонентов драйверов микроконтроллерных устройств.

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

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

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

Разработана математическая модель взаимодействия ПО МК с внешними устройствами в целях создания входных воздействий для верификации ПО драйверов МК.

На основе результатов диссертационного исследования разработаны программные средства, зарегистрированные в Федеральной службе по интеллектуальной собственности (свидетельство № 2004612425 от 15.10.2004).

Результаты проведённых исследований и разработок внедрены в производственный процесс ООО «ВИСАТ-ТЕЛ» и ООО «АРКОМТЕЛ».

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

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

Диссертационная работа состоит из введения, четырёх глав, заключения, приложения и библиографического списка. Основной текст диссертации изложен на 115 страницах, содержит 64 рисунка, 10 таблиц и библиографический список из 119 наименований.

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

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

В диссертации получены следующие основные результаты:

1. Разработан комплекс программно-математических средств для решения задач верификации временных характеристик драйверов ПО МК, включающий в себя методику построения спецификаций ПО драйверов МК и методику построения моделей взаимодействия ПО МК с внешними устройствами, программные средства зарегистрированы в Федеральной службе по интеллектуальной собственности (свидетельство № 2004612425 от 15.10.2004).

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

3. Разработана математическая модель взаимодействия ПО МК с внешними устройствами.

4. Разработана методика построения моделей взаимодействия ПО МК с внешними устройствами по нестандартному интерфейсу.

Разработанный комплекс программно-математических средств, как результат диссертационной работы внедрён в производственный процесс ООО «ВИСАТ-ТЕЛ» и ООО «АРКОМТЕЛ». В частности, результаты исследований применены в проектах спутниковых систем связи.

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

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

ЗАКЛЮЧЕНИЕ

1. А.Б. Боборыкин, Г.П. Липовецкий и др. Однокристальные микро ЭВМ. -М.: МИКАП, 1994. - 400 с.:илл.

2. Абдеев П.Ф. Философия информационной цивилизации. М.: ВЛАДОС, 1994.

3. А.Л. Гуртовцев, С.В. Гудыменко. Программы для микропроцессоров: Справ. Пособие. -М.: Высш. шк., 1989. -352 е.: илл.

4. Арсеньев Б.П., Яковлев С.А. Интеграция распределённых баз данных. СПб.: Лань, 2000.

5. Алексенко А.Г., Шагурин И.И. Микросхемотехника. -М.: Радио и связь, 1990.

6. Балашов Е.П., Григорьев В.Л., Петров Г.А. Микро и мини ЭВМ: Учебное пособие для вузов. -Л.: Энергоиздат. Ленинградское отделение, 1984.

7. Бродин В.Б., Шагурин И.И. Микроконтроллеры: Справочник. -М.: ЭКОМ, 1999.

8. Бусленко Н.П. Моделирование сложных систем. М.:Наука,1988.

9. Важенин В.И. и др. Методы моделирования сложных систем на ЭВМ // Труды Радиотехнического института АНСССР 1972. №12.

10. Ван Тассел, Д. Стиль, разработка, эффективность, отладка и испытание программ: Пер. с англ. -М.: Мир, 1985.

11. В.Я. Нерода, В.Э. Торбинский, Е.Л. Шлыков. Однокристальные микро ЭВМ MCS-51. Архитектура. -М.: изд. Диджитал Компоненте, 1995. -164с.:илл.

12. В.В. Сташин, А.В. Урусов, О.П. Мологонцева. Проектирование цифровых устройств на однокристальных микроконтроллерах. -М.: Энергоатомиздат, 1990. -224 е.: илл.

13. Веников В.А., Веников Г.В., Теория подобия и моделирования. -М.: Высшая школа, 1984.

14. В.А. Захаров, Д.В. Царьков. Эффективные алгоритмы проверки выполнимости формул темпоральной логики CTL на модели и их применение для верификации параллельных программ. // Программирование, 1998, №4.

15. В.Б. Стешенко. EDA. Практика автоматизированного проектирования радиоэлектронных устройств. -М.: Издатель Молгачаева С.В., Издательство «Нолидж», 2002.

16. Головин Ю.А., Яковлев С.А., Применение языков моделирования в обучении методам программной имитации сложных систем //Тез. докл. 6-й Междунар. конф. «Региональная информатика-98»; 4.1.-СПб, 1998.

17. Глушков В.М. Синтез цифровых автоматов. -М.: Физматгиз,1962.

18. Громов Г.Р. Очерки информационной технологии. -М.: Инфоарт.,1992.

19. Грушин С.И., Душутин И.Д., Мелехин В.Ф. Проектирование аппаратных средств микропроцессорных систем: Учеб. Пособие. -Л.: ЛПИ им. Калинина, 1990.

20. Глушков В.М., Цейтлин Г.Е, Ющенко Е.А, Алгебра, языки, программирование. -Киев; Наукова думка, 1978.

21. Дегтярев Ю.И. Исследование операций. -М.: Высшая школа,1986.

22. Ермаков С.М., Мелос В.Б. Математический эксперимент с моделями сложных стохастических систем. СПб.: Изд. ГУ, 1993.

23. Имитационное моделирование производственных систем./ Под ред. А.А. Вавилова. -М.: Машиностроение; Берлин: Техник, 1983.

24. Инструментальные средства персональных ЭВМ. В 10 кн. -М.: Высшая школа, 1993.

25. Карниган Б., Пайк Р. Практика программирования: Пер. с англ. -СПб.: Невский Диалект, 2001.

26. Карниган Б., Ритги Д. Язык программирования Си: Пер. с англ. -3 изд-е испр СПб.: Невский диалект, 2000.

27. Калашников В.В., Рачев С.Т. Математические методы построения стохастических моделей обслуживания. -М.: Наука, 1988.

28. Калянов Г.Н. CASE структурный системных анализ. -М.: Лори,1996.

29. Клейнен Дж. Статистические методы в имитационном моделировании.-М.: Статистика, 1978.

30. Кипер Сэм и др. Тестирование программного обеспечения: Пер. с англ. К.: Duesoft, 2000.

31. Корнеев В.В. Киселев А.В. Современные микропроцессоры. -М.:НОЛИДЖ, 1998.

32. Куприянов М.С. и др. Техническое обеспечение цифровой обработки сигналов. -СПб.: Наука и техника, 2000.

33. Каган Б.М., Сташин В.В. Основы проектирования микропроцессорных устройств автоматики. -М.: Энергоатомиздат, 1983.

34. Колосов В.Г., Мелехин В.Ф. Проектирование узлов и систем автоматики и вычислительной техники: Учеб. Пособие для вузов. -JL: Энегоатомиздат, 1983.

35. Куприянов М.С., Матюшкин Б.Д., Цифровая обработка сигналов: Процессоры.

36. Алгоритмы. Средства проектирования. -СПб.: Политехника,1998.

37. Лебедев О.Н., Мирошниченко А.И., Телец В.А. Изделия электронной техники. Цифровые микросхемы. Микросхемы памяти. Микросхемы ЦАП и АЦП: Справочник. -М.: Радио и связь, 1994.

38. Левенталь Л, Введение в микропроцессоры: программное обеспечение, аппаратные средства, программирование. -М.: Энергоатомиздат, 1985.

39. Липаев В.В. Методы обеспечения качества крупномасштабных программных средств. -М.: СИНТЕГ, 2003. -520 е., ил. (Серия «Управление качеством»).

40. Липаев В.В. Отладка сложных программ. М.: Энергоатомиздат.1993.

41. Математическая теория планирования эксперимента / Под ред. С. М. Ермакова. -М.: Наука, 1983.

42. Марк Д.А., Мак-Гоуен К. SADT. Методология структурного анализа и проектирования - М.: Метатехнология, 1993.

43. Мухин О.И. Компьютерная инструментальная среда. -Пермь: ПГТУ, 1991.

44. Микропроцессоры. В 3-х кн: Учеб. для втузов / П.В. Нестеров, В.Ф. Шаньчин, В.Л. Горбунов и др. / Под ред. Л.Н. Преснухина. -М.: Высшая школа, 1986.

45. Мурсаев А.Х., Угрюмов Е.П. Структуры и схемотехника современных интегральных полупроводниковых запоминающих устройств. -СПб.: ТЭТУ, 1997.

46. Микроконтроллеры AVR: от простого к сложному / М.С. Голубцов -М.: СОЛОН-Пресс, 2003.

47. М. Месарович, Я. Такахара. Общая теория систем: математические основы. Издательство «Мир», Москва 1978.

48. Непомнящий В.А., Рякин О.М. Прикладные методы верификации программ. М.: Радио и связь. 1988.

49. Основы технической диагностики. Книга первая. Под ред. П.П. Пархоменко.-М.г Энергия, 1976.

50. Питерсон Дж. Теория сетей Петри и моделирование систем. -М.: Мир, 1984.

51. Полляк Ю.Г., Филимонов В.А. Статистическое машинное моделирование средств связи. -М.: Радио и связь, 1988.

52. Полляк Ю.Г. Вероятностное моделирование на электронных вычислительных машинах. -М.: Сов. Радио, 1971. -400 с.

53. Применение микропроцессорных средств в системах передачи информации / Под ред. Б.Я. Советова. -М.: Высшая школа, 1987.

54. Прицкер А. Введение в имитационное моделирование и язык С ЛАМП. -М.:Мир, 1987.

55. Потёмкин И.С. Функциональные узлы цифровой автоматики. -М.: Энергоатомиздат, 1988.

56. Пухальский Г.И., Новосельцева Т.Я. Цифровые устройства: Учебное пособие для втузов. -СПб.: Политехника, 1996.

57. Системное обеспечение пакетов прикладных программ / Под ред.

58. A. А. Самарского. -М.: Наука, 1990.

59. Советов Б.Я. Информационная технология. -М.: Высшая школа,1994.

60. Советов Б.Я., Яковлев С.А. Моделирование систем. -М.: Высшая школа, 1985.

61. Советов Б.Я., Яковлев С.А. Моделирование систем (2-е изд.). -М.: Высшая школа, 1998.

62. Советов Б.Я., Яковлев С.А. Построение сетей интегрального обслуживания. -Л.: Машиностроение, 1990.

63. Солонина А.И., Яковлев Л.А. Основы построения микропроцессорных систем. -Учебн. пособие. -Л.: ЛЭИС, 1991.

64. Страуструп Б. Язык программирования С++. 3-е изд. / Пер. с англ. -СПб.; М.: Невский Диалект «Изд-во БИНОМ», 1999.

65. Савельев А.Я. Арифметические и логические основы цифровых автоматов: Учебник. -М.: Высшая школа, 1980.

66. Саломатин Н.А. Имитационное моделирование в оперативном управлении производством, 1984.

67. Солонина А.И., Улахович Д.А., Яковлев Л.А. Алгоритмы и процессоры цифровой обработки сигналов. -СПб.: БХВ-Петербург, 2001.

68. С.Д. Погорелый, Т.Ф. Слободянюк. Программное обеспечение микропроцессорных систем. Справочник. -К.: Техника, 1985.

69. Технология проектирования комплексов программ АСУ / В.В. Липаев, Л.А. Серебровский, П.Г. Гаганов и др.; Под ред. Ю.В. Асафьева,

70. B.В. Липаева. -М.: Радио и связь, 1983. -264 с.

71. Теория автоматов / Ю.Г. Карпов -СПб.: Питер, 2003.

72. Турчина Е.Д., Коробова И.Л., Соснина Н.Н, Структурно-функциональный подход к построению тестеров для дискретных устройств. -Тез.докл. в Межреспуб. шк.-сем. по тех.диагн., Таллин, 1984.

73. Угрюмов Е.П. Цифровая схемотехника. -СПб.: БХВ-Петербург,2000.

74. Фингаров И.Т., Симеонов И.Л., Стоянова Ц.С. Тестирование системы управления гибким производством средствами программной имитации // Приборы и системы управления. -1988. —№1.

75. Философские основы моделирования сложных систем управления / Андрющенко М.Н., Советов Б.Я., Яковлев С.А. и др. // Системный подход в технических науках (Методологические основы): Сб. научн. тр. -Л.: Изд. АН СССР, 1989.

76. Царьков Д.В. Использование модульности при верификации распределенных программ. // Тематический сборник факультета ВМиК МГУ им. Ломоносова Nl/Под ред. Л.Н.Королева -М.: МАКС Пресс, 2000.

77. Царьков Д.В. О выборе уровня абстракции модели при верификации параллельных программ // тезисы Международной конференции студентов и аспирантов по фундаментальным наукам "Ломоносов 2001", М, 2001.

78. Шеннон Р. Имитационное моделирование систем искусство и наука /пер. с англ. -М.: Мир, 1978. —418 с.

79. Шлеер С., Мейлор С. Объектно-ориентированный анализ: моделирование мира в состояниях. -Киев: Диалектика, 1993.

80. Шилд Г. Справочник программиста на C/C++: Пер. с англ. / Учебн. пособие. -М.: Издательский дом «Вильяме», 2000.

81. Шейнаускас Р.И. Построение тестов для схем с функционально сложными элементами." В кн. Логическое управление, М.: Атомиздат, МИФИ, 1981, вып.З.

82. Яковлев С.А. Эволюционные имитационные модели процессов и систем как методологическая основа интеллектуальных технологий обучения // Тез. докл. Междунар. конф. «Современные технологии обучения».-СПб., 1996.

83. Яковлев С.А., Шабуневич Е.В. Системное моделирование процессов управления информационными ресурсами в цифровых сетях интегрального обслуживания // Сб. науч. тр. «Вычислительная техника и новые информационные технологии». -Уфа: изд. УГАТУ, 1997.

84. Abraham J.A, Functional test for complex digital systems. -IEEE Test Conference, 1981.

85. Abramoviei M., Breuer M.A., Kumar K. Concurrent fault simulation and functional level modeling. Proc. 14-th Design Automat.

86. Bellon С., Saucier G. Hardware description levels and test for complex circuits. -18-th Design Automation Conference, 1981.

87. Brey B. The 8085A Microprocessor: Software, Programming and Architecture. Prentice-Han, Englewood cliffs. -N.J.,1986.

88. Breuer M.A., Friedaan A.D. Functional level primitives in test generation. -IEEE Trans, on Comput., 1980,vol. c-29,March.

89. David R., Thevenod-Posse P. Panorama des methodes des test non deterministes des circuits logiques. -RA1BO Automatique / Systems Analysis and control, 1979.

90. Dias F.J. Fault masking in combinatorial logic circuits, IEEE Trans, on Comput., 1975,vol. C-24, May.

91. Fujiwara H., Kinoshita K. Design of diagnosable sequential machine utilizing extra outputs. -IEEE Trans, on Computers, 1974, vol. c-25, February.

92. Gonenc G.A. method for design of fault detection experiments. -IEEE Trans, on Computers, 1970, vol.c-19, June.

93. Hennie F.C. Fault detection experiments for sequential circuits. -Eroc. 5 Ann. Symp. on Switching Theory and Logical Design, Erinceton University, 1964.

94. Hoare C.A.R. An axiomatic approach to computer programming. -Corn. ACM, 1969.

95. Howden W.E. Functional program testing and analysis. N.Y.: McGraw-Hill, 1987.

96. Johnson W.A. Behavioral-level test development, -16-th Des. Autom. Conf., 1979.

97. Kane J.R., Yan S.S, On the design of easily testable sequential machines. Proc. 12-th Ann. switching and Automate Theory Symposium, 1971.

98. Kohavi Z., Lavalle P. Design of sequential machines with fault detection capabilities. -IEEE Trans, on Electronic Computer, 1967, vol. EC-16, August.

99. Levendel Т.Н., Menon .P.R. Test generation algorithms for computer hardware description languages. -IEEE Trans, on Comput., 1982, vol. c-51, July.

100. Murakami S.,Kinoshita K., Ozaki H. Sequential machines capable of fault diagnosis. -IEEE Trans, on Comput., 1970, vol. c-19, November.

101. Muehldorf E.I., Savkar A.D. LSI logic testing an overview. IEEE Trans, on Comput., 1981, vol. 0-50, N 1.

102. Putzolu C.R., Roth J.P. A heuristic algorithm for testing of asynchronous circuits.- IEEE Trans, on Comput., 1971,vol. C-20, June.

103. Richard J.-P. Generation des test de detection pour les systems logiques. These doct. Univ. Paul Sabatier, Toulouse, 1974.

104. Robach С., Bellon С., Sausier G. Application oriented test for dedicated microprocessor systems. -Microp. and their appl. 5th EUROMICEO Symp., 1979.

105. Robach C., Saucier G. Application oriented microprocessor test method. -FTCS -10 Proc., -1980.

106. Sheppard D.A., Uranesic Z.G. Fault detection of binary sequential machines using R-valued test machines. -ISEE Trans, on Computers, 1974, vol. c-25, April.

107. Su Y.H. Hsieh Y.-I. Testing functional faults in digital systems described by register transfer language. -IEEE Test Conference, 1981.

108. Szygenda S.A., Lekkos A.A. Integrated, techniques for functional and. gate level digital logic simulation. -Proc. 10-th Design Automat Conf., 1973.

109. Thatte S.M., Abraham A, A methodology for functional level testing of microprocessors.-FTCS-8 Eroc.,1978.

110. Thatte S.M., Abraham J.A. Test generation for general microprocessor architectyres. -FTGS-9 Proc., 1979.

111. Thevenod P., David R. Random testing of the data processing section of microprocessor. -FTCS-11 Proc., 1981.

112. Интернет-университет Информационных Технологий http://www.INTUIT.ru.

113. Powertip Technology Corporation, http://www.powertip.com.tw.

114. Инструментальные редства разработки и отладки для микроконтроллеров, http://www.phyton.ru/cpl251/infos/articles.shtml.

115. Худов К.А. Программная система эмуляции внешней среды элементов управления. // Свидетельство об официальной регистрации программы для ЭВМ (свидетельство № 2004612425 от 15.10.2004).