Основой современных технологий проектирования и разработки сложных технических систем, обеспечивающих высокую надежность и масштабируемость, являются формальные методы, под которыми понимаются математически обоснованные методы спецификации, разработки и верификации аппаратного и программного обеспечения (ПО) технических систем [1, c. 370]. Дальнейшее эволюционное развитие проектируемой системы поддерживается за счет расширения формальных моделей, что обеспечивает соответствие свойств разрабатываемой системы заданным требованиям и определяет достоверность принятых технических решений.
При построении современных интегрированных средств проектирования бортовой аппаратуры (БА) космических аппаратов (КА) необходимо соблюдать следующие требования:
– применять методы интегрированной модульной разработки, обеспечивающие проектирование и интеграцию программного и аппаратного обеспечения, использовать архитектурные модели для автоматизации, а также унификации представления данных разрабатываемого проекта;
– использовать языки описания архитектурных моделей;
– использовать автоматизацию проектирования и представления данных проекта БА, в том числе в среде Заказчика;
– применять методы анализа и синтеза отдельных частей модели, а также верификации сложных технических систем на основе архитектурных моделей.
При решении задач такого типа требуется точная детализация бортовой аппаратуры на различных уровнях представления, а также гарантированная точность и трассируемость требований при анализе последствий в случае внесения изменений в процессе проектирования. При этом возрастающая техническая сложность проектов современных КА требует более тщательного анализа и проектирования. В таких условиях применение специалистами традиционных способов разработки БА, основанных на строгом описании всех требований и архитектурных решений в текстовых документах, становится чрезмерно трудоемким и подверженным ошибкам [2, с. 204].
Возможность подключить к разрешению указанных проблем программные средства автоматизации наталкивается на слабую структурированность информации, а также ее разнородность в различных проектах.
В связи с этим требуется учитывать спецификацию проекта с использованием универсальной модели для ее автоматизированной обработки.
Из вышеизложенного следует, что необходимо разрабатывать как технологии для оптимизации сложных программно-аппаратных проектов КА, которые позволили бы провести предварительную оценку качества изделия до появления опытного образца, так и его анализ на отказоустойчивость. В авиационной промышленности примерами таких решений являются интегрированные среды OSATE [3, c. 259], MASIW [4].
В данной статье представлено решение задачи применения архитектурного языка AADL (Architecture Analysis and Design Language), который в настоящее время является стандартом для моделирования архитектуры и выполнения требований по безопасности БА в аэрокосмической области [5], при проектировании системы бортовой аппаратуры.
Целью исследования является разработка способа проектирования интегрированной бортовой аппаратуры космического аппарата с использованием архитектурного языка AADL.
Рис. 1. Структурная схема применения формальных методов для спецификации моделей требований и поведения
Материалы и методы исследования
Применение способа проектирования интегрированной бортовой аппаратуры космического аппарата с использованием архитектурного языка AADL
Основой современного проектирования аппаратного и программного обеспечения бортовой аппаратуры космических аппаратов является применение формальных методов.
При проектировании и разработке систем формальные методы обычно включают следующие три вида деятельности [6]:
1. Системное моделирование – абстрактное представление аппаратного и программного обеспечения для анализа, моделирования и генерации кода.
2. Формальная спецификация – описание некоторых свойств, которым должна удовлетворять система.
3. Формальная верификация – проверка того, что модель системы удовлетворяет спецификации.
Необходимо отметить, что архитектурное проектирование является первоначальным этапом применения формальных методов при создании системы. Как показано на рис. 1, основная идея формального анализа требований к проектированию системы состоит в том, чтобы специфицировать модели поведения и требований бортовой аппаратуры, подлежащие их проверке с использованием выбранного формального научно-методического аппарата.
В настоящее время существуют определенные инструменты разработки технических систем, которые обеспечивают не только среду моделирования, но также и определенные встроенные модели их верификации на базе формальных методов. Наиболее известной средой разработки является программный продукт OSATE, который охватывает этапы разработки от требований к системе до программного кода, включая спецификацию требований, моделирование встроенных систем, оценку отказоустойчивости и т.п. [7].
На основе вышеизложенного в статье представлен способ проектирования интегрированной бортовой аппаратуры космического аппарата с использованием архитектурного языка AADL.
Способ проектирования интегрированной бортовой аппаратуры космического аппарата с использованием архитектурного языка AADL
Предметно-ориентированный архитектурный язык AADL предназначен для построения моделей технических систем, которые используются для представления статической модульной архитектуры программного обеспечения, архитектуры среды выполнения с точки зрения решения коммуникационных задач, а также архитектуры компьютерной платформы, на которой программное обеспечение развертывается, и любой физической системы или среды, с которыми система взаимодействует.
В языке AADL используются следующие встроенные средства для формализованного описания элементов системы и отношений между ними:
– на аппаратном уровне: элементарное устройство, процессор, память, порт, шина;
– на абстрактном уровне: виртуальный процессор, виртуальная шина, поток исполнения.
При разработке проекта БА его архитектура представляется как иерархия взаимодействующих компонентов. При этом разрабатываются спецификации интерфейсов, схемы реализации программного обеспечения, а аппаратные и физические компоненты группируются в пакеты для поддержки масштабирования и совместной работы проектировщиков.
Свойства компонентов в языке AADL представляют собой универсальный механизм семантического расширения конструкций языка, так как могут вводиться пользователем в соответствии с абстракциями создаваемой модели практически без ограничений.
Алгоритм проектирования интегрированной БА КА с использованием архитектурного языка AADL представлен на рис. 2.
На первом этапе работы осуществляется определение компонентов модели БА и размещение их спецификаций в пакеты.
На следующем этапе функционирования алгоритма производится интеграция отдельных компонентов в систему (разработка модели верхнего уровня) путем объявления экземпляров компонентов и их связей. При этом определяются окончательный вариант системы и ее реализация. Компоненты проектируемой системы могут быть аппаратными устройствами (например, датчики, устройства управления или интерфейсные блоки оператора) или представлять собой программное обеспечение.
Затем производится детализация состава процессов управления, которая включает в себя принятие решений, связанных с разделением функциональности, требуемых от БА для обеспечения контроля управления. Для каждого процесса управления создаются потоки исполнения, которые обеспечивают его функциональность.
Рис. 2. Схема алгоритма проектирования БА КА на языке AADL
Потоки могут получать данные от датчиков, выполнять операции масштабирования и фильтрации данных, пересылки данных в другие потоки. В случае композитного решения для процесса управления определяются дополнительные потоки, осуществляется спецификация их режимов выполнения и оптимизации вычислений.
Следующим этапом является добавление аппаратных компонентов алгоритма. После определения компонентов программного обеспечения системы управления производится определение аппаратного обеспечения среды выполнения, необходимое для поддержки ПО.
На этапе объявления физических соединений алгоритма продолжается интеграция проекта, добавляются экземпляры, необходимые для компонентов платформы исполнения реализации системы. Так как управляющее программное обеспечение системы, выполняющееся на процессоре, должно получать данные от датчиков и интерфейсных блоков, а также отправлять команды к исполнительным устройствам, то необходимо создать объявление, связывающее исполнительные устройства и шину.
Следующим этапом является привязка программного обеспечения к аппаратному обеспечению. Объявления в проекте позволяют специфицировать потокам исполнения определенный тип процессоров (для решения сложных вычислительных задач, например для сильно загруженного потока исполнения в современном встроенном оборудовании может быть указан тип процессора 500 или 1000 МГц). Также проводится анализ планирования и оценивается загрузка процессора потоками исполнения.
По построенной модели системы и подсистем строится формальное описание для верификации требуемых свойств разрабатываемой системы.
Рассмотрим применение формальных методов для верификации созданных архитектурных моделей. Авторами статьи в докладе [8] рассмотрена верификация протокола информационно-логического взаимодействия бортового комплекса управления (БКУ) и специальной аппаратуры с помощью формальной модели. Для проверки выполнимости свойств протокола информационного взаимодействия задаются формулы линейной темпоральной логики (LTL).
Пример проверки ограничения между двумя условиями Q и R:
(1)
где Q – БКУ провел тестирование,
P – РСА прошел режим тестирования аппаратуры,
R – БКУ передал команду на установку режима радиолокационного наблюдения.
Предложенный способ ранней диагностики ошибок СПО БА КА, основанный на темпоральной логике и общей формализованной модели данных, предоставляет возможность раннего обнаружения ошибок функционирования информационных протоколов программного обеспечения бортовой аппаратуры КА.
Другой областью применения формальных методов при проектировании бортовой аппаратуры является верификация задач систем реального времени (СРВ) [9, c. 454]. Планировать задачи в СРВ можно статическими и динамическими методами. В качестве политики планировщика со статическими приоритетами используется алгоритм RMS (Rate Monotonic Scheduling – планирование с монотонной скоростью). Статические приоритеты назначаются задачам в соответствии с продолжительностью цикла задания, поэтому наиболее короткая продолжительность цикла приводит к более высокому приоритету задачи. В случае применения планировщиком алгоритма EDF (Earliest Deadline First – первоочередное планирование более раннего срока выполнения) используется динамический принцип назначения приоритетов задачам. Планировщик задач, построенный на данном алгоритме, считает, что чем ближе предельный срок выполнения задачи, тем ее приоритет в системе выше.
Для описания свойств планировщика задач в СРВ был использован механизм дополнений языка AADL – Cheddar [10, c. 4], позволяющий расширять функциональную содержательность проектируемой архитектуры.
При моделировании приложения реального времени представляются набором задач. Для планирования времени исполнения каждая задача обычно определяется следующими временными параметрами [11, c. 7]:
− Ci – время выполнения задачи в наихудшем случае (worst-case execution time – WCET),
− Pi – период (продолжительность между двумя задачами),
− Di – критический срок завершения выполнения задачи;
− U – коэффициент использования процессора.
Необходимое условие того, что система реального времени будет исполнимой – коэффициент использования процессора должен быть меньше или равен 1:
1) по алгоритму RMS
(2)
2) по алгоритму EDF
. (3)
В качестве примера планирования проекта рассмотрим варианты оборудования КА в составе: три потока исполнения (поток управления thread_control, поток обработки данных thread_data и поток управления радиоканалом thread_radio) и один или два процессора (с тактовой частотой 1 ГГц).
При этом потоки исполнения задаются с конкретным периодом выполнения: поток thread_data – 2,…,18 мс, поток thread_radio – 1,…,6 мс, поток thread_control – 13,…,34 мс.
В табл. 1 представлены оценки производительности (общей загрузки вычислительных ресурсов) бортовой аппаратуры с двумя вариантами.
Результаты исследования и их обсуждение
Из анализа полученных результатов следует, что в случае применения одного процессора общая загрузка потоков превышает вычислительную производительность системы. Поэтому нет возможности построить корректное расписание, что приводит к срыву выполнения задачи обработки (потоки управления имеют больший приоритет в бортовых вычислительных системах). При варианте с двумя процессорами потоки используют 62 % вычислительных ресурсов проекта БА, что позволяет организовать дополнительные задачи обработки или передачи данных.
Оценки планирования потоков исполнения могут основываться на временных измерениях кода прототипа или данных для аналогичного проекта (например, системы с одинаковыми или сопоставимыми процессорами). Проводя анализ на ранней стадии процесса разработки с использованием технологии AADL, можно получить количественные прогнозы производительности проекта.
С целью определения требуемых вычислительных ресурсов для проектируемого КА радиолокационного наблюдения были проведены расчеты для различных реализаций алгоритмов по типовым операциям обработки радиолокационных данных – свертки радиолокационного изображения (РЛИ) по дальности и азимуту (табл. 2).
Анализ оценок производительности алгоритмов синтеза РЛИ показывает наибольший прирост при многопоточной реализации для свертки по дальности.
Как видно из представленных данных, увеличение производительности бортовой аппаратуры космического аппарата не приводит к линейному росту производительности специального программного обеспечения обработки радиолокационных данных.
Таблица 1
Предварительная оценка производительности бортовой аппаратуры
|
Потоки системы |
Вариант системы (1 процессор) |
Вариант системы (2 процессора) |
|
Поток обработки данных (thread_data) |
2–18 мс |
2–18 мс |
|
Поток управления (thread_control) |
13–34 мс |
13–34 мс |
|
Поток радиоканала (thread_data) |
1–6 мс |
1–6 мс |
|
Общая загрузка |
Превышение вычислительной производительности системы |
62,46 % |
Таблиц 2
Оценка производительности алгоритмов обработки радиолокационных данных
|
Наименование операции |
Размеры исходного файла, пиксели |
Время реализации варианта обработки, с |
|
|
Обычный (1 процессор) |
Многопоточный (2 процессора) |
||
|
Свертка РЛИ (дальность) |
20 × 23552 |
15,72 |
11,04 |
|
Свертка РЛИ (азимут) |
20 × 23552 |
5,28 |
4,48 |
|
Свертка РЛИ (дальность) |
200 × 23552 |
140,05 |
98,03 |
|
Свертка РЛИ (азимут) |
200 × 23552 |
76,35 |
64,89 |
Кроме указанных операций синтеза, на производительность обработки радиолокационных данных большое влияние оказывает выбор вычислительной платформы и способа реализации алгоритмов. Располагая на борту стандартизованной вычислительной платформой задачи оптимизации кода являются для данных средств приоритетными (в том числе низкоуровневое исполнение на языках Си и ассемблере и использование специализированных плат обработки).
Таким образом, приведенные оценки производительности проекта помогают избежать проблем на поздних этапах его создания (например, во время реализации кода или системной интеграции). Разработка БА КА с использованием архитектурного языка проектирования AADL позволяет автоматизировать процесс разработки бортовой аппаратуры, производить предварительное планирование потоков исполнения, использовать библиотеки компонентов проектов для стандартизованных решений, представлять в среде Заказчика данные по текущему состоянию проекта БА КА с целью оценки реального прогресса по работам и оценки обоснованности технических решений.
Заключение
Применение универсальных архитектурных языков при проектировании бортовых систем КА является необходимым условием создания современных интегрированных решений в космической отрасли.
В данной статье рассмотрен способ проектирования интегрированной БА КА с использованием архитектурного языка AADL. Представленный алгоритм основан на применении архитектурных методов разработки бортового комплекса КА, определяет процесс автоматизированного проектирования и интеграции программного и аппаратного обеспечения.
Результаты проведенных исследований могут быть использованы при создании новых образцов космической техники и разработки процедур верификации проектов интегрированной бортовой аппаратуры КА.