Сборники трудов ИСП РАН


Разработка программного обеспечения квадрокоптера с повышенными требованиями к надёжности на основе партицированной ОС и технологий формальной верификации

Старолетов С.М. (АлтГТУ, Барнаул, Россия)
Амосов М.С. (АлтГТУ, Барнаул, Россия)
Шульга К.М. (АлтГТУ, Барнаул, Россия)

Аннотация

Создание надежных беспилотных летательных аппаратов является важной задачей для науки и техники, потому что необходимо обеспечивать надежность таких решений. В этой статье предлагается использование аппаратного прототипа квадрокоптера и разработка программного решения для полетного контроллера с высокими требованиями к надежности, которое будет соответствовать новым стандартам для программного обеспечения авионики и будет использовать существующие программные решения с открытым исходным кодом. В ходе исследования мы анализируем состав квадрокоптеров и полетных контроллеров для них. Мы описываем открытое программное обеспечение Ardupilot для беспилотных летательных аппаратов, контроллер APM и методы ПИД-регулирования. Сегодняшним стандартом надежного программного обеспечения для бортовых контроллеров являются партицированные операционные системы реального времени, которые способны реагировать на события от оборудования с ожидаемой скоростью, а также разделять процессорное время и память между изолированными разделами. Хорошим примером такой ОС с открытым исходным кодом является POK (Partitioned Operating Kernel). В репозитории она содержит пример описания системы для дронов с использованием языка AADL с моделированием аппаратного и программного обеспечения решения. Мы применяем такую технику к демонстрационной системе, которая работает на реальном оборудовании и содержит процесс управления полетом с PID-регулятором в виде изолированного процесса. Использование партицированной ОС выводит надежность программного обеспечения полетного контроллера на новый уровень. Для того, чтобы повысить уровень корректности логики управления, мы предлагаем использовать формальные методы верификации и демонстрируем примеры проверяемых свойств на уровне кода, используя дедуктивный подход, а также проводя моделирование на уровне киберфизической системы с использованием динамической дифференциальной логики для доказательства устойчивости.

Ключевые слова

квадрокоптер; операционная система; партицирование; ARINC 653; формальная верификация

Издание

Труды Института системного программирования РАН, том 31, вып. 4, 2019, стр. 39-60.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2019-31(4)-3

Для цитирования

Старолетов С.М., Амосов М.С., Шульга К.М. Разработка программного обеспечения квадрокоптера с повышенными требованиями к надёжности на основе партицированной ОС и технологий формальной верификации. Труды Института системного программирования РАН, том 31, вып. 4, 2019, стр. 39-60. DOI: 10.15514/ISPRAS-2019-31(4)-3.

Полный текст статьи в формате pdf (на английском) Вернуться к содержанию тома