Методы генерации тестовых сценариев на основе структурированных UCM-моделей проектируемой системы тема диссертации и автореферата по ВАК РФ 05.13.11, кандидат технических наук Воинов, Никита Владимирович

• Воинов, Никита Владимирович
• кандидат технических наук
• 2011

Оглавление диссертации кандидат технических наук Воинов, Никита Владимирович

Введение.

Глава 1. Обзор методов и средств тестирования на основе моделей.

1.1 Подходы к тестированию в промышленных программных проектах.

1.1.1 Подходы к повышению качества ПО.

1.1.2 Виды тестирования.

1.1.3 Обзор инструментов тестирования.

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

1.2.1 Особенности подхода к тестированию на основе моделей.

1.2.2 Методы создания тестовых сценариев на основе моделей.

1.2.3 Преимущества и ограничения тестирования на основе моделей.

1.3 Сравнительный обзор инструментов тестирования на основе моделей.

1.3.1 Покрытие определенных элементов дерева поведения модели.

1.3.2 Покрытие входных значений переменных.

1.3.3 Отслеживание покрытия требований.

1.3.4 Поддержка работы с моделью и тестирования.

1.3.5 Автоматическое создание окружения тестирования.

1.3.6 Результаты сравнения инструментов тестирования на основе моделей.

1.4 Выводы.

Глава 2. Концепция методов генерации тестовых сценариев и их интеграция в технологии VRS/TAT.

2.1 Технологическая цепочка VRS/TAT и схема интеграции методов генерации тестовых сценариев.

2.2 Формальные модели в нотациях UCM и базовых протоколов.

2.2.1 Применение двух формальных нотаций в рамках одной технологии.

2.2.2 Основы нотации UCM.

2.2.3 Нотация базовых протоколов.

2.2.4 Преобразование компонентов и элементов UCM в базовые протоколы.

2.3 Метод структурирования пространства поведения формальной модели.

2.3.1 Генерация трасс.

2.3.2 Метод расширенных протоколов.

2.3.3 Факторизация поведения UCM-модели с помощью элемента Stub.

2.3.4 Интерпретация элемента Stub в виде расширенного протокола.

2.3.5 Подключение расширенного протокола к общему сценарию поведения системы с помощью протоколов-коннекторов.

2.3.6 Факторизация пространства поведения модели базовых протоколов.

2.4 Оценка сложности пространства поведения формальной модели и метод его сокращения для генерации тестовых сценариев.

2.4.1 Описания поведения системы, представленной в виде базовых протоколов.

2.4.2 Комбинаторный взрыв числа состояний.

2.4.3 Метод эвристик.

2.5 Формулировка критерия покрытия функциональных требований.

2.5.1 Измеряемость требований.

2.5.2 Структурный критерий покрытия требований.

2.6 Выводы.

Глава 3. Реализация методов генерации набора тестовых сценариев по структурированным формальным моделям.

3.1 Реализация методов создания и структурирования формальной модели.

3.1.1 Инструмент UCM2BP.

3.1.2 Режим UCM2MSC.

3.1.3 Структурирование формальной модели.

3.2 Реализация методов создания эвристик для получения тестовых сценариев.

3.2.1 Метод создания эвристик по набору MSC-диаграмм.

3.2.2 Метод создания эвристик по набору MSC-диаграмм и критериальным цепочкам

3.2.3 Инкрементальный метод создания эвристик.

3.3 Реализация методов оценки критериального покрытия и сокращения тестового набора

3.3.1 Реализация метода отслеживания соответствия между требованиями и элементами модели.

3.3.2 Реализация метода поиска покрытия требований в трассах.

3.3.3 Реализация метода сокращения тестового набора и разметка требований в трассах

3.4 Выводы.

Глава 4. Результаты применения разработанных методов генерации тестовых сценариев.

4.1 Обобщенная схема применения разработанных методов.

4.2 Применение разработанных методов в проекте CDMA.

4.3 Анализ результатов применения разработанных методов.

4.4 Выводы.

Введение диссертации (часть автореферата) на тему «Методы генерации тестовых сценариев на основе структурированных UCM-моделей проектируемой системы»

Актуальность работы. Одной из основных проблем разработчиков программного обеспечения (ПО) является проверка корректности функционирования ПО. Требования, предъявляемые к качеству ПО, становятся все более критичными, поскольку от функционирования автоматизированных систем управления зависит не только эффективность производства, но и жизни людей - особенно в таких областях, как транспорт, телекоммуникации, медицина и т.п. Из практики промышленного производства ПО известно, что проверка качества программного обеспечения начинается с разработки требований к проектируемой системе, продолжается до момента вывода системы из эксплуатации и занимает до 50% времени всего жизненного цикла ПО [32]. Этим определяется повышение требований к полноте и производительности подобных проверок.

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

Рис. 1 Стоимость исправления ошибок в зависимости от стадии проекта

Как показывает рис. 1, гораздо сложнее исправить дефекты, которые найдены при эксплуатации продукта, чем в процессе его создания [33].

Следовательно, предотвращение ошибок в требованиях и обнаружение их на ранних этапах проекта сильно уменьшает объём корректировок продукта и таким образом сокращает общую стоимость разработки ПО. Поэтому возникает целевая установка: концентрироваться на поиске ошибок на самых ранних фазах жизненного цикла ПО, не дожидаясь их обнаружения в процессе тестирования готовой реализации [22]. Отвечая этой установке, в последнее время активно развиваются методы и инструменты тестирования на основе моделей.

Построение тестовых сценариев на основе моделей (model-based testing) использует формальные модели требований и спецификаций. Получаемые в результате тестовые сценарии обычно слабо связаны со специфическими особенностями кода тестируемой системы, но содержат представительный набор ситуаций с точки зрения исходной модели [17]. Несмотря на то, что реализации систем отличаются уровнем абстракции от своих моделей, такой подход позволяет автоматизировать процесс генерации тестов из формальных спецификаций системы и значительно сокращает трудозатраты на тестирование.

Однако создание формального описания систем — весьма трудоемкий процесс. Во-первых, свойственная на ранних стадиях проекта неполнота и изменчивость исходных требований затрудняет построение модели, требует перманентной коррекции формализации, и как следствие, привносит значительные временные затраты в выполнение проекта. Во-вторых, высокий уровень необходимых знаний в области математической логики, предъявляемый исполнителям, является дополнительным ограничивающим фактором, усложняющим внедрение формальных методов в процесс индустриальной разработки ПО. В-третьих, существует проблема крупных размеров современных систем, порождающая комбинаторный взрыв числа состояний модели при её проверке. Состояние проверяемой модели включает большое количество переменных и процессов. Даже если число процессов конечно и переменные могут принимать только конечное число значений, общее число состояний может быть очень большим. Реальные системы обычно используют параллельные процессы, а число состояний моделей параллельной системы растет экспоненциально с числом компонентов [16]. Как создание, так и анализ дерева поведения модели такой системы практически невозможны.

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

Сформулируем требования к подобным нотациям:

• во-первых, они должны предоставлять возможность внедрения методов для сокращения пространства поведения модели путем укрупнения детализации описания поведения, факторизации, композиции состояний;

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

Решением проблемы комбинаторного взрыва числа состояний являются методы выбора из всех возможных путей поведения модели ограниченного набора сценариев поведения, покрывающих требования. Главная сложность данного подхода - реализация поиска нужных сценариев. Упростить процесс позволяют методы структурирования модели, предоставляющие возможность ее пошагового анализа по компонентам и на различных уровнях абстракции.

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

Однако вопрос о том, в каком соотношении находятся показатели тестового покрытия модели и показатели покрытия основных требований к целевой системе, как правило, не рассматривается с точки зрения их семантического соответствия [16].

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

Отметим, что отдельно методы структурирования модели и отслеживания соответствия между требованиями и элементами модели для определения покрытия требований реализованы в различных инструментах тестирования на основе моделей (разделы 1.3.3 и 1.3.4). Однако эти инструменты не поддерживают другие важные функции, например, создание модели или исполнение тестов (разделы 1.3.1-1.3.5). В результате, рассмотренные в этих разделах инструменты не покрывают все этапы процесса проверки качества ПО, начиная от создания модели и заканчивая анализом результатов тестирования. Альтернативный подход - технология УЯБ/ТАТ, покрывающая все этапы процесса проверки качества, изложена в работах [1,2,48,11,12,19,20,29,30,31,69-72,121]. Основным преимуществом данной технологии является интегрирование целого набора методов и инструментов верификации и тестирования, каждый из которых реализует отдельный этап в рамках процесса создания модели, ее верификации, тестирования и анализа результатов тестирования, в единую технологическую цепочку. Такой подход делает УЯБ/ТАТ полностью самодостаточной технологией и избавляет пользователей от необходимости обращения к разработкам других фирм на отдельных этапах проверки качества разрабатываемого ПО. Результаты сравнительного анализа представленных на рынке инструментов тестирования на основе моделей (таблица 1.5 в разделе 1.3.6) свидетельствуют о более широких возможностях, предоставляемых УЯЗ/ТАТ в области проверки качества ПО.

Следует отметить пробелы, существовавшие в данной технологии до выполнения настоящей работы:

• отсутствие возможности отслеживания соответствия семантики между исходными требованиями и элементами создаваемой модели;

• как следствие, сложность определения покрытия требований в полученных тестовых сценариях, созданных по модели;

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

Реализация автором данных методов позволила усовершенствовать технологию УЯЗ/ТАТ и сделала ее применение более удобным и эффективным.

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

Настоящая работа посвящена разработке методов генерации тестовых сценариев на основе высокоуровневых иСМ-моделей проектируемой системы. В качестве базового инструментария в работе используется технология УЯЗ/ТАТ, которая является одним из наиболее перспективных современных инструментов верификации и автоматизации тестирования на основе моделей. Реализованные в работе методы позволили сократить трудоемкость процесса разработки тестовых сценариев путем автоматизации ручных этапов, устранив некоторые недостатки и ограничения в инструментарии УЯЗ/ТАТ и сделав его применение более эффективным.

Цели и задачи диссертационной работы. Целью диссертационной работы является сокращение трудоемкости процесса разработки тестовых сценариев путем применения высокоуровневых иСМ-моделей, контролируемых заказчиком. Сокращение трудоемкости осуществляется автоматизацией следующих этапов: преобразование иСМ-моделей в модели базовых протоколов; структурирование модели базовых протоколов; поиск определенных сценариев поведения модели; отслеживание соответствия между требованиями и элементами модели; поиск покрытия требований полученными тестовыми сценариями. Для достижения цели в работе решены следующие задачи:

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

• разработка методов и инструментов автоматического преобразования высокоуровневой формальной модели в формальную модель в нотации, с которой работают инструменты верификации и автоматизации тестирования (например, УЯ8/ТАТ);

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

• формулировка критериев покрытия тестовыми сценариями набора функциональных требований на систему с возможностью отслеживания соответствия между требованиями и элементами модели;

• разработка методов и инструментальных средств построения тестовых сценариев, удовлетворяющих заданному критерию, на основе анализа формальной модели;

• разработка методов и инструментальных средств сокращения полученного набора тестовых сценариев;

• интеграция разработанных методов в технологическую цепочку УЯЗ/ТАТ;

• применение и проверка работоспособности предложенных методов и инструментальных средств в составе технологической цепочки VRS/TAT в крупных промышленных телекоммуникационных проектах. Предметом исследования являются методы и инструментальные средства тестирования на основе моделей.

Методы исследования. Для решения поставленных в работе задач используются теория инсерционного программирования, аппарат формальных спецификаций. Применяются стандарты языков Use Case Maps (UCM) и Message Sequence Charts (MSC).

Обоснованность и достоверность полученных результатов обеспечивается корректным использованием теории инсерционного программирования; использованием аппарата формальных спецификаций; положительными итогами использования разработанных методов и программных средств в четырех индустриальных проектах с помощью технологии VRS/TAT.

Научные результаты и их новизна.

• Разработан подход к процессу генерации тестовых сценариев на основе двух формальных моделей, новизна которого заключается в одновременном применении следующих нотаций: высокоуровневой нотации UCM, позволяющей контролировать заказчиком описание поведения системы и согласовывать с ним поведенческие сценарии, и нотации базовых протоколов для последующего создания тестовых сценариев по модели базовых протоколов.

• Разработан метод автоматизированной генерации базовых протоколов, новизна которого заключается в трансформации UCM-модели в структурированную модель базовых протоколов. Данный метод позволяет заменить ручное создание базовых протоколов их генерацией по высокоуровневой UCM-модели и анализировать поведение модели по компонентам и на различных уровнях абстракции.

• Разработаны методы создания эвристик, новизна которых заключается в автоматизированном построении цепочек базовых протоколов, направляющих поиск определенных сценариев в дереве поведения модели базовых протоколов, что помогло сократить время получения тестовых сценариев при работе с крупными проектами.

• Впервые применен критерий покрытия требований, новизна которого заключается в выявлении последовательностей наблюдаемых событий одновременно как в терминах исходных требований, так и в терминах соответствующих им элементов формальной модели базовых протоколов.

• Для применения критерия цепочек наблюдаемых событий были разработаны новые методы отслеживания соответствия между требованиями и элементами модели базовых протоколов и оценки покрытия требований набором тестовых сценариев по данному критерию, позволяющие определить качество покрытия до этапа создания исполняемых тестов и их исполнения на целевой платформе. Практическая значимость работы. На базе полученных научных результатов разработан комплекс программных средств, интегрированный в технологию VRS/TAT. Усовершенствованная технология VRS/TAT после интеграции разработанных методов была применена в ряде промышленных телекоммуникационных проектов и доказала свою высокую эффективность для обеспечения проверки качества разрабатываемого ПО, позволив сократить более чем на 60% трудоемкость разработки тестовых сценариев по сравнению с существующим подходом.

Апробация работы. Основные положения и результаты диссертационной работы доложены и обсуждены на международных научных конференциях "The Third Spring Young Researchers' Colloquium on Software Engineering" (Moscow, 2009), Motorola Technology Day (SPb, 2007, 2010), "Технологии Microsoft в теории и практике программирования" (СПб, 2008, 2009, 2010), XXXVI неделя науки СПбГПУ (СПб, 2007), XXXIX неделя науки СПбГПУ (СПб, 2010).

Публикации. Основные положения диссертации изложены в 9 печатных работах, в том числе в двух работах в журналах из перечня ВАК.

Внедрение. Разработанные методы внедрены в компаниях ЗАО "Моторола ЗАО", ООО "ИЦ "Северо-Западная лаборатория" и использованы при разработке учебно-методического комплекса СПбГПУ по курсам "Технология разработки программного обеспечения" и "Индустриальные технологии разработки ПО" на кафедре "Информационные и управляющие системы". Практическое использование представляемых на защиту результатов подтверждено соответствующими актами о внедрении.

Структура и объем работы. Диссертация состоит из введения, четырех глав, заключения, списка литературы и трех приложений. Общий объём диссертации с приложениями - 169 страниц машинописного текста, содержит 62 рисунка, 11 таблиц, список литературы содержит 125 наименований.

Заключение диссертации по теме «Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей», Воинов, Никита Владимирович

Основные результаты, полученные в ходе выполнения работы:

1) Разработан и применен новый подход к процессу генерации тестовых сценариев на базе формализованных моделей, заключающийся в применении двух формальных моделей: одной - в высокоуровневой нотации Use Case диаграмм (UCM - Use Case Maps), используемой для контролируемого заказчиком описания поведения и согласования с ним поведенческих сценариев, другой - в нотации базовых протоколов для последующего создания по ней тестовых сценариев.

2) Разработаны и интегрированы в технологию VRS/TAT методы сокращения трудоемкости процесса получения тестовых сценариев:

• автоматическое построение по UCM-модели структурированной формальной модели в виде базовых протоколов;

• автоматическое создание эвристик;

• отслеживание соответствия между требованиями и элементами модели;

• поиск покрытия требований в соответствии с критерием цепочек наблюдаемых событий;

• сокращение набора тестовых сценариев.

3) Усовершенствованная технология VRS/TAT после интеграции разработанных методов была применена в четырех крупных телекоммуникационных проектах в компаниях ЗАО "Моторола ЗАО" и ООО "ИЦ "Северо-Западная лаборатория" и доказала свою высокую эффективность для обеспечения проверки качества разрабатываемого ПО, обеспечив более чем 60%-ное сокращение трудоемкости разработки тестовых сценариев по сравнению с традиционным подходом без использования моделей.

Общий объем разработанного ПО, реализующего разработанные методы, составил около 600 килобайт на языках Perl и Java. Объем документации на разработанное ПО - более 100 страниц.

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

Заключение

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

1) Проведен сравнительный анализ 11 современных инструментов тестирования на основе моделей, выявлены основные недостатки и преимущества по сравнению с технологией УКЭ/ТАТ.

2) В качестве высокоуровневой формальной нотации выбрана нотация иСМ, изучены ее возможности и проанализированы преимущества перед другими формальными нотациями.

3) Разработан метод и инструменты автоматического преобразования иСМ-модели в формальную нотацию базовых протоколов, с которой работают инструменты верификации и автоматизации тестирования УКД/ТАТ.

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

5) Применен критерий покрытия требований, основанный на выполнении последовательностей наблюдаемых событий, характеризующих требования.

6) Для оценки покрытия требований разработаны методы и инструменты отслеживания соответствия между требованиями и элементами модели и поиска покрытия требований в соответствии со сформулированным критерием.

7) Разработаны методы и инструментальных средства построения тестовых сценариев, удовлетворяющих сформулированному критерию, на основе анализа формальной модели.

8) Разработан метод и инструментальные средства сокращения полученного набора тестовых сценариев.

9) Разработанные методы интегрированы в технологическую цепочку VRS/TAT.

10) Для проверки работоспособности разработанные методы и инструментальные средства в составе технологической цепочки VRS/TAT были применены в четырех крупных промышленных телекоммуникационных проектах.

Список литературы диссертационного исследования кандидат технических наук Воинов, Никита Владимирович, 2011 год

1. Баранов С.Н., Дробинцев П.Д., Летичевский A.A., Котляров В.П. Верификационная технология базовых протоколов для разработки и проектирования программного обеспечения // Программные продукты и системы. 2005. № 1(69). С. 25-28.

2. Бурдонов И.Б., Косачев A.C., Пономаренко В.Н., Шнитман В.З. Обзор подходов к верификации распределенных систем. Препринт Института системного программирования РАН, № 16, 2006. 61 с.

3. Веселов А.О., Котляров В.П. Автоматизация тестирования проектов в области телекоммуникаций // Научно-технические ведомости СПбГПУ. № 4. СПб.: Изд-во Политехнического ун-та, 2010. С. 180-185.

4. Веселов А.О., Иванов A.C., Тютин Б.В., Котляров В.П. Автоматизация тестирования телекоммуникационных приложений // Научно-технические ведомости СПбГПУ. № 3. СПб.: Изд-во Политехнического ун-та, 2009. С. 208212.

5. Воинов Н.В., Веселов А.О., Котляров В.П. Автоматизация тестирования UML проектов // Вычислительные, измерительные и управляющие системы. Сборник научных трудов. СПб.: Изд-во Политехнического ун-та. 2007. - С. 57-65.

6. Воинов Н.В., Котляров В.П. Верификация и автоматизация тестирования UML проектов // Научно-технические ведомости СПбГПУ. № 3. СПб.: Изд-во Политехнического ун-та, 2009. С. 220-225.

7. Воинов Н.В., Котляров В.П. Применение метода эвристик для создания оптимального набора тестовых сценариев // Научно-технические ведомости СПбГПУ. № 4 (103). СПб.: Изд-во Политехнического ун-та. 2010. - С. 169174.

8. Дробинцев П.Д. Интегрированная технология обеспечения качества программных продуктов с помощью верификации и тестирования. Диссерт. на соискание уч. ст. канд. техн. наук. СПб.: СПбГПУ, 2006. 238 с.

9. Карпов Ю.Г. Model Checking. Верификация параллельных и распределенных программных систем. "БХВ-Петербург", 2010. 560 с.

10. Кознов Д.В., Арчак H.A. Апробация технологии тестирования UniTesK // Системное программирование. / Под ред. проф. А.Н.Терехова и Д.Ю.Булычева. СПб : Изд СПбГУ, 2004. С. 335-348.

11. Колчин A.B. Разработка инструментальных средств для проверки формальных моделей асинхронных систем. Диссерт. на соискание уч. ст. канд. физ.-мат. наук. Киев, 2009. 140 с.

12. Кулямин В.В. Методы верификации программного обеспечения // Всероссийский конкурсный отбор обзорно-аналитических статей по приоритетному направлению "Информационно-телекоммуникационные системы". 2008. 117 с.

13. Кулямин В.В., Петренко А.К., Косачев A.C., Бурдонов И.Б. Подход UniTesK к разработке тестов // Программирование. 2003. - №29(6). С. 25-43.

14. Летичевский A.A. Верификация и тестирование интерактивных систем, специфицированных базовыми протоколами. Диссерт. на соискание уч. ст. канд. физ.-мат. наук. Киев, 2005. 138 с.

15. Летичевский A.A., Капитонова Ю.В., Волков В.А., и др. Спецификация систем с помощью базовых протоколов // Кибернетика и Системный Анализ. 2005. №4. С. 3-21.

16. Никифоров И.В., Петров A.B., Юсупов Ю.В. Генерация формальной модели системы по требованиям, заданным в нотации Use Case Map // Научно-технические ведомости СПбГПУ. № 4. СПб.: Изд-во Политехнического ун-та, 2010. С. 191-195.

17. Петренко А.К., Бритвина E.H., Грошев С.Г., Монахов A.A., Петренко О.Л. Тестирование на основе моделей // Открытые системы. 2003. - № 9. http://www.osp.ru/os/2003/09/183388/*

18. Abrial J.-R. The B-Book: Assigning Programs to Meanings. Cambridge University Press, 1996. 813 p.

19. AGEDIS // http://www.agedis.de/

20. Последняя проверка актуальности приведенных ссылок 22.02.2011

21. Ambert F., Bouquet F., Chemin S., Guenaud S., Legeard B., Peureux F., Vacelet N., Utting M. BZ-TT: A tool-set for test generation from Z and B using constraint logic programming. Proc. of FATES'2002 August 2002. P. 105-119.

22. Ammann P., Black P. E. Abstracting formal specifications to generate software tests via model checking. Proc. of 18-th Digital Avionics Systems Conference, IEEE, October 1999 Vol.2. P. 10.A.6-1-10.A.6-10.

23. Artisan Studio // http://www.artisansoftwaretools.com/products/artisan-studio/

24. Boehm B. Software risk management: principles and practices. Software, IEEE, 8(1), 1991. P. 32-41.

25. Booch Gr., Maksimchuk R., Engel M., Young B., Conallen J., Houston K. Object-Oriented Analysis and Design with Applications. Addison-Wesley Professional; 3rd edition, 2007. 720 p.

26. Borland Together // http://www.borland.com/us/products/together/index.html

27. Boyapati C., Khurshid S., Marinov D. Korat: automated testing based on Java predicates. Proc. of International Symposium on Software Testing and Analysis, 2002. P. 123-133.

28. Brinksma E. A theory for the derivation of tests. Proc. of 8-th International Conference on Protocol Specification, Testing and Verification, North Holland, 1988. P. 63-74.

29. Broy M., Jonsson B., Katoen J.-P., Leucker M., Pretschner A. (eds.). Model Based Testing of Reactive Systems. LNCS 3472, Springer, 2005. 659 p.

30. Buhr R. J. A., Casselman R. S. Use Case Maps for Object-Oriented Systems, Prentice Hall, 1995. 302 p.

31. Eclipse // www.eclipse.org/

32. Engel C., Hahnle R. Generating unit tests from formal proofs. Y. Gurevich, B. Meyer, eds. Proc. of TAP 2007. LNCS 4454, Springer-Verlag, 2007. P. 169-188.

33. Enterprise Architect // http://www.sparxsvstems.com.au/

34. Enterprise JavaBeans // http://www.oracle.com/technetwork/topics/eib3Q-092128.html

35. Everette R. Keith. Agile Software Development Processes: A Different Approach to Software Design. 25 p. www.cs.nvu.edu/courses/spring03/V22.0474-001/lectures/agile/AgileDevelopmentDifferentApproach.pdf

36. Farchi E., Hartman A., Pinter S. S. Using a model-based test generator to test for standard conformance. IBM Systems Journal, 41(1), 2002. P. 89-110.

37. Fernandez J.-C., Jard C., Jeron T., Viho C. Using On-the-Fly Verification Techniques for the Generation of Test Suites. Proc. of 8-th International Conference on Computer Aided Verification, LNCS 1102, Springer, 1996. P. 348-359.

38. Futatsugi K., Goguen J. A. Principles of OBJ2. In: 12th ACM Symp. on Principles of Programming Languages. - New Orleans, 1985. P. 52-66.

39. Gargantini A., Heitmeyer C. Using model checking to generate tests from requirements specifications. ACM SIGSOFT Software Engineering Notes, 24(6), November 1999. P. 146-162.

40. GOTCHA-TCBeans // www.haifa.ibm.com/proiects/verification/gtcb/index.html

41. Gotlieb A., Botella B., Rueher M. Automatic test data generation using constraint solving techniques. ACM SIGSOFT Software Engineering Notes, 23(2), 1998. P. 53-62.

42. GraphML // http ://graphml. graphdrawing.org/51 . GraphXML // http://strategoxt.org/Transfon-n/GraphXML

43. Gurevich Y. Evolving Algebras: An Introductory Tutorial. Bulletin of the European Association for Theoretical Computer Science 43:264-284, February 1991.

44. Guttag J., Horning J. Larch: Languages and Tools for Formal Specification. -Heidelberg: Springer-Verlag, 1993. 250 p.

45. HP QuickTest Professional //https://hl0078.wwwl.hp.com/cda/hpms/display/main/hpms content.jsp?zn=bto&cp:= 1-11-127-24A1352 4000 100

46. Hoare C.A.R. Communicating sequential processes, Prentice Hall, London, 1985.260 p.

47. Huima A., Invited Talk: Implementing Conformiq Qtronic. Lecture Notes in Computer Science, 2007, Volume 4581, Testing of Software and Communicating Systems. P. 1-12.

48. IBM Rational SDL Suite http://www-01 .ibm.com/software/awdtools/sdlsuite/

49. IBM Rational Software Architect (RSA) // http://www-01 .ibm.com/software/awdtools/architect/swarchitect/

50. IBM Rational Software Modeler (RSM) // http://www-01 .ibm.com/software/awdtools/modeler/swmodeler/

51. IBM Rhapsody // http://www-01.ibm.com/software/awdtools/rhapsody/

52. ISO TC97/SC21, Estelle—A Formal Description Technique Based on an Extended State Transition Model, 1988. International Standard 9074.

53. ITU-T Recommendation Z.100, CCITT Specification and Description Language (SDL), 03/93.

54. ITU Recommendation Z.120. Message Sequence Charts (MSC), 11/99.

55. JUnit II http://www. junit.org/

56. Kull A. PhD Thesis: Model Based Testing of Reactive Systems, Thesis, Tallinn University of Technology, Faculty of Information Technology, 2009. 101 p.

57. Larman C., Basiii V. Iterative and Incremental Development: A Brief History, Computer, vol. 36, no. 6, June 2003. P. 47-56.

58. Letichevsky A.A., Kapitonova J.V., Volkov V.A., Vyshemirskii V.V., Letichevsky Jr. A.A. Insertion Programming // Cybernetics and Systems Analysis, Volume 39, Issue 1 (January 2003). P. 16-26.

59. Letichevsky A.A., Kapitonova J.V., Volkov V.A., Letichevsky Jr A.A., Baranov S.N., Kotlyarov V.P., Weigert T. System Specification with Basic Protocols // Cybernetics and Systems Analysis, Volume 41, Issue 4 (July 2005). P. 479-493.

60. LoadRunner // http://software-testing.rU/library/vendors/l41 -loadrunner/

61. MDL // http://verifV.stanford.edu/dill/murphi.html

62. MessageMagic // http://www.elvior.ee/messagemagic/general

63. Microsoft Solutions Framework (MSF) // http://www.microsoft.com/rus/msdn/msf/

64. Milner R. Communication and Concurrency. Prentice Hall, 1989. 272 p.80. MOTES // www.elvior.ee

65. Myers G. J. The Art of Software Testing. John Wiley & Sons, 1979. 192 p.

66. NUnit // http://www.nunit.org/

67. Objecteeing // http://www.obiecteering.com/

68. OCL // http://lcm.csa.iisc.ernet.in/soft arch/OCL.htm

69. OMG Unified Modeling Language http://www.omg.Org/spec/UML/2.2/

70. ParTeG // http://parteg.sourceforge.net

71. Paulk M.C., Curtis B., Chrissis M.B., Weber C.V. Capability Maturity Model for Software, version 1.1. // CMU/SEI-93-TR-024, February, 1993. 82 p.

72. Pezze M., Young M. Software Testing and Analysis: Process, Principles and Techniques, Wiley, 2007. 488 p.

73. Pex: Microsoft Research // http://research.microsoft.com/en-us/projects/pex/

74. Poseidon // http://www.gentleware.com/91. QARun //http://supportline.microfocus.com/documentation/ASQ/QARunDocs.aspx/

75. Qtronic // www.conformiq.com

76. RAISE // http://www.iist.unu.edu/raise

77. Rational Robot // http://www-01 .ibm.com/software/awdtools/tester/robot/

78. Rising L, Janoff NS. The scrum software development process for small teams. IEEE Software, 2000;(4):2-8.

79. RUP (Rational Unified Process ) //http://www.augustana.ab.ca/~mohri/courses/2000.winter/csc220/papers/rupbestpra ctices/rup bestpractices.html

80. Sen K., Agha G. CUTE and jCUTE: Concolic unit testing and explicit path model-checking tools. Proc. of Computer Aided Verification, Aug 2006. P. 419-423.

81. Shafique M., Labiche Y. A Systematic Review of Model Based Testing Tool Support. Carleton University, Technical Report, May 2010. 21 p.99. SOATest//http://www.parasoft.com/isp/solutions/soa solution.isp;jsessionid-aaa7EAlvipZLSd? itemld=319

82. Spec Explorer: Microsoft Research // http://research.microsoft.com/specexplorer

83. Spec Explorer: MSDN // http://msdn.microsoft.com/en-us/library/ee62041 l.aspx

84. Spy editor // http://www.altova.com/xml-editor/

85. Telelogic TAU G2 // http://www.telelogic.com/products/tau/tau/index.cfm/

86. Telelogic TTCN Suite // http://www.telelogic.com/products/ttcn/index.cfiTi/

87. TestArchitect // http://www.logigear.com/services/test-automation/turnkey-global-test-automation-with-testarchitect.html/

88. TestOptimal // www.testoptimal.com

89. Test Designer // www.smartesting.com

90. Test RealTime // http://www-01 .ibm.com/software/awdtools/test/realtime/

91. TopCased // http://www.topcased.org/

92. Tretmans J. A Formal Approach to Conformance Testing. PhD thesis, University of Twente, Enschede, The Netherlands, 1992. 282 p.

93. Tretmans J., Belinfante A. Automatic testing with formal methods. Proc. Of 7th European Conference on Software Testing, Analysis and Review, Barcelona, Spain, November 1999. P. 8-10.

94. The Z Notation: a reference manual // http://spivey.oriel.ox.ac.uk/mike/zrm/

95. UniTESK // http://www.unitesk.ru/

96. UPPAAL // http://www.uppaal.com/

97. Uppaal CORA // http://www.es.aau.dk/~behrmann/cora/

98. Use Case Map Navigator http://iucmnav.softwareengineering.ca

99. Utting M., Pretschner A., Legeard B. A Taxonomy of Model-Based Testing. Technical Report, Department of Computer Science, The University of Waikato, New Zealand, 2006. 17 p.

100. Utting M., Legeard B. Practical Model-Based Testing: A Tools Approach. Morgan-Kaufmann, 2007. 456 p.

101. VDM // http ://www.vienna.cc/e/evdm.htm

102. Visser W., Pasareanu C. S., Khurshid S. Test input generation with Java PathFinder. ACM SIGSOFT Software Engineering Notes, 29(4), July 2004. P. 97107.

103. Voinov N., Kotlyarov V. Verification and Testing Automation of UML Projects // Proceedings of the Third Spring Young Researchers' Colloquium on Software Engineering. Vol. 3. Moscow, 2009. P. 41-45.

104. WinRunner // http://www.cbueche.de/WinRunner%20User%20Guide.pdf

105. XMI // http://www.omg.org/spec/XMI125. yED // http://www.vworks.com