Извлечение архитектурной информации из исходного кода ARINC 653 совместимых приложений с использованием алгоритма CEGAR

Модельно-ориентированный подход к разработке позволяет построить архитектурную модель существующей системы по ее исходному коду. Построенная архитектурная модель существующей системы позволяет проанализировать ее различные статические и динамические характеристики, включая производительность, требуемые аппаратные ресурсы, надежность и другие. Архитектурные модели могут использоваться как для анализа, так и для повторного использования некоторых компонентов существующей системы в новом проекте. Во многих случаях такой подход позволяет избежать построения новой системы с нуля. Для создания архитектурных моделей могут использоваться различные языки моделирования. В данной работе используется язык анализа и проектирования архитектуры (AADL). Данная статья описывает алгоритм извлечения архитектурной информации из исходного кода ARINC 653 совместимых программных приложений. Спецификация ARINC 653 определяет требования к программным компонентам для систем интегрированной модульной авионики (ИМА). Для доступа к различным сервисам операционной системы программные приложения используют прикладной исполняемый интерфейс. Архитектурная информация в исходном коде программных приложений совместимых с требованиями спецификации ARINC 653 включает процессы в каждом разделе, объекты для взаимодействия между процессами внутри и за пределами раздела, а также глобальные переменные. Для анализа исходного кода и получения архитектурной информации необходимо проанализировать все программные вызовы прикладного исполняемого интерфейса. Извлеченная архитектурная информация далее используется для построения архитектурных моделей системы. Для анализа исходного кода используется подход на основе алгоритма CEGAR (уточнение абстракции с помощью контрпримера), широко используемого при верификации программного обеспечения. Алгоритм CEGAR анализирует возможные пути исполнения программы, используя представление программы в виде абстрактного графа достижимости. В классическом алгоритме CEGAR исследуемый путь программы называется контрпримером и означает путь от начала программы до некоторого ошибочного состояния. Для подтверждения наличия ошибки в коде программы алгоритм CEGAR выполняет проверку достижимости для исследуемого пути. В программном инструменте CPAchecker базовый основанный на предикатах алгоритм CEGAR расширен для анализа явных значений переменных. В данной статье расширенный для анализа явных значений переменных алгоритм CEGAR используется для задачи извлечения архитектурной информации из исходного кода приложений. Основной вклад данной статьи заключается в применении идей контрпримера и проверки достижимости пути к задаче извлечения архитектурной информации из исходного кода приложений.