Software & Systems

Создание специального ПО для автоматизированных систем военного назначения (АСВН), отвечающего современным требованиям к функциональности, обусловливает необходимость совершенствования мероприятий процесса разработки, в частности, верификации как основного вида работ по контролю качества программного продукта. Нацеленность на улучшение процесса верификации объясняется растущей сложностью специального ПО, что становится причиной наличия в нем все большего количества дефектов. Серьезность сложившейся в программной инже- нерии ситуации подтверждается фактом увеличения доли затрат на выявление и устранение дефектов до 80 % от общей стоимости специального ПО [1, 2].

Нарушение требований к функциональности касается в основном специального ПО, которое разрабатывается эксклюзивно для реализации возможностей вновь создаваемых АСВН, что отличает специальное ПО от унифицированных решений для общего ПО. Данная особенность до минимума сокращает возможность повторного использования уже проверенных фрагментов кода программ и влечет появление новых дефектов. Зачастую необнаруженными после отладки и тестирования остаются функциональные дефекты, которые представляют собой искажения алгоритмов, реализующих информационно-расчетные задачи, что выражается не только в нарушении порядка вычислений (дефекты в условных и циклических конструкциях), но и в ошибочной записи расчетных выражений в операторах программы (подмена истинных значений операций и операндов). АСВН, применяемые для управления боевыми средствами и воинскими формированиями, в функциональной части имеют подсистемы боевого управления, информационную и информационно-расчетную подсистемы. Данные подсистемы включают комплекс информационно-расчетных задач, реализуемых в специальном ПО, общим для которого является оперирование данными, обладающими физическим смыслом. Проверку корректности специального ПО возможно организовать по принципу размерной однородности физических уравнений, используемых в информационно-расчетных задачах. Нарушение данного принципа будем называть дефектами естественной семантики (ДЕС) программных объектов (переменных, функций и т.п.) с целью акцентирования внимания на их различной природе с семантическими дефектами, вызванными нарушением требований спецификации языка программирования.

Существует возможность обнаружения ДЕС при верификации как с помощью экспертиз, предоставляющих качественную субъективную оценку некоторой стороны продукта процесса разработки, так и на основе тестирования, полнота покрытия которого и временные затраты на проведение остаются слабым местом [3]. Статический анализ при определенной доработке также способен выявлять ДЕС, при этом он не подвержен вышеописанным недостаткам и дает воспроизводимое доказательство наличия дефектов. Статический анализ позволяет снизить суммарные трудозатраты на поиск и локализацию дефектов специального ПО за счет значительной автоматизации процедуры его проведения при наличии достаточных вычислительных ресурсов [3, 4]. Подход может применяться уже на ранних этапах фазы разработки специального ПО, так как в качестве входной информации требует исходный код программы. Кроме того, возможность применения статического анализа во время кодирования позволяет сократить стоимость исправления дефектов специального ПО до пяти раз по сравнению с этапом тестирования [1].

Метод верификации специального ПО АСВН на основе статического анализа для поиска ДЕС

Структура метода обусловлена целями, сто- ящими перед процессом верификации согласно нормативным документам, и включает методику статического анализа для поиска ДЕС программных объектов и методику расчета полноты статического анализа для поиска ДЕС программных объектов.

Методика статического анализа основана на работе со значениями семантического домена, состоящего из утверждений о значениях свойств объектов и о зависимостях между ними [5, 6]. Выбранное для проверки принципа размерной однородности свойство объектов программы – размерность физических величин (естественная семантика (ЕС)) формализуется в виде векторов ЕС (ВЕС) и образует линейное пространство. Кроме того, семантический домен содержит зависимости между объектами как отображение множества операций с программными объектами, характерных для языков C/C++, на множество операций с ВЕС. Непосредственно проверка на наличие ДЕС по зависимостям между объектами программы происходит во время обхода внутреннего представления программы в виде абстрактного синтаксического дерева.

Расчет полноты статического анализа для поиска ДЕС программных объектов осуществляется автоматически в процессе анализа по математическим выражениям, полученным путем аналитического моделирования поведения анализатора по поиску дефектов в некоторой элементарной конструкции, что при переходе от частного к общему позволяет делать выводы о полноте статического анализа в целом. Такой подход более предпочтительный по сравнению с преднамеренным внесением искажений в программный код, который требует затрат времени, кратных числу итераций внесения дефектов, тогда как уменьшение числа итераций снижает достоверность оценки полноты [7].

Информационная технология верификации специального ПО АСВН

Информационная технология верификации специального ПО АСВН представляет собой совокупность способов обработки и представления информации о ДЕС с применением вычислительной техники и программных средств об исследуемом специальном ПО на основе исходного кода программы и постановки задач. При этом информационная технология верификации обеспечивает переход от рутинных к промышленным методам и средствам работы с информацией во время выполнения верификации специального ПО, предоставляя возмож- ность для ее рационального и эффективного использования [8].

Целью информационной технологии верификации является инструментальная поддержка процесса верификации специального ПО АСВН на языках C и C++ при поиске нарушений функциональных требований, заключающихся в несоблюдении принципа размерной однородности физических уравнений, реализованных в программе.

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

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

Функциональная модель информационной технологии верификации специального ПО АСВН

Информационная технология верификации специального ПО АСВН представлена в виде функциональной модели IDEF0 [9], формализующей и описывающей работы процесса верификации. Применение методологии функционального моделирования IDEF0 обусловлено популярностью у предприятий промышленности процессного подхода к управлению, где IDEF0 считается классическим инструментом. На рисунке 1 представлена диаграмма А0 функциональной модели.

Работы информационной технологии верификации специального ПО АСВН включают следующие блоки:

-     блок А1; осуществляется формализация требований к ЕС программных объектов, а именно формирование их ВЕС, на выходе – формальная спецификация требований к ЕС программных объектов (O1);

-     блок А2; выполняется статический анализ для поиска ДЕС, на выходе – сообщения о дефектах (O2) и полноте анализа (O3);

-     блок А3; происходит интерпретация результатов статического анализа для поиска ДЕС программных объектов, на выходе – отчет о результатах статического анализа для поиска ДЕС программных объектов (O4).

Входные данные представляют собой документацию (I1) и исходный код программы (I2). Документация должна включать постановку задач, анализ которых позволит выделить и систематизировать требования к ЕС, интерпретируемой в объектах программы. Код програм- мы должен быть представлен на исходном языке высокого уровня C, C++, Objective-C, Objective-C++ в машинно-читаемой форме, пригодной для ввода в статический анализатор.

В качестве управления выступают требования и планы в рамках верификации специального ПО, которые определяют условия, необходимые процессу для производства правильного выхода: требования к формированию уникальных идентификаторов программных объектов (M1), требования к формированию ВЕС программных объектов (M2), план верификации (M3). План верификации специального ПО устанавливает временные зависимости и ограничения при выполнении работ и может быть оформлен как диаграмма Ганта.

Уникальные идентификаторы програм- мных объектов должны включать не только имя конкретного объекта, но и имена его семантических родителей вплоть до имени файла с исходным кодом, что позволяет однозначно определить его для конкретной программы. Вариантом разрешенной таким образом не- однозначности могут быть объявление в рамках главной функции программы переменной и объявление поля с таким же именем в клас- се. Пример уникального идентификатора: speed | missile | function.cpp – поле speed (скорость) объявлено в классе missile (ракета) и размещено в файле function.cpp.

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

,

где ei – элемент на i-й позиции в ВЕС; L – длина; M – масса; T – время; I – электрический ток; Θ – термодинамическая температура; N – количество вещества; J – сила света; a – плоский угол; Ω – телесный угол.

В роли механизмов выполнения работ выступают специалист по верификации (R1) и программные утилиты для верификации, позволяющие автоматизировать подготовку исходных данных для анализа (R2) и процесс его выполнения (R3). Данные программные утилиты предназначены для формирования уникальных идентификаторов программных объектов в рамках формализации требований и для выполнения поиска ДЕС при статическом анализе.

Процесс формализации требований к ЕС программных объектов детализируется на диаграмме A1 функциональной модели и иллюстрируется рисунком 2. Целью работ является подготовка исходных данных для статического анализа в виде списка пар «Уникальный идентификатор программного объекта – ВЕС». Работа складывается из формирования уникальных идентификаторов программных объектов и установки им соответствующих ВЕС.

Работы процесса А11: специалист по верификации специального ПО в соответствии с планом работ с помощью специальной программной утилиты в автоматическом режиме обрабатывает исходный код программы.

Входы: исходный код программы (I2).

Выходы: уникальные идентификаторы программных объектов (O5).

Управление: требования к формированию уникальных идентификаторов программных объектов (M1), план верификации (M3).

Механизмы: специалист по верификации (R1), программная утилита для формирования уникальных идентификаторов программных объектов на базе инфраструктуры LLVM и фронтенда Clang (R2).

Работы процесса А12: специалист по верификации, руководствуясь планом работ, в ручном режиме преобразует в векторы размерности, характерные для объектов исследуемой программы.

Входы: документация (I1).

Выходы: ВЕС программных объектов (O6).

Управление: требования к формированию ВЕС программных объектов (M2), план верификации специального ПО (M3).

Механизмы: специалист по верификации (R1).

Работы процесса А13: специалист по верификации вручную формирует пары для программных объектов вида «Уникальный идентификатор – ВЕС».

Входы: документация (I1), исходный код программы (I2), уникальные идентификаторы программных объектов (O5) и ВЕС програм- мных объектов (O6).

Выходы: формальная спецификация требований к ЕС программных объектов (O1).

Управление: план верификации специального ПО (M3).

Механизмы: специалист по верификации (R1).

В рамках выполнения статического анализа для поиска ДЕС (А2) специалист по верификации вводит в утилиту NSDdetector программный код исследуемого специального ПО (I2), формальную спецификацию требований к ЕС программных объектов (O1) и начинает процедуру анализа. Программная утилита опционально выводит либо на экран компьютера, либо в текстовый файл результат анализа, который включает сообщения о ДЕС, указывающие на строку в файле исходного кода и позицию в операторе (O2), а также частные (по типам конструкций) и интегральный показатели полноты статического анализа для поиска ДЕС (O3).

Интерпретация результатов подразумевает подготовку отчета о проведении статического анализа для поиска ДЕС (O4), который включается в итоговый отчет о верификации специального ПО. Данные о проведении статиче- ского анализа (рис. 3) содержат название файла с исходным кодом программы, используемый язык программирования, размер программы в строках кода, время проведения анализа, локализацию ДЕС в файле исходного кода и описание корректирующих действий для его устранения; интегральный и частные показатели полноты, вывод о корректности программы с точки зрения наличия ДЕС программных объектов.

Утилиты поддержки информационной технологии верификации специального ПО АСВН

Программные утилиты для верификации, позволяющие автоматизировать поиск ДЕС и расчет полноты статического анализа, разработаны с использованием инфраструктуры для создания промышленных компиляторов LLVM и анализатора Clang.

Поиск ДЕС возможно производить до этапов оптимизации и генерации кода, что при создании утилит позволяет ограничиться фронтендом фреймворка LLVM – Clang. Основным преимуществом Clang является его ориентация на максимальное сохранение информации о ходе процесса компиляции и коде программы, что гарантирует его точное воспроизведение в абстрактное синтаксическое дерево. Фронтенд дает возможность доступа к дереву через ме- ханизм курсоров (узлов), а также удобный инструментарий для его обхода и манипулирования, что делает доступным, кроме сбора статистических данных об исследуемом специальном ПО, вычисление производных значений ВЕС программных объектов и контроль корректности операций с ними. При обнаружении ДЕС в узле абстрактного синтаксического дерева Clang предоставляет способ локализации его в файле исходного кода с точностью до строки и позиции в операторе.

Эффективность мероприятий процесса верификации специального ПО АСВН для поиска ДЕС

В качестве показателя эффективности процесса верификации специального ПО АСВН выбрана интенсивность выявления ДЕС, связывающая полезный эффект – количество обнаруженных ДЕС вариантом содержания процесса верификации и необходимые затраты времени на вариант, каждый из которых представляет собой некоторую совокупность мероприятий для достижения цели верификации: , где Nk – количество дефектов, обнаруживаемых k-м мероприятием; Tk – время выполнения k-го мероприятия. Логично полагать, что, чем выше интенсивность обнаружения, тем эффективнее верификация.

Для выполнения оценки выигрыша в эффективности верификации рассматриваются исходный вариант, представленный тестированием, и предлагаемый как сочетание тестиро- вания и статического анализа для поиска ДЕС. Время на работы по тестированию оценивалось по детальной методике COCOMO II [10]. Время статического анализа получено опытным путем с помощью специально разрабо- танной программной утилиты для поиска ДЕС на основе Clang Analyzer. Время на допоиск тестированием не выявленных статическим анализом дефектов рассчитывалось по COCOMO II исходя из достигнутой полноты статического анализа. Для обоих вариантов при расчете использовались номинальные значения факторов, характеризующих время на верификацию, детальной модели COCOMO II.

Зависимость выигрыша в эффективности процесса верификации от полноты статического анализа для поиска ДЕС для програм- много кода размером порядка тысячи строк кода на C++ показана на рисунке 4.

Заключение

Представленная информационная технология верификации специального ПО АСВН реализует полноценный с точки зрения требований нормативных документов метод поиска и регистрации функциональных дефектов и может использоваться как одно из мероприятий в рамках процесса верификации специального ПО АСВН для раннего выявления ДЕС с большей эффективностью. При этом использование предлагаемой информационной технологии верификации для поиска ДЕС программных объектов позволяет получить выигрыш в эффективности процесса верификации до 20–25 % для большинства практических случаев.

Литература

1.    Лобанова Н.М., Дубровин Д.А. Оценка затрат на качество программного обеспечения // Вестн. ун-та. 2016. Вып. 6. С. 87–91.

2.    Черников Б.В., Поклонов Б.Е. Оценка ка- чества программного обеспечения. М.: ФОРУМ–ИНФРА-М, 2012. 400 с.

3.    Кулямин В.В. Методы верификации программного обеспечения. М.: Изд-во ИСП РАН, 2008. 117 с.

4.    Ицыксон В.М., Моисеев М.Ю., Цесь- ко В.А., Захаров А.В., Ахин М.Х. Алгоритм интервального анализа для обнаружения дефектов в исходном коде программ // Информационно-управляющие системы. 2009. Вып. 2. С. 34–41.

5.    Глухих М.И., Ицыксон В.М., Цесько В.А. Использование зависимостей для повышения точности статического анализа программ // Моделирование и анализ информационных систем. 2011. Вып. 4. С. 68–79.

6.    Несов В.С., Маликов О.Р. Использование информации о линейных зависимостях для обна- ружения уязвимостей в исходном коде программ // Тр. ИСП РАН. 2006. № 9. С. 51–57.

7.    Гуров Д.В., Гуров В.В., Иванов М.А. Использование моделей надежности программного обеспечения для оценки защищенности программного комплекса // Безопасность информационных технологий. 2012. № 1. С. 88–91.

8.    Андреев Г.И., Созинов П.А., Тихоми- ров В.А. Управленческие решения при проектировании радиотехнических систем. М.: Радиотехника, 2018. 560 с.

9.    Бистерфельд О.А. Методология функционального моделирования IDEF0. Рязань: Изд-во Рязан. гос. ун-та им. С.А. Есенина, 2008. 48 с.

10. Липаев В.В. Технико-экономическое обоснование проектов сложных программных средств. М.: СИНТЕГ, 2004. 284 с.

References

1. Lobanova N.M., Dubrovin D.A. Software quality cost assessment. University Herald. 2016, no. 6, pp. 87–91 (in Russ.).
2. Chernikov B.V., Poklonov B.E. Software Quality Assessment. Moscow, “FORUM” INFRA-M Publ., 2012, 400 p.
3. Kulyamin V.V. Methods of Software Verification. Moscow, ISP RAN Publ., 2008, 117 p.
4. Itsykson V.M., Moiseev M.Yu., Tsesko V.A., Zakharov A.V., Akhin M.Kh. Interval analysis algorithm for detecting defects in a software source code. Information Control Systems. 2009, no. 2, pp. 34–41 (in Russ.).
5. Glukhikh M.I., Itsykson V.M., Tsesko V.A. The use of dependencies for improving the precision of program static analysis. Modeling and Analysis of Information Systems. 2011, no. 4, pp. 68–79 (in Russ.).
6. Nesov V.S., Malikov O.R. The use of linear dependency information to detect vulnerabilities in program source code. Proc. ISP RAS. 2006, no. 9, pp. 51–57 (in Russ.).
7. Gurov D.V., Gurov V.V., Ivanov M.A.  Use of software reliability models to assess software package security. IT Security. 2012, no. 1, pp. 88–91 (in Russ.).
8. Andreev G.I., Sozinov P.A., Tikhomirov V.A. Management Disisions in the Design of Radio Systems. Moscow, Radiotekhnika Publ., 2018, 560 p.
9. Bisterfeld O.A. IDEF0 Functional Modeling Methodology. Ryazan, Ryaz. gos. un-t im. Esenina Publ., 2008, 48 p.
10. Lipaev V.V. Feasibility Study of Complex Software Projects. Moscow, SINTEG Publ., 2004, 284 p.