Классификация частично формализованных и формальных моделей и методов верификации программного обеспечения

Н.А. Бурякова, А.В. Чернов

РГСУ, Ростов-на-Дону

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

В данной статье рассматриваются методы верификации ПО, в основном нацеленные на оценку технического состояния и работоспособности. Такие методы разделяются на группы, которые выделены на рис.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].

Методы статического анализа проводят сравнение некоторого ПО с заранее определенным шаблоном.

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

Динамические методы анализируют уже готовый, работающий продукт и выявляют проблемы с работоспособностью.

Динамические методы верификации применяются для анализа и оценки уже результатов работы ПО, либо некоторых ее прототипов и моделей.

Примерами таких методов являются тестирование ПО или имитационное тестирование, мониторинг и профилирование.

Динамические методы применяются на этапе эксплуатации ПО поэтому необходимо иметь уже работающую систему или хотя бы некоторые ее работающие компоненты. Такие методы нельзя использовать на стадиях разработки и проектирования ПО, зато с их помощью можно контролировать характеристики работы системы в ее реальном окружении, которые иногда невозможно точно определить с помощью других подходов. Динамические методы позволяют обнаруживать в ПО только ошибки, проявляющиеся при его функционировании. Это обстоятельство ограничивает область их применения, например, с их помощью невозможно найти ошибки ПО, связанные с удобством сопровождения программы.

Классификация видов тестирования достаточно сложна, потому что может проводиться по нескольким разным классификационным признакам.

По уровню или масштабу проверяемых элементов системы тестирование делится на следующие виды:

Модульное или компонентное (unit testing, component testing);
Интеграционное (integration testing);
Системное (system testing);
Регрессионное тестирование (regression testing).

По источникам данных, используемых для построения тестов, тестирование относится к одному из следующих видов:

Тестирование черного ящика (black-box testing, часто также называется тестированием соответствия, conformance testing, или функциональным тестированием, functional testing);
Тестирование белого ящика (white-box testing, glass-box testing, также структурное тестирование, structural testing);
Тестирование серого ящика (grey-box testing);
Тестирование, нацеленное на ошибки.

По роли команды, выполняющей тестирование, оно может относиться к следующим видам:

Внутреннее тестирование;
Независимое тестирование;
Аттестационное тестирование (приемочные испытания);
Пользовательское тестирование.

Формальные модели верификации ПО

Методы формального анализа работают с математическими моделями и абстрактными представлениями, интересующего нас ПО.

Формальные методы верификации. Их отличительной особенностью является возможность проведения поиска ошибок на математической модели, без обращения к физической реализации, что в некоторых случаях довольно удобно и экономично. Для проведения анализа формальных моделей применяются специфические техники, такие как дедуктивный анализ (theorem proving), проверка моделей (model checking), абстрактная интерпретация (abstract interpretation). К сожалению, для построения таких моделей всегда необходимо исходить так же из корректности и адекватности модели ПО. Лишь после правильного построения этой модели можно автоматически проанализировать некоторые из ее свойств. Тем не менее, в большинстве случаев для эффективного анализа от специалистов потребуются глубокие знания математической логики и алгебры и некоторого набора навыков работы с этим аппаратом.

Понятия логических и алгебраических исчислений довольно близки. Но для некоторой ясности и определенности можно сказать, что логика применима к утверждениям, записанным на каком либо языке, а алгебра работает с равенствами и неравенствами, записанными на языке выражений.

На нынешнее время логические исчисления могут быть классифицированы следующим образом:

Исчисление высказываний (пропозициональное исчисление, propositional calculus);
Исчисление предикатов (predicate calculus);
Исчисления предикатов более высоких порядков (higher-order calculi);
l-исчисление (lambda calculus);
Модальные логики;
Специальным случаем модальных логик являются временные логики (temporal logics);
Логика дерева вычислений (Computation Tree Logic, CTL*);
m-исчисление (или исчисление неподвижных точек);
Логики явного времени (timed temporal logics).

Другим направлением построения моделей верификации являются алгебраические модели:

Реляционные алгебры;
1. Алгебраические модели абстрактных типов данных;
2. Алгебры процессов (исчисления процессов, process calculi).

В последнее время, привлекают внимание исследователей и другие изучаемые модели:

1. Исполнимые модели (или операционные, executable models) это модели, реализуя которые изучаются свойства моделируемого ПО. Каждая исполнимая модель является, по сути, программой для некоторой виртуальной машины.

Примерами исполнимых моделей являются:

Конечный автомат (finite state machine, FSM);
Конечные системы помеченных переходов (или просто системы переходов, labeled transition systems, LTS);
Расширенные конечные автоматы (extended finite state machines, EFSM);
Взаимодействующие автоматы (communicating finite state machines, CFSM);
Иерархические автоматы (hierarchical state machines);
Временные автоматы (timed automata) [2];
Гибридные автоматы (hybrid automata);
Сети Петри (Petri nets);
Обычный конечный автомат, его принято называть -автоматом;
Машины абстрактных состояний (abstract state machines).

2. Модели промежуточного типа имеют черты как одних - логико-алгебраических, так и других - исполнимых. Стоит отметить, что часть перечисленных выше примеров может быть отнесена к обоим этим классам. Есть, однако, виды моделей, в которых логико-алгебраические и исполнимые элементы сочетаются более глубоко. Основные их виды следующие:

Логики Хоара (Hoare logics);
Динамические или программные логики (dynamic logics, program logics);
Программные контракты (software contracts).

Чаще всего для проверки этих моделей используются методы дедуктивного анализа (theorem proving), проверки моделей (model checking) [1], согласованности, (conformance).

Синтетические методы .Синтетические методы верификации сочетают техники нескольких типов - статический анализ, формальный анализ свойств ПО, тестирование. К таким методам относятся:

Тестирование на основе моделей (model based testing);
Мониторинг формальных свойств ПО (для этой области используется два английских термина — runtime verification и passive testing);
Метод статического анализа формальных свойств;
Синтетические методы генерации структурных тестов.

Представленная в статье классификация частично формализованных и формальных методов верификации отражает современное состояние исследований в данной области.

Литература

Кларк Э.М., Гамбург О., Пелед Д. Верификация моделей программ: Model Checking. // Пер. с англ./ Под ред. Р. Смелянского. - М.: МЦНМО, 2002. – 416 с.
Vardi M.Y., Wolper P. An automata-theoretic approach to automatic program verification. // In LICS86 Journal of the ACM. - Vol. 20, №1. - P.332-334.
Kazman R., Bass L., Abowd G., Webb M. SAAM: A Method for Analyzing the Properties of Software Architectures. // Proc. Of 16-th International Conference on Software Engineering. -1994 – P. 81-90.
Kazman R., Barbacci M., Klein M., Carriere S. J., Woods S.G. Experience with Performing Architecture Tradeoff Analysis. // Proc. of International Conference of Software Engineering. - May 1999 – P. 54-63.
Kazman R., Klein M., Barbacci M., Lipson H., Longstaff T., Carriere S. J. The Architecture Tradeoff Analysis Method. // Proc. of 4-th International Conference on Engineering of Complex Computer Systems. - August 1998 – P. 68-78.

Верификация

Verification

кспертиза

review

Статический анализ

Формальные методы

Динамические методы

Синтетические методы

Общая

Специализированная

Техническая

Technical review

Сквозной контроль

Walkthrough

Инспекция

Inspection

Аудит

Audit

Организационная

Management review

Экспертиза удобства использования

Экспертиза защищенности

Анализ свойств архитектуры

Software architecture evaluation

Проверка правил корректности

Поиск дефектов по шаблонам

Дедуктивный анализ

Theorem proving

Проверка моделей

Model checking

Абстрактная интерпретация

Abstract interpritation

Мониторинг

Тестирование

Профилирование

Имитационное тестирование

Тестирование на основе моделей

Model-based testing, model driven testing

Мониторинг формальных свойств

Runtime verification, passive testing

Статический анализ формальных свойств

Синтетический метод структурного тестирования