Журнал СФУ. Техника и технологии / Методика статического анализа для поиска дефектов естественной семантики программных объектов и ее программная реализация на базе инфраструктуры компилятора LLVM и фронтенда Clang

Полный текст (.pdf)
Номер
Журнал СФУ. Техника и технологии. 2018 11 (7)
Авторы
Викторов, Д.С.; Жидков, Е.Н.; Жидков, Р.Е.
Контактная информация
Викторов, Д.С.: Военная академия воздушно-космической обороны им. Маршала Советского Союза Г.К. Жукова Россия, 170022, Тверь, ул. Жигарева, 50; Жидков, Е.Н.: Военная академия воздушно-космической обороны им. Маршала Советского Союза Г.К. Жукова Россия, 170022, Тверь, ул. Жигарева, 50; Жидков, Р.Е.: Военная академия воздушно-космической обороны им. Маршала Советского Союза Г.К. Жукова Россия, 170022, Тверь, ул. Жигарева, 50
Ключевые слова
автоматизированные системы; программное обеспечение; программный объект; верификация; статический анализ; функциональные дефекты; абстрактное синтаксическое дерево; LLVM; Clang; automated systems; software; program object; verification; static analysis; functional defects; abstract syntax tree; LLVM; Clang
Аннотация

В статье описывается методика статического анализа для поиска функциональных дефектов программ, разработка которой обусловлена необходимостью создания качественного отечественного программного обеспечения автоматизированных систем военного назначения в условиях временных и финансовых ограничений процесса разработки. Использование статического анализа позволит автоматизировать процесс выявления дефектов и упростит их локализацию в рамках мероприятий процесса верификации, при этом приоритетным объектом проверок должно быть специальное программное обеспечение вновь создаваемых автоматизированных систем ввиду своей эксклюзивности, масштабности и логической сложности. Предлагается подход, основанный на контроле выполнения принципа размерной однородности физических уравнений, представленных в программе, для чего идентификаторам программных объектов назначается неизменный признак в виде вектора физической размерности интерпретируемой величины. Совокупность всех векторов образует семантический домен, используемый при проверке соотношений между программными объектами по аналогии с анализом зависимостей при абстрактной интерпретации. Для проверки используется внутреннее представление программы, по которому происходят вычисления производных векторов на основании операций с исходными программными объектами. Программная реализация предлагаемой методики основывается на компиляторе LLVM и фронтенде Clang для трансляции кода на языках C, C++, Objective-C. Получаемое с помощью API Clang абстрактное синтаксическое дерево модифицируется для хранения данных о векторах программных объектов

Страницы
801-810
Статья в архиве электронных ресурсов СФУ
https://elib.sfu-kras.ru/handle/2311/109150

Лицензия Creative Commons Эта работа лицензируется по лицензии Creative Commons Attribution-NonCommercial 4.0 International License (CC BY-NC 4.0).