Алгоритмы верификации программного обеспечения — это алгоритмы, позволяющие гарантировать, что верифицируемый объект будет соответствовать требованиям, а также то, что он выполнен без непредусмотренных функций и удовлетворяет проектным спецификациям и стандартам.
Введение
Одной из самых важных проблем при формировании и разработке программного обеспечения (ПО) считается его верификация. Способы верификации программного обеспечения служат, для того чтобы подтвердить факты соответствия конечного программного продукта заявленным требованиям. Целями верификации программного обеспечения заключаются в обнаружении ошибок, уязвимостей, неправильно реализованных свойств и требований.
Проблема формирования новой классификации способов верификации ПО считается достаточно актуальной, поскольку позволяет рассматривать известные на данный момент способы верификации ПО и их программную реализацию, определить их достоинства и недостатки. Классификация и изучение существующих способов предоставляет возможность формирования списка требований и рекомендаций для последующей разработки и изучения синтетической методики верификации ПО, на базе SMT-решателя (satisfiability modulo theories).
Алгоритмы верификации программного обеспечения
Известные методики верификации ПО подразделяются на следующие типы:
- Методы эмпирического типа, то есть, применяющие экспертизу.
- Формальные методы, то есть, применяющие математический аппарат для верификации программного обеспечения.
- Методы динамического типа, то есть, которые проверяют работу программной реализации при помощи непосредственного запуска.
А если рассматривать эту проблему с позиций уровня автоматизации, то можно выделить следующие типы систем верификации ПО:
- Системы с ручным управлением.
- Автоматизированные системы.
- Автоматические системы.
Одной из главных задач верификации ПО считается проверка соответствия реализованного программного кода техническому заданию и выполнения требований к функциональному набору. Экспертиза применяется, для того чтобы проверить документацию и коды программного обеспечения на соответствие нормам и стандартам оформления, принятым в стране, отрасли и компании. Экспертиза делится на общую и специализированную.
Методы формальной верификации предоставляют возможность проведения верификации программного обеспечения, опираясь на математические модели программы без обращения к ее физической реализации. Технология символьного исполнения повсеместно применяется сегодня для тестирования и анализа программных продуктов и дает возможность осуществлять моделирование исполнения программы, при котором набор входных переменных может быть представлен в символьном виде. Символ переменной способен обозначать множество значений входной переменной программы из области ее определения.
Любое символьное исполнение является эквивалентным исполнению программы на совокупности фактических тестовых значений входных переменных, что позволяет сократить мощность множества формируемых тестов. Также может определяться альтернативный набор семантики исполнения программы, то есть, семантика символического исполнения для языка программирования, в котором объекты данных представляются в виде символов. Семантика может задаваться путем расширения основных конструкций языков программирования для работы с символьными значениями.
Наиболее важным этапом верификации ПО считается его проверка на соответствие заявленным качественным параметрам. Самыми важными характеристиками программного обеспечения являются следующие:
- Характеристика корректности, то есть, уровень соответствия программы своему предназначению.
- Характеристика безопасности системы.
- Характеристика устойчивости системы в случае неопределенного поведения окружения, к примеру, это могут быть неправильные входные данные.
- Характеристика эффективности использования ресурсов времени и памяти.
- Возможности системы адаптироваться к незначительным изменениям окружения.
- Характеристика переносимости и совместимости.
Известно большое количество методов верификации ПО, основные из которых приведены на рисунке ниже.
Рисунок 1. Методы верификации ПО. Автор24 — интернет-биржа студенческих работ
В первую очередь следует отметить символьное исполнение, проверка моделей, динамические и статические методы верификации ПО. Эти методики считаются самыми эффективными на текущий момент. Исследование алгоритмов и принципов работы известных методик верификации, может служить базой для реализации синтетического метода верификации на основе SMT-решателей.
Приведем некоторые понятия, которые лежат в основе данной классификации методик:
- Виды метода являются описанием основных видов рассматриваемой методики.
- Уровень автоматизации является уровнем, определяющим, в какой степени могут быть автоматизированы алгоритмы той или иной методики верификации.
- Уровень функциональной пригодности призван определять насколько широкий круг задач способен покрыть метод верификации ПО.
- Точность является характеристикой качества полученных измерений, а также она способна показать на сколько погрешность методики, то есть, оценка отклонения измеренного значения величины от ее истинного значения, устремляется к нулю.
- Типы выявляемых ошибок.
- Эффективность является определителем продуктивности метода.
- Область применимости призвана определить на каком этапе разработки применима та или иная методика верификации ПО, а также она способна определить к каким артефактам ПО может быть применен метод верификации. Артефактом ПО является изучаемый фрагмент кода программы.
- Время исполнения призвано определить время, которое необходимо для осуществления верификации программы.
- Метод достижения результата призван определить методы, и алгоритмы, при помощи которых инструменты анализа осуществляют верификацию ПО.
