Designing robust quadcopter software based on a real-time partitioned operating system and formal verification techniques

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