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

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

архитектурная информация, архитектурные модели, интегрированная модульная авионика (ИМА), алгоритм CEGAR

1. OMG Systems Modeling Language (OMG SysML™) Version 1.5, 2017.

2. [Online]. Режим доступа: http://www.omg.org/spec/SysML/1.5/

3. SAE International standard AS5506C, Architecture Analysis & Design Language (AADL), 2017. [Online]. Режим доступа: http://standards.sae.org/as5506c/

4. Feiler P., Gluch D. Model-Based Engineering with AADL: An Introduction to the SAE Architecture Analysis & Design Language. Addison-Wesley, 2012.

5. ARINC Specification 653P1-4. Avionics Application Software Standard Interface Part 1 – Required Services. Published by SAE-ITC, Maryland, USA. August 21, 2015.

6. [Online]. Режим доступа: https://cpachecker.sosy-lab.org/

7. D. Beyer, T. A. Henzinger and G. Theoduloz. Program Analysis with Dynamic Precision Adjustment. In Proc, of the 2008 23rd IEEE/ACM International Conference on Automated Software Engineering, 2008, pp. 29-38.

8. Beyer D., Löwe S. Explicit-State Software Model Checking Based on CEGAR and Interpolation. Lecture Notes in Computer Science, vol. 7793, pp 146-162