Методы верификации программного обеспечения (ПО) предназначены для подтверждения фактов соответствия свойств ПО заявленным требованиям. Такие методы разнообразны и разнородны, как по своему назначению, так и по способам достижения конечного результата и включают как эмпирические, так и формальные доказательства подтверждения наличия у ПО предопределенных свойств. Понятие о верификации ПО понимается в достаточно широком смысле и на отдельных этапах жизненного цикла ПО формальные математические модели, служащие основой верификации существенно различаются. В процессе верификации ПО может достигаться и еще одна цель, состоящая в поиске некорректно реализованных свойств, невыполненных требований и сопутствующем обнаружении ошибок в ПО. В связи с этим, современные методы верификации ПО могут включать в себя методы тестирования ПО. Методы верификации ПО в целом можно разделить на структурные и функциональные, а также имеющие в своей основе формальную математическую модель, либо зависящие от квалификации лиц, принимающих решение о корректности ПО.
В данной статье рассматриваются методы верификации ПО, в основном нацеленные на оценку технического состояния и работоспособности. Такие методы разделяются на группы, которые выделены на рис.1 следующим образом:
· Экспертиза (1);
· Статический анализ (2);
· Динамические методы (3);
· Формальные методы (4);
· Синтетические методы (5).
Рис.1. Общая схема классификации методов верификации ПО
Частично формализованные методы верификации ПО
Методы первой группы в основном, представляют собой тестирование и экспертный анализ свойств ПО и его соответствие некоторому образцу.
Экспертиза (review, переводится как рецензирование, просмотр, обзор, оценка, анализ). Отличительной особенностью экспертизы при верификации ПО является наличие ряда международных стандартов [ISO 12207, IEEE 1074, ISO 15288, ISO 15504], причем заметим, что в нашей стране стандартов аналогичного назначения пока нет. В целом, при таком подходе к верификации ПО, наблюдается ориентированность на экспертные оценки, которые при рассмотрении различных парадигм программирования изменяются. Таким образом, их нельзя отнести к универсальным и строго формализованным. Кроме того, экспертиза применима только непосредственно к самому ПО, а не к формальным моделям, или результатам работы. В качестве видов экспертиз выделяются организационные экспертизы (management review), технические экспертизы (technical review), сквозной контроль (walkthrough), инспекции (inspection) и аудиты (audit). Различные виды экспертиз применяются к различным свойствам ПО на различных этапах проектирования. Своевременное обнаружение дефектов позволяет снизить до минимума риск некорректной работы ПО в дальнейшем.
Особое место среди экспертиз занимают систематические методы анализа архитектуры ПО. Такие как: SAAM (Software Architecture Analysis Method) [3]; ATAM (Architecture Tradeoff Analysis Method) [4,5].
Методы статического анализа проводят сравнение некоторого ПО с заранее определенным шаблоном.
Статический анализ корректного построения исходного кода или поиск часто встречающихся дефектов по некоторым шаблонам хорошо автоматизирован и практически не нуждается в процедурах принятия решений человеком. Однако, круг ошибок, выявляемых статическим анализом, достаточно узок. Одним из применений шаблонов типичных ошибок является их включение в семантические правила компиляторов языков программирования.
Динамические методы анализируют уже готовый, работающий продукт и выявляют проблемы с работоспособностью.
Динамические методы верификации применяются для анализа и оценки уже результатов работы ПО, либо некоторых ее прототипов и моделей.
Примерами таких методов являются тестирование ПО или имитационное тестирование, мониторинг и профилирование.
Динамические методы применяются на этапе эксплуатации ПО поэтому необходимо иметь уже работающую систему или хотя бы некоторые ее работающие компоненты. Такие методы нельзя использовать на стадиях разработки и проектирования ПО, зато с их помощью можно контролировать характеристики работы системы в ее реальном окружении, которые иногда невозможно точно определить с помощью других подходов. Динамические методы позволяют обнаруживать в ПО только ошибки, проявляющиеся при его функционировании. Это обстоятельство ограничивает область их применения, например, с их помощью невозможно найти ошибки ПО, связанные с удобством сопровождения программы.
Классификация видов тестирования достаточно сложна, потому что может проводиться по нескольким разным классификационным признакам.
По уровню или масштабу проверяемых элементов системы тестирование делится на следующие виды:
1. Модульное или компонентное (unit testing, component testing);
2. Интеграционное (integration testing);
3. Системное (system testing);
4. Регрессионное тестирование(regression testing).
По источникам данных, используемых для построения тестов, тестирование относится к одному из следующих видов:
1. Тестирование черного ящика (black-box testing, часто также называется тестированием соответствия, conformance testing, или функциональным тестированием, functional testing);
2. Тестирование белого ящика (white-box testing, glass-box testing, также структурное тестирование, structural testing);
3. Тестирование серого ящика (grey-box testing);
4. Тестирование, нацеленное на ошибки.
По роли команды, выполняющей тестирование, оно может относиться к следующим видам:
1. Внутреннее тестирование;
2. Независимое тестирование;
3. Аттестационное тестирование (приемочные испытания);
4. Пользовательское тестирование.
Формальные модели верификации ПО
Методы формального анализа работают с математическими моделями и абстрактными представлениями, интересующего нас ПО.
Формальные методы верификации. Их отличительной особенностью является возможность проведения поиска ошибок на математической модели, без обращения к физической реализации, что в некоторых случаях довольно удобно и экономично. Для проведения анализа формальных моделей применяются специфические техники, такие как дедуктивный анализ (theorem proving), проверка моделей (model checking), абстрактная интерпретация (abstract interpretation). К сожалению, для построения таких моделей всегда необходимо исходить так же из корректности и адекватности модели ПО. Лишь после правильного построения этой модели можно автоматически проанализировать некоторые из ее свойств. Тем не менее, в большинстве случаев для эффективного анализа от специалистов потребуются глубокие знания математической логики и алгебры и некоторого набора навыков работы с этим аппаратом.
Понятия логических и алгебраических исчислений довольно близки. Но для некоторой ясности и определенности можно сказать, что логика применима к утверждениям, записанным на каком либо языке, а алгебра работает с равенствами и неравенствами, записанными на языке выражений.
На нынешнее время логические исчисления могут быть классифицированы следующим образом:
1. Исчисление высказываний (пропозициональное исчисление, propositional calculus);
2. Исчисление предикатов (predicate calculus);
3. Исчисления предикатов более высоких порядков(higher-order calculi);
4. l- исчисление (lambda calculus);
5. Модальные логики;
6. Специальным случаем модальных логик являются временные логики (temporal logics);
7. Логика дерева вычислений(Computation Tree Logic, CTL*);
8. m-исчисление (или исчисление неподвижных точек);
9. Логики явного времени (timed temporal logics).
Другим направлением построения моделей верификации являются алгебраические модели:
1.Реляционные алгебры;
2.Алгебраические модели абстрактных типов данных;
3.Алгебры процессов (исчисления процессов, process calculi).
В последнее время, привлекают внимание исследователей и другие изучаемые модели:
1. Исполнимые модели (или операционные, executable models) это модели, реализуя которые изучаются свойства моделируемого ПО. Каждая исполнимая модель является, по сути, программой для некоторой виртуальной машины.
Примерами исполнимых моделей являются:
1. Конечный автомат (finite state machine, FSM);
2. Конечные системы помеченных переходов (или просто системы переходов, labeled transition systems, LTS);
3. Расширенные конечные автоматы (extended finite state machines, EFSM);
4. Взаимодействующие автоматы (communicating finite state machines, CFSM);
5. Иерархические автоматы (hierarchical state machines);
6. Временные автоматы (timed automata) [2];
7. Гибридные автоматы (hybrid automata);
8. Сети Петри (Petri nets);
9. Обычный конечный автомат, его принято называть ω -автоматом;
10. Машины абстрактных состояний (abstract state machines).
2. Модели промежуточного типа имеют черты как одних - логико-алгебраических, так и других - исполнимых. Стоит отметить, что часть перечисленных выше примеров может быть отнесена к обоим этим классам. Есть, однако, виды моделей, в которых логико-алгебраические и исполнимые элементы сочетаются более глубоко. Основные их виды следующие:
1. Логики Хоара (Hoare logics);
2. Динамические или программные логики (dynamic logics, program logics);
3. Программные контракты (software contracts).
Чаще всего для проверки этих моделей используются методы дедуктивного анализа (theorem proving), проверки моделей (model checking) [1], согласованности, (conformance).
Синтетические методы. Синтетические методы верификации сочетают техники нескольких типов - статический анализ, формальный анализ свойств ПО, тестирование. К таким методам относятся:
1. Тестирование на основе моделей (model based testing);
2. Мониторинг формальных свойств ПО (для этой области используется два английских термина — runtime verification и passive testing);
3. Метод статического анализа формальных свойств;
4. Синтетические методы генерации структурных тестов.