Тема: Формальное описание взаимодействия микроконтроллера с программой с помощью композиции временных автоматов

Развитие микроэлектроники привело к широкому распространению электронных цифровых устройств. Эти устройства внедряются повсеместно, и в том числе для задач управления различными процессами от автоматов по выдаче кофе, до управления светофорами, открытия/закрытия дверей и т.п. Одним из основных управляющих элементов стал цифровой микроконтроллер. Микроконтроллер представляет собой вычислительный элемент малой мощности, обладающий рядом полезных свойств, таких как малые размеры, небольшое энергопотребление, дешевизна и универсальность. Универсальность микроконтроллеров достигается возможностью «вшить» в него нужную в конкретном случае программу, выполняя которую, он будет реализовывать необходимую логику управления. Таким образом, готовый к использованию управляющий элемент на базе микроконтроллера представляет собой аппаратно¬программный комплекс. И как любое другое устройство этот комплекс необходимо протестировать перед использованием, чтобы избежать в будущем непредвиденных или нежелательных ситуаций.
Классический способ построения тестов для исследуемой системы - это представить желаемое поведение этой системы в виде некоторой формальной модели [3], а затем воспользоваться известными методами построения тестов для этой модели. Поскольку на кафедре ИТИДиС хорошо изучены автоматные модели, для которых предложены оригинальные методы построения проверяющих тестов, то в данной работе предполагается использовать конечные автоматы и их расширения для описания спецификаций управляющих элементов на базе микроконтроллера.
Другой подход к проверке правильного функционирования устройств и программ в случаях, когда исходные коды системы (программы) доступны. Тогда по программе можно построить модель, которая будет описывать поведение этой программы. Затем необходимо сравнить две модели: исходную (спецификацию) и той, которая получилась в результате. И именно на этот подход к тестированию мы ориентируемся в работе.
Особенностью данной работы является рассмотрение не просто программы самой по себе, а «комплекса», состоящего из двух компонентов - программы и микроконтроллера, поскольку поведение итогового продукта существенно зависит не только от программы «зашитой» в микроконтроллер, но и от конкретных характеристик микроконтроллера (тактовая частота, используемая память особенности организации внешних интерфейсов и т.д.). Насколько нам известно, подобный подход нигде ранее не использовался до настоящего времени, кроме работы [6], идея которой развивается в нашей работе.
Целью данной работы ставится построение формальной модели системы «микроконтроллер-программа» с использованием композиции временных автоматов. В основание работы положена идея рассматривать микроконтроллер и программу, как два взаимодействующих между собой временных автомата [3]. Полученный временной автомат затем может быть использован для анализа правильного поведения (в том числе и с учётом временных аспектов поведения).
Для достижения цели в магистерской работе поставлены следующие задачи:
1. Обзор литературы и ознакомление с задачами, возникающими при тестировании цифровых устройств на основе микроконтроллеров .
2. Обзор основных языков программирования, используемых для
микроконтроллеров и изучение литературы по теории автоматов для построения диаграмм переходов.
3. Построение автоматов для описания компонентов системы «микроконтроллер-программа».
4. Замер временных задержек отдельных кусков (частей) программы.
5. Построение композиции из автоматов, извлечённых из программы сигнализации.
6. Обобщение результатов НИР магистранта. Составление и редактирование
текста диссертации.
Научная новизна:
1. Предложена структура композиции для систем, подобным системам «микроконтроллер-программа» (содержащим три компоненты) для случаев, в которых возникает необходимость, чтобы одна из компонент выдавала сигнал одновременно в разные каналы.
2. Разработан метод построения автоматной модели по отдельным компонентам (функциям) программ для определённого микроконтроллера. Также предложена методика для измерения времени выполнения отдельных компонентов программы.
Основные положения, выносимые на защиту:
1. Выражение «тернарной» композиции системы «микроконтроллер- программа» через бинарные композиции компонентов тернарной композиции.
2. Методика построения автоматной модели по отдельным компонентам (функциям) программ для определённого микроконтроллера. Также предложена методика для измерения времени выполнения отдельных компонентов программы.
Достоверность результатов: полученные в данной работе положения и выводы опираются на известные утверждения и теоремы теории автоматов и формальных языков.
Практическая ценность (значимость): полученный результат пригоден для анализа возникающих задержек в системе между внешним входным воздействием (условно нажатие кнопки) и внешней выходной реакцией (условно загорание/тушение светодиода), а значит можно оценивать предлагаемые решения о том, подходят те или иные временные ограничения к реальной модели или не подходят.
Апробация работы: Результаты работы были представлены на российской конференции с международным участием ICAM’2018.
Во введении обусловлена актуальность работы, сформулирована цель и задачи, представлены научные положения, выносимые на защиту и апробация работы.
В первой главе вводятся основные определения, используемые в магистерской диссертации, проводится обзор среди наиболее широко распространённых цифровых микроконтроллеров, а также языков программирования и компиляторов, используемых для них. Представляются основные моменты теории автоматов: их языки, композиция и другие основные операции, совершаемые над конечными автоматами.
Во второй главе описано построение диаграмм переходов (полу)автоматов для компонентов-программы по программной реализации охранной сигнализации, реализованной микроконтроллера STM32F407VG.
В третьей главе приводится метод, и результаты, полученные по нему замеров времени выполнения участков (фрагментов) кода.
В четвёртой главе рассмотрены различные типы и способы построения параллельной композиции из трёх элементов. Предложен способ построения «тернарной» композиции через композицию двух бинарных. Вкратце описан инструмент, используемый для автоматического построения параллельной композиции, а также показано представление формата описания временных автоматов для построения композиции системы через используемый в работе инструмент BALM-II.
В заключении кратко изложены основные результаты и итоги по ним, полученные в ходе выполнения работы над диссертацией.

Купить

Была изучена литература по конечным автоматам [1,4], проведено знакомство с основными используемыми языками программирования, существующими на данный момент, а также наиболее часто используемым компиляторам и микроконтроллерам [7]. Были построены автоматы по программе сигнализации для каждой из функций. Также, изучены работы [2 ,3, 6]. В них изложены основные идеи, которые предполагалось положить в основу данной магистерской работы.
В качестве языка, на который мы ориентировались в нашей работе, выбран язык C [7] как (де факто) единственный язык высокого уровня доступный для написания программ для микроконтроллера STM32F407VG. Для работы с микроконтроллером использовалась бесплатная программная среда, имеющая открытый код и основанная на базе Eclipse, предназначенная для разработки кода микроконтроллеров архитектуры ARM - CooCox CoIDE.
Произведены замеры задержек при выполнении (групп) команд (фрагментов кода) для каждой из функций в программе сигнализации. Построены композиции из автоматов, извлечённых из программы сигнализации.
Таким образом, произведено построение формальной модели системы «микроконтроллер-программа» с использованием композиции временных автоматов.
По итогам работы над магистерской диссертацией был подготовлен доклад для участия в XII Российской конференции с международным участием «Новые информационные технологии в исследовании сложных структур» (ICAM-2018 Алтай, 4-8 июня 2018 г.) на тему: «Определение временных характеристик автомата, описывающего систему «микроконтроллер-программа» в соавторстве с научным руководителем канд. физ.-мат. наук Громовым М.Л.
По результатам конференции опубликован сборник трудов конференции, входящий в базу РИНЦ.

Купить