Классификация частично формализованных и формальных моделей и методов верификации программного обеспечения - umotnas.ru o_O
Главная
Поиск по ключевым словам:
страница 1
Похожие работы
Название работы Кол-во страниц Размер
Данное пособие предназначено для поддержки двухсеместрового курса... 1 989.37kb.
Разработка методики и моделей управления рисками в проектах разработки... 1 291.63kb.
Курс лекций москва 2006 Цели курса 5 Для кого предназначен этот курс? 25 3011.89kb.
Программный принцип работы компьютера. Программное обеспечение. 1 57.34kb.
Техническое задание на выполнение исследовательского проекта «Разработка... 1 93.18kb.
Система анализа данных коллаборативных платформ CrowDM 1 99.21kb.
Минимизация ошибок и сбоев программного обеспечения 1 62.06kb.
Традиционные процессы разработки по. Стадии разработки по. Водопадный... 1 82.28kb.
В точностную теорию надежности программного обеспечения 1 135.47kb.
Моделирование оценки длительности разработки программного обеспечения 1 95.3kb.
Проектирование Информационных Систем Лектор: Пальмов В. С. V курс. 4 506.3kb.
А. Н. Мешков реализация программного комплекса, моделирующего многопроцессорные... 1 130.37kb.
Викторина для любознательных: «Занимательная биология» 1 9.92kb.

Классификация частично формализованных и формальных моделей и методов верификации - страница №1/1

Классификация частично формализованных и формальных моделей и методов верификации программного обеспечения
Н.А. Бурякова, А.В. Чернов

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


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

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



  • Экспертиза (1);

  • Статический анализ (2);

  • Динамические методы (3);

  • Формальные методы (4);

  • Синтетические методы (5).



Рис.1. Общая схема классификации методов верификации ПО


Частично формализованные методы верификации ПО

Методы первой группы в основном, представляют собой тестирование и экспертный анализ свойств ПО и его соответствие некоторому образцу.



Экспертиза (review, переводится как рецензирование, просмотр, обзор, оценка, анализ). Отличительной особенностью экспертизы при верификации ПО является наличие ряда международных стандартов [ISOISIS], причем заметим, что в нашей стране стандартов аналогичного назначения пока нет. В целом, при таком подходе к верификации ПО, наблюдается ориентированность на экспертные оценки, которые при рассмотрении различных парадигм программирования изменяются. Таким образом, их нельзя отнести к универсальным и строго формализованным. Кроме того, экспертиза применима только непосредственно к самому ПО, а не к формальным моделям, или результатам работы. В качестве видов экспертиз выделяются организационные экспертизы (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. -исчисление (lambda calculus);

  5. Модальные логики;

  6. Специальным случаем модальных логик являются временные логики (temporal logics);

  7. Логика дерева вычислений (Computation Tree Logic, CTL*);

  8. -исчисление (или исчисление неподвижных точек);

  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. Синтетические методы генерации структурных тестов.

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


Литература

  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.