×

Вы используете устаревший браузер Internet Explorer. Некоторые функции сайта им не поддерживаются.

Рекомендуем установить один из следующих браузеров: Firefox, Opera или Chrome.

Контактная информация

+7-863-218-40-00 доб.200-80
ivdon3@bk.ru

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

Аннотация

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

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

05.13.18 - Математическое моделирование, численные методы и комплексы программ

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

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

    • Реляционные алгебры;
    • Алгебраические модели абстрактных типов данных;
    • Алгебры процессов (исчисления процессов, 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);
  • Метод статического анализа формальных свойств;
  • Синтетические методы генерации структурных тестов.

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

Литература

1. Кларк Э.М., Гамбург О., Пелед Д. Верификация моделей программ: Model Checking. // Пер. с англ./ Под ред. Р. Смелянского. - М.: МЦНМО, 2002. – 416 с.
2. 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.
3. 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.
4. 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.
5. 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.