Разработка надёжного программного обеспечения для малых спутников с одноплатным бортовым компьютером

В современном процессе проектирования спутниковых систем наблюдается тенденция к экспоненциальному росту размеров программного обеспечния для бортовых компьютеров, что в конечном итоге приводит к созданию неэргономичных и чрезмерно сложных интерфейсов. Несмотря на. то, что аппаратное обеспечение достаточно стандартизировано в форме так называемых COTS-компонентов (components-off-the-shelf), программное обеспечение всегда зависит от типа полезной нагрузки. Это приводит к дифференциации конструкций космических аппаратов в зависимости от учреждений, ответственных за. производство этих систем. Каждый из этих проектов должен пройти процесс проверки, который становится дорогостоящим на. поздних стадиях разработки. В качестве иллюстрации, на. рис. 1 представлена, широко изестная V-диаграмма процесса, разработки в системной инженерии [1].

Каждый уровень диаграммы соответствует уровню детализации проекта, слева. - на. этапе проектирования, справа - на этапе реализации и тестов. Исходя из структуры диаграммы, нетрудно заметить, что чем раньше ошибка, в архитектуре аппарата, будет замечена, тем быстрее и экономнее будет её исправить. Так, например, если ошибка, обнаружена.

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

План валидации системы

Системные требования

Концепция плана операции

Анализ осуществимости

Высокоуровневое проектирование

План верификации системы

План верификации

< подсистем

Детальное проектирование

План тестирований

Верификация подсистем

Разработка программного / аппаратного обеспечений

Эксплуатация и обслуживание

Валидация системы

Верификация системы

Тест отдельных модулей

Документ / Утверждение

Время

Реализация

Процесс разработки

Рис. 1. V-диаграмма системной инженерии

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

Разумное решение к поставленной проблеме - указать и проверить системные требования на ранних стадиях проектирования, убедившись в том, что модель работает должным образом (метод correctness-by-construction). Таким образом, строгий подход был введен для построения сложных систем - architecture-based design, который интегрирует более простые системы в сложные и проверяет, сохраняют ли они заданные свойства, технические требования и ограничения своих простейших составляющих. Язык моделирования SysML может использоваться для описания системы в целом, а затем для проверки некоторых свойств. Однако он недостаточно строгий, чтобы обеспечить автоматическую верификацию и валидацию программного обеспечения [11].

Поэтому в данной статье предлагается использовать фреймворк Behavior-Interaction-Priorities (BIP) [12]. BIP может использоваться для формального моделирования сложных систем и предоставляет набор инструментов для их проверки, валидации и генерации кода. Также BIP позволяет использовать итеративный подход при проектировании спутников и адаптируется к изменению аппаратного обеспечения.

Мы использовали BIP фреймворк, чтобы показать возможность спроектировать логику работы малых спутников и скомпилировать её в машинный код, который должен выполняться на одноплатном компьютере (например, BeagleBone Black с процессором Cortex-A8). Эта работа доказала свою техническую осуществимость и выявила ряд проблем с выбранным подходом. В этой статье мы представим основные принципы структуры BIP, нашу реализацию и задачи для реализации.

2.    Преимущества строгого подхода

Наш подход заключается в использовании формальной структуры валидации для создания и проверки логики системы с последующим переносом кода C++ непосредственно на микропроцессор. Он обеспечивает следующие качества всей системы (необходимые для спутникового оборудования [13]):

• •    Надёснсностъ - разработчик не должен беспокоиться о роли аппаратного обеспечния при продумывании логики системы. Перед началом работы с драйверами оборудования можно будет смоделировать поведение всей системы, используя установленные шаблоны проектирования. Система также будет проверена на соответствие ряду правил проектирования. Таким образом, можно будет устранить ряд ошибок или неясностей, которые обычно обнаруживаются в конце цикла разработки проекта.

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

• •    Портативность - система будет иметь аппаратный интерфейс в виде низкоуровневых функций С или C++, которые реализованы для отражения возможностей выбранных компонентов. В случае замены компонентов нам нужно только заменить соответствующий драйвер, сохраняя при этом общую логику системы. Это было бы серьезным улучшением текущего состояния дел, где смена компонентов также требует модификации логики. Такие изменения чрезвычайно дороги, поскольку логика уже реализована в коде С ++ и требует большого количества реверс-инжиниринга.

3.    ВІР фреймворк 3.1.    Характеристики BIP фреймворка

Наш подход основан на фреймворке ВІР [14] для компонентно-ориентированного проектирования correct-by-construction приложений. BIP предоставляет простой, но мощный механизм для координации параллельно работающих компонентов, накладывая три уровня: Behavior (Поведение), Interaction (Взаимодействие) и Priority (Приоритет).

Во-первых, поведение компонентов описывается портами, которые обозначают переходы между компонентами, и данными, хранящимися в локальных переменных. Порты также могут экспортировать часть локальных переменных, предоставляя доступ к данным компонента.

Во-вторых, наборы взаимодействий определяют координацию компонентов. Взаимодействия - это наборы портов, которые определяют допустимые синхронизации между компонентами. Модель взаимодействия определяется структурой соединений (связей) [6].

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

Состояние компонента BIP не может быть напрямую изменено любым другим компонентом. Порты компонентов BIP не являются ни данными ввода/вывода, ни методами, которые должны быть вызваны. Вместо этого порт обозначает событие, которое происходит, когда компонент выполняет переход, для которого этот порт является обозначением. Таким образом, соединение обеспечивает синхронизацию таких событий. Механизм BIP решает в каких компонентах должны выполняться какие переходы, основываясь на полной информации о соединениях и приоритетах в системе.

Атомы (Atoms). Системы BIP собираются из атомарных компонентов (атомов), соответствующих параллельно испоняемым процессам, таким как алгоритмы управления, драйверы шины и памяти и т.д. Атомы имеют непересекающиеся пространства состояний. Атом определяется соответствующими наборами портов, состояний, переходов, переменных и update-функциями, которые связаны с переходами.

Для примера возьмём рис. 2 [15], на котором изображена BIP-модель проблемы «обедающих философов» [2]. Проблема формулируется следующим образом:

Условие: N философов сидят вокруг круглого стола, перед каждым философом стоит тарелка с едой. Вилки лежат на столе между каждой парой ближайших философов. Каждый философ может либо есть, либо размышлять. Философ может есть только тогда, когда держит две вилки - взятую справа и слева. Каждый философ может взять ближайшую вилку (если она доступна) или положить - если он уже держит её. Взятие каждой вилки и возвращение её на стол являются раздельными действиями, которые должны выполняться одно за другим.

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

Рис. 2. ВІР компонента, из четырёх обедающих философов

Данная система состоит из 8 атомов, 4 из которых являются философами Р, другие 4 -вилками Ғ. Атом философа Р может находиться в 2-х состояниях - e (eating) и h (hungry). Переход из одного состояния в другое отмечен также и в названии соответствующего порта: release (положить вилку на стол) и get (взять видку со стола). Атом вилки Ғ чуть сложнее и может находиться в 3-х состояниях - u_r (used in right), и/ (used in left) и f (finished). Переходы подчинятюся следующей логике: если вилка свободна, то только тогда её можно использовать одному из философоф (справа, или слева). Описание соединений для этого примера, в следующем параграфе.

Соединения (Connectors). У системы на рис. 2 имеется 8 соединений, 4 из которых синхронизируют взятие вилок одним из философов (порты use_r,use/,get), другие 4 синхронизируют возвращение вилок на стол (порты free_r,free/, release). Это означает, например, что переход философа Ро из состояния h в состояние e обязательно должно сопровождаться переходом вилки Ғо из сос тояния f в состояние и/ и переход ом вилки Ғ1 из сос тояния f в состояние u_r (т.е. соответствующие порты переходов синхронизированы).

Соединения определяют набор взаимодействий между компонентами на основе типов портов, которые могут быть либо триггерами, либо синхронами (рис. За). Если все соединённые порты являются синхронами, то происходит синхронизация типа рандеву, т.е. требуемое взаимодействие может произойти, только если все участвующие компоненты разрешают переход на этих портах (рис. 36). Если у соединения есть хотя бы один триггер, то синхронизация происходит по типу широковещания, т.е. разрешённые взаимодействия - это все непустые подмножества подключенных портов, содержащих по крайней мере один из портов триггера (рис. 36). Более сложные соединения могут быть построены иерархически (рис. Зв).

• (а) Типы портов: Синхрон Триггер

  • (б)    Плоские соединения:

  
  
  

  a b c

  Рандеву

  {abc}

  
  
  

  abc

  
  
  

  abc

  
  

  Широковещание

  {a, ab, ac, abc} {a, b, ab, ac, bc, abc}

  
  
  

  a b c a b c

  Атомарное широковещание

  
  

  • (в)    Иерархические соединения:   Рандеву

  
  

  {abc}

  
  

  {a, abc}

  
  
  

  bc

  
  

  Причинная цепочка {a, ab, abc}

  
  
3.2.    Обеспечение свойств — Архитектуры

Рис. 3. Типы соединений в BIP фреймворке

Приоритеты (Priorities). На рис. 2 не показан пример использования приоритетов в системе BIP, однако легко представить, зачем они нужны. Если соединители разрешают несколько переходов одновременно с участием одних и тех же портов, можно самостоятельно указать, какой именно переход должен исполняться сначала. Иначе говоря, можно установить приоритет взаимодействия. В общем случае нет необходимости устанавливать приоритеты во всех конфликтных ситуациях: согласно семантике BIP, одному из возможных взаимодействий выбирается максимальный приоритет недетерминированным путём [6].

Комплексы (Compounds). Наконец, комплексные компоненты состоят из наборов подкомплексов (атомов и / или комплексов), соединений и приоритетов. Комплекс может экспортировать порты, определенные в соединениях, для взаимодействия с другими компонентами в большем комплексе. Так, на рис. 2 4 философа и 4 вилки, соединённые в одну компоненту, являются комплексом.

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

Известно, что в задаче об «обедающих философах» основная цель - избежать взаимной блокировки, например, когда все N философов будут сидеть с вилкой в левой руке и ждать, пока кто-нибудь не положит на стол свою. Модель на рис. 2 не решает данную проблему. Один из способов решения проблемы - добавление координатора, который будет сохранять очерёдность питающихся философов. Так, на рис. 4 показана простая ВІР модель для взаимного исключения между двумя задачами [9]. Он состоит из двух компонентов, моделирующих собственно задачи, и одного компонента-координатора С . Четыре бинарных соединения синхронизируют каждое из действий 61,62 (или fi,f2) в задачах с действием t (пли т) координатора (обозначения здесь: 6 - begin. f - finish, t - take, r -release).

Рис. 4. Модель взаимного исключения в ВІР фреймворке

Архитектуру можно рассматривать как модель ВІР, в которой некоторые атомарные компоненты рассматриваются как координаторы, а остальные являются параметрами. Когда архитектура применяется к набору компонентов, эти компоненты используются в качестве операндов для замены параметров архитектуры. Таким образом, на рис. 5 показана архитектура, которая обеспечивает свойство взаимного исключения для любых двух компонентов с интерфейсами {61, fi} и {62^2}, удовлетворяющая следующему свойству:

Как только компонент выполнил переход f, он не войдет в критическую секцию, если он не выполнит переход 6.

Для компонентов-операндов на рис. 4 критической секцией является состояние work.

Композиция архитектур основана на ассоциативном, коммутативном и идемпотентном операторе ’ф’ [16]. Если две архитектуры Лі и Л2 обеспечивают соответствующие свойства Ф1 и Ф2, то их композиция Лі ФЛ2 обеспечит свойство ФіЛФ2, что значит, что оба свойства сохранены композицией архитектур.

Поскольку архитектуры ограничивают поведение компонентов, к которым они применяются, отсутствие взаимной блокировки, как правило, не может быть гарантировано конструкцией. Вместо этого отсутствие взаимной блокировки должно быть проверено апостериори с помощью специальных инструментов, таких как DFinder [17].

4.    Реализация

В качестве образца взята работа [18], в которой выполняется полный рабочий процесс проектирования (т.е. анализ требований, логическое проектирование, разработка В1Р-кода, компиляция в микропроцессор и тестирование) подсистемы управления командами и данными (CDMS) для проекта CubETH [19], тем самым демонстрируя осуществимость использования концепта ВІР для малых спутников. В качестве микроконтроллера был выбран EFM32GG880 ARM Cortex-МЗ со 128 КБ ОЗУ и 1 МБ программной памяти, работающий на частоте 48 МГц. CubETH - это швейцарский проект [20] по созданию 1U кубсата для демонстрации новых технологий в области спутниковых систем навигации при использовании COTS-компонент аппартного обеспечивания.

Вся модель состояла из 56 атомов и не вместилась в доступную память модели спутника. Таким образом, обоснование было сделано для сокращенной модели программного обеспечения, содержащей 19 атомов и 60 соединений.

Основными сложностями были: 1) необходимость статического распределения памяти, 2) большой объем ОЗУ сгенерированного кода и 3) необходимость компиляции процессора BIP и сгенерированного кода с помощью специального компилятора ARM. Объем потребляемой памяти сгенерированного кода показан на рис. 6. Объем ОЗУ (128 МБ) на процессоре Cortex-АЗ является основным ограничением, ограничивающим число атомов и соединений (и, следовательно, сложность модели), которые могут быть использованы одновременно. Доступно только статическое распределение, поэтому невозможно перераспределить данные в основную память. Это ограничение легко снимается на более мощных платформах. Выбранная архитектура использовалась из-за низкого энергопотребления и, в более общем смысле, режима ограничения мощности на 1U кубсате.

ОЗУ (128 КБ)

■ Статическая ■ Динамическая ■ Стэковая ■ Свободная

Рис. 6. Объём потребляемой оперативной памяти сокращённой BIP модели

Модель, разработанная в [18], была проанализирована для того, чтобы определить, какие паттерны проектирования повторяются. Эти шаблоны были формализованы как архитектуры BIP (см. раздел 3.2) и использовались в [9] для разработки новой модели BIP бортового программного обеспечения CubETH с нуля. Более конкретно, начиная с небольшого набора атомов, которые реализуют простейшие ключевые функциональные возможности программного обеспечения, мы систематически применяли вышеупомянутые архитектуры для сохранения свойств, налагаемых требованиями, сформулированными для бортового программного обеспечения. Поскольку свойства сохраняются посредством архитектурной композиции [16], все свойства, которые мы связали с требованиями CubETH, удовлетворяются конструкцией этой последней модели.

Архитектуры обеспечивают требуемые свойства, ограничивая совместное поведение компонентов-операндов (раздел 3.2). Из чего следует, что совместное применение архитектур может привести к взаимным блокировкам. Был использован инструмент DFinder [17] для проверки свободы от блокировок исследуемой модели. DFinder применяет композиционную проверку на моделях BIP, переоценивая набор достижимых состояний и символически проверяя, что пересечение полученного набора и набора блокировочных состояний пусто. Такой подход позволяет DFinder анализировать очень большие модели. Инструмент надежный, но неполный: из-за вышеупомянутого приближения он может давать ложные срабатывания, то есть потенциальные тупиковые состояния, которые недоступны в конкретной системе. Тем не менее модель исследования показала отсутствие блокировок. Таким образом, никакого дополнительного анализа достижимости не потребовалось.

Также нами была проверена возможность использовать полную модель BIP из [18] на одноплатном компьютере, которая была бы не урезана из-за недостатка программной и оперативной памяти. В качестве одноплатного компьютера был использован BeagleBone Black (рис. 7), в основе которого находится процессор ARM Cortex-A8. В отличие от микроконтроллера EFM32, в BeagleBone намного больше памяти - 512 МБ ОЗУ, однако и намного больше электропотребление, что сильно сказывается на применимости данного устройства в проектах с малыми спутниками. Мы попробовали откомпилировать процессор BIP напрямую внутри BeagleBone и, соответственно, компилировать модель для системы управления данными также напрямую внутри одноплатного компьютера, без использования тулчейна.

Рис. 7. BeagleBone Black

Так как компиляция процессора BIP внутри архитектуры ARM имеет свою специфику, к которой относится отказ от оптимизации при верификации сгенерированного кода из-за несоответствия предустановленной для BIP версии Java с доступными на BeagleBone, мы посчитали необходимым опубликовать трудные моменты сборки процессора BIP для одноплатного компьютера:

• 1)    Компиляторы GCC и G++ версий не старше 4.8.5, headless Java SE не моложе 1.7.

• 2)    Оптимизация должна быть пропущена, так как она использует предустановленный LPSolve java файл.

• 3)    Реконфигурация процессора BIP сопровождается требуемыми вашей системой изменениями в PackageLoader’e.

5.    Заключение

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

В этой работе мы продемонстрировали осуществимость BIP-подхода для разработки спутникового программного обеспечения. Ограничения процессора Cortex-МЗ привели к уменьшению модели. Однако демонстрация уменьшенной модели на плате кубсата прошла успешно. В1Р-подход также возможно использовать на одноплатных компьютерах типа BeagleBone Black, которые позволяют использование гораздо большего количества памяти, однако для этого следует учесть энергетические параметры планируемой миссии.

Оказалось, что крайне полезно иметь возможность проверять логику проектирования перед компиляцией на аппаратное обеспечение. Кроме того, применение подхода проектирования на основе архитектуры BIP позволило разработать аналогичную модель, в которой все требуемые свойства обеспечиваются конструкцией. Этот подход требует только проверки модели на наличие взаимных блокировок, чего удалось добиться с помощью инструмента DFinder из набора инструментов BIP.

Эта работа показала, что для относительно небольших миссий, таких как кубсаты, фреймворк BIP можно использовать для разработки полного бортового программного обеспечения.