Математическое и программное обеспечение средств верификации программ микроконтроллерных устройств тема диссертации и автореферата по ВАК РФ 05.13.11, кандидат технических наук Худов, Ким Андреевич

• Худов, Ким Андреевич
• кандидат технических наук
• 2006

Оглавление диссертации кандидат технических наук Худов, Ким Андреевич

ВВЕДЕНИЕ.

ГЛАВА 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. Разработана методика построения моделей взаимодействия ПО МК с внешними устройствами по нестандартному интерфейсу.

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

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

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

ЗАКЛЮЧЕНИЕ

Список литературы диссертационного исследования кандидат технических наук Худов, Ким Андреевич, 2006 год

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).