Способ верификации исходного кода программного обеспечения бортовой аппаратуры космического аппарата с применением темпоральной логики

При разработке современного программного обеспечения (далее – ПО) для космических аппаратов (далее – КА) с учетом размеров комплексов бортовой аппаратуры (далее – БА) и количества существенных деталей возможность подключать программные средства автоматизации наталкивается на разнородность и неструктурированность информации. Естественным шагом по преодолению указанной проблемы является формализация информации, переведение её в унифицированный машинный вид, что позволяет автоматизировать её обработку. Помимо традиционных методов отработки комплексов бортового оборудования космических аппаратов на наземных эксплуатационных стендах, для проведения тестирования программного обеспечения широко применяются формальные методы [1, с. 105]. Их целью является спецификация, разработка и верификация различных свойств программного обеспечения КА. При этом применяются математические методы, и поведение системы определяется с помощью формальных спецификаций [2–6]. Дальнейшее расширение проекта поддерживается на основе формальных моделей, обеспечивая тем самым соответствие свойств разрабатываемой системы требованиям, определяя её качество и надежность.

Для ранней диагностики неисправностей бортовой аппаратуры КА, возникающих при функционировании ПО, необходимо применение современных научных методов выявления ошибок. Цель статьи – разработка способа верификации исходного кода программного обеспечения бортовой аппаратуры КА с применением научно-методического аппарата линейной темпоральной логики.

Способ верификации исходного кода программного обеспечения бортовой аппаратуры космического аппарата с применением темпоральной логики

Особенности методов верификации исходного кода программного обеспечения с применением темпоральной логики

Одной из задач методов верификации является формальный анализ исходного кода программного обеспечения БА КА. Как видно из Рисунка 1, верификацию исходного кода можно разделить на определение соответствия исходного кода требованиям, отслеживаемость между исходным кодом и моделями поведения и статический анализ исходного кода.

При этом следует, что методы доказательства теорем и проверка модели для своего применения предлагают наличие спецификаций. Для применения метода доказательства теоремы спецификации должны быть извлечены как предшествующие и постусловия с преобразованием в аннотации программы на языке программирования Си. На конечном этапе метода применяются дедуктивные доказательства для проверки используемых аннотаций. Наиболее развитыми инструментами доказательства теорем, которые обычно используются в отрасли, являются VCC [7; 8] и Frama-C ¹ [9].

Другой метод верификации основан на проверке модели. Построив формальную модель из исходного кода и используя темпоральную логику (LTL, CTL и др.) для представления спецификаций требований, инструменты проверки моделей, определяют контрпример (путь исполнения системы), когда требования системы не выполняются [10]. Существует множество инструментов проверки модели, таких как SPIN ² , NuSMV ³ . При построении процесса разработки на базе инструмента NuSMV возможно прямое преобразование проверенных формальных моделей в исходный код.

Модели поведения

Спецификации требований

Инструментальные средства автоматической генерации кода (SCADE, Simulink, Event-B)

Инструментальные средства проверки модели (Spin, SMV, Event-B)

Инструментальные средства доказательства теорем (VCC, Frama-C)

Проверка модели (BLAST, СВМС)

Абстрактная интерпретация (PolySpace, Fluctuat)

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

Источник: здесь и далее рисунки выполнены авторами.

Вестник Российского нового университета

Серия «Сложные системы: модели, анализ и управление». 2025. № 3

Темпоральная логика фокусируется на соблюдении последовательности и времени событий и может описывать широкий спектр свойств, таких как безопасность, достижимость, справедливость и свойства реального времени. Для формальных спецификаций, написанных с использованием темпоральной логики, модель ПО должна быть представлена соответствующим формальным языком, таким как Promela, BDD ⁴ [11] и др.

Кроме того, цикл разработки программного обеспечения может быть значительно сокращен с помощью средств автоматической генерации кода. Например, инструменты SCADE от Esterel Technologies и Simulink от Mathworks имеют встроенные генераторы кода, которые могут преобразовывать модели поведения в эквивалентный код языка Си. Код, сгенерированный из формальной модели, обеспечивает отслеживаемость от исходного кода к модели поведения.

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

Наиболее часто используемые средства статического анализа исходного кода включают PolySpace ⁵ , Fluctuat (основаны на абстрактной интерпретации), SLAM, BLAST [12] и CBMC (основаны на проверке модели) и др.

Рассмотрим применение программных средств верификации исходного кода программного обеспечения, основанных на методе проверки модели.

Математическая постановка задачи верификации исходного кода программного обеспечения бортовой аппаратуры

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

Для проверки исполнения принятых свойств ПО бортовой аппаратуры задаются формулы линейной темпоральной логики LTL. В случае проверки допустимых границ массива из адресной области процесса необходимо убедиться, что при любом его функционировании значения границ массива не будут превышены.

Формула темпоральной логики LTL, выражающая данный инвариант, представлена выражением

G ( - array_round_ 1 v — array_round _ 2 ) ,                    (1)

где G – модальный оператор ‘глобально, все время’; array_round_1 – первое условие для границы многомерного массива; array_round_2 – второе условие для границы многомерного массива.

Логический инвариант проверки выполнения ограничения инициализации указателя на данные перед обращением функции обработки представлен выражением

( — function_load ) U ( pointer_data_init л — function_load ) ,             (2)

Способ верификации исходного кода программного обеспечения бортовой аппаратуры космического аппарата с применением темпоральной логики где U – модальный оператор ‘с тех пор, как’; function_load – начало выполнения процедуры загрузки данных; pointer_data_init – условие инициализации указателя на данные.

Логический инвариант проверки освобождения мьютекса при функционировании конкурирующих процессов представлен выражением

G ( mutex_ree ^ Gprocess_1_run ) v G ( mutex_ree ^ Gprocess_2_run ) , (3) где mutex_free – условие освобождения мьютекса; process_1_run – начало выполнения первого процесса; process_2_run – начало выполнения второго процесса.

Проверка получения сообщения путем обработки при функционировании двух асинхронных процессов информационного протокола представлена следующим выражением:

F process_rec_message ^ ( - process_send_message ) Uprocess_rec_message , (4) где F – модальный оператор ‘когда-нибудь в будущем’; process_rec_message – начало процесса обработки сообщений; process_send_message – начало процесса отправки сообщений.

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

На основе математической постановки задачи разработан способ верификации исходного кода программного обеспечения бортовой аппаратуры с использованием линейной темпоральной логики.

Способ верификации исходного кода программного обеспечения бортовой аппаратуры

Существует множество методов оценки качества кода и уменьшения количества остаточных ошибок ПО: ручное пошаговое выполнение кода, экспертная оценка, статический анализ исходного кода, модульное и интеграционное тестирование. Данные методы справляются с задачами при тестировании последовательного кода – определяют ошибки, но они не совершенны для задач тестирования многопоточного кода. Иногда применяют термин «граница качества», который накладывается стандартными методами тестирования [2].

Существующие способы верификации программного обеспечения бортовой аппаратуры не полностью охватывают вопросы проверки асинхронных или многопоточных версий программного обеспечения. С данной целью необходимо применять специальные инструменты, предназначенные для проведения формальной проверки асинхронного или многопоточного программного обеспечения. В качестве примера такого инструмента для программного обеспечения, написанного на языке программирования Си, рассмотрим применение Modex ⁶ .

Инструмент поддерживает три типа утверждений, которые пользователь может добавить в исходный код: базовые утверждения, утверждения ответа и утверждения приоритета.

Базовое утверждение имеет форму assert (ВЫРАЖЕНИЕ) . Проверяется, что выражение принимает значение ИСТИНА всякий раз, когда выполняется оператор утверждения во всех возможных системных исполнениях.

Вестник Российского нового университета

Серия «Сложные системы: модели, анализ и управление». 2025. № 3

Утверждение ответа имеет форму assert_r (ВЫРАЖЕНИЕ) . Проверяется, что выражение принимает значение ИСТИНА в течение конечного числа шагов после достижения утверждения во всех возможных исполнениях системы. Выражение должно стать истинным во всех системных исполнениях.

Утверждение приоритета имеет вид assert_p (ВЫРАЖЕНИЕ 1, ВЫРАЖЕНИЕ 2) . Проверяется, что выражение 1 истинно каждый раз, когда это утверждение выполняется, и остается истинным по крайней мере до тех пор, пока выражение 2 не станет истинным.

Тестовая программа, созданная для описанного выше инструмента, обычно определяет следующие сущности: процессы, взаимодействие процессов и объекты данных.

На Рисунке 2 представлен алгоритм верификации исходного кода программного обеспечения, поэтапную работу которого рассмотрим.

На первом этапе работы алгоритма тестовой программы для исходного кода определяются исходные файлы на языке Си с помощью одной или нескольких команд “%F” . Далее определяются целевые процедуры, которые будут включены в качестве потоков асинхронного процесса, при помощи команды “%X” . Кроме того, требуются некоторые тестовые драйверы, а также минимальная инфраструктура, необходимая для обеспечения связи между процессами в тестовой программе. Реализация их производится либо в исходном коде на языке Си как функции Cи, которые затем извлекаются как часть окончательной модели, или как процессы на языке Promela.

Далее рассматриваются определения стандартных версий таблиц сопоставления для сегментов “%L” в тестовой программе. В результате работы инструмента Modex создаются файлы с расширением lut или nlut. Данные файлы содержат полностью заполненные таблицы сопоставления для каждого целевого объекта (функции в исходном коде), на который была сделана ссылка в команде “%X” в тестовой программе с заполненными правилами преобразования по умолчанию.

На следующем этапе определяется необходимое покрытие сегментов “%L” в тестовой программе. Переопределяются операции потока, экземпляры процессов (используются операции языка Promela) и все операции отправки и получения данных.

Затем создается полная модель проверки исходного кода программного обеспечения.

Для этого применяется вызов команды modex без параметров:

Далее из модели создается код проверки. В случае необходимости определяется необходимый перечень переменных с помощью командной опции сегментов “%D” .

На заключительном этапе производится компиляция кода, сгенерированного верификатором Spin.

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

Таким образом, для проведения качественной диагностики неисправностей ПО, возникающих при функционировании бортовой аппаратуры КА, необходимо применение

Способ верификации исходного кода программного обеспечения бортовой аппаратуры космического аппарата с применением темпоральной логики современных методов выявления ошибок. Помимо традиционных методов тестирования исходного кода программного обеспечения требуется верификация исходного кода ПО БА с использованием моделей проверки (Model Checking), основанных на спецификациях темпоральных логик [2; 4; 5].

Рисунок 2. Алгоритм верификации исходного кода программного обеспечения бортовой аппаратуры

Вестник Российского нового университета

Серия «Сложные системы: модели, анализ и управление». 2025. № 3

Заключение

Для реализации современных методов верификации исходного кода ПО бортовой аппаратуры КА необходимо использовать математический аппарат темпоральных логик LTL и инструментальные средства верификации [2; 6; 8].

Представлен разработанный способ верификации исходного кода ПО бортовой аппаратуры с использованием линейной темпоральной логики LTL.

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