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

• Никифоров, Игорь Валерьевич
• кандидат наук
• 2013

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

Оглавление

Введение

Глава 1. Анализ подходов и средств обеспечения качества программного продукта

1.1. Методы повышения качества программного продукта

1.1.1. Формальный подход к проблеме обеспечения качества программного продукта

1.1.2. Тестирование программного продукта на основе формальных моделей

1.1.3. Верификация и её основные задачи

1.2. Способы представления требований и анализ формальных языков спецификаций

1.2.1. Исходные документы, фиксирующие требования к системе

1.2.2. Сравнительный анализ формальных языков

1.2.3. Язык Use Case Map

1.3. Сравнительный анализ технологий и инструментальных средств повышения качества программного продукта

1.3.1. Анализ технологий на основе UCM-спецификаций

1.3.2. Сравнение преобразователей языка UCM

1.4. Выводы

Глава 2. Обзор методов проверки требований в технологии VRS/TAT

2.1. Инсерционное программирование

2.2. Критериальные цепочки, как способ доказательства корректности требования

2.3. Критерии покрытия требований

2.4. Генерация и отбор тестовых сценариев, удовлетворяющих выбранному интегральному критерию покрытия

2.4.1. Тестовые сценарии

2.4.2. Отбор тестовых сценариев в соответствии с критерием покрытия

2.5. Метод направленного поиска

2.6. Результаты анализа и выводы по главе 2

Глава 3. Концепции методов автоматизации построения поведенческой

модели программного продукта на основе UCM-спецификаций

3.1. Схема интеграции методов построения и отладки формальных

моделей в технологию VRS/TAT

3.2. Метод преобразования неформальных требований в формальную модель системы на языке UCM

3.2.1. Особенности выделения последовательности критериальных событий

3.2.2. Особенность моделирования параллельных участков исполнения

3.2.3. Особенность моделирования временных задержек

3.2.4. Особенность моделирования прерываний

3.3. Метод автоматической проверки ограничений на элементы и конструкции языка UCM

3.3.1. Формулировка ограничений на моделирование параллельных . процессов

3.3.2. Проверка корректности формализации метаданных UCM-

проекта

3.4. Метод преобразования элементов и конструкций языка UCM в модель

на языке базовых протоколов

3.4.1. Описание семантики UCM в терминах базовых протоколов

3.4.2. Сокращение модели системы, построенной из базовых протоколов

3.5. Метод автоматизированной отладки процесса генерации тестовых сценариев на основе гидов

3.5.1. Автоматическое преобразование тестовых сценариев в последовательность UCM-событий

3.5.2. Анализ покрытия UCM-модели сгенерированными тестовыми сценариями на основе заданного критерия

3.5.3. Отладка процесса генерации тестовых сценариев на основе

гидов

3.6. Выводы

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

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

4.1.1. Выделение критериальных цепочек из требований

4.1.2. Алгоритм нахождения критических точек параллельных потоков

4.2. Выполнение метода проверки ограничений на элементы и конструкции языка UCM

4.2.1. Структура статического анализатора UCM-модели

4.2.2. Признаки некорректных многопоточных конструкций

4.3. Реализация метода преобразования элементов и конструкций языка UCM в модель на языке базовых протоколов

4.3.1. Архитектура преобразователя UCM2FM

4.3.2. Преобразование конструкций моделирующих параллельное исполнение

4.3.3. Преобразование конструкций моделирующих временные свойства

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

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

4.4.1. Автоматическое преобразование тестовых сценариев в последовательность UCM событий

4.4.2. Отображение тестовых сценариев на UCM-модели

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

4.5 Выводы по главе 4

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

экспериментальных проектах

5.1. Результаты применения метода проверки ограничений на элементы и конструкции языка UCM

5.1.1. Характеристики уточненной UCM-модели для

экспериментальных проектов

5.1.2. Статический анализ метаданных

5.2. Оценка эффективности автоматического преобразования UCM-

модели в модель на языке базовых протоколов

5.2.1. Сравнение ручного и автоматического подходов генерации формальной модели системы

5.2.2. Оценка эффективности уменьшения числа поведений в системе

5.3. Применение метода автоматизированной отладки сгенерированных тестовых сценариев

5.3.1. Применение подхода отладки сгенерированных тестовых сценариев

5.3.2. Результаты применения метода анализа покрытия и автоматизированного поиска расхождения трассы и гида

5.4. Оценка преимущества технологии VRS/TAT при разработке тестовых сценариев

5.5. Выводы

Заключение

Литература

ПРИЛОЖЕНИЯ

Приложение 1

Приложение 2

Приложение 3

Приложение 4

Приложение 5

Приложение 6

Приложение 7

Приложение 8

Приложение 9

Приложение 10

Приложение 11

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

Введение

I-Ia современном этапе развития информационных технологий при создании программного продукта особое значение приобретает разработка требований к проектируемой системе. Требования — это официальный документ, в котором изложены функциональные свойства, характеристики и условия использования объекта. Эти свойства должны быть реализованы в системе или компоненте системы для удовлетворения контракта, стандарта, спецификации или иных документов, оговоренных заказчиком. В данном контексте требования выступают как соглашения между заказчиком и разработчиком о результатах, которые должны быть получены в ходе выполнения работ, и формах их представления. Отсутствие требований или неправильная их формулировка к началу создаиия программного продукта приводит к появлению ошибок, которые требуют в дальнейшем исправлений и существенных материальных затрат [47]. Требования должны быть проверяемыми как для заказчика, так и для разработчика [111].

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

Большинство применяемых в существующей практике подходов к описанию требований, равно как и к описанию высокоуровневого дизайна (например, представление на естественном языке, на языке диаграмм и т. п.) не предполагают использования автоматизированных средств, проверяющих их полноту, корректность и непротиворечивость. Таким образом, основным способом проверки различных свойств спецификаций остаются инспекции [5] и обзоры (от англ. review [111]).

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

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

В соответствии с теорией Б. Боэма [66] существует экспоненциальная зависимость между фазами разработки программного продукта, изображенная на рис. 1.В, и затратами на исправление ошибок. Чем позже будет обнаружена ошибка в программном продукте, тем больше она потребует ресурсов на исправление, что в наибольшей степени проявляется при создании промышленных программных проектов, описываемых сотнями спецификаций.

требований Тестирование Эксплуатация

Этапы жизненного цикла проекта

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

Ошибка в требованиях, обнаруженная на этапе тестирования, может привести к изменению в исходных спецификациях, что в свою очередь может потребовать:

— перепланирования разработки функциональности;

— разработки нового или корректировки существующего дизайна;

— изменения архитектуры программной системы;

— кодирования в соответствии с новыми требованиями;

— тестирования исправленного кода.

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

Актуальность работы и степень ее разработанности. Фундаментальные работы отечественных (Ершов А. П. Лавров С.С., Карпов Ю. Г. и др.) и

зарубежных (Летичевский А. А., Бухр К., Маерс Г., Кларк Э.М., Грамберг О., Пелед Д. и др.) ученых составляют базис теорий тестирования и формальных методов, который необходимо применять и адаптировать к требованиям современной индустрии программного обеспечения. На основе формальных моделей исходных требований можно осуществлять проверку их полноты, непротиворечивости и корректности, что должно быть обеспечено средствами верификации. Используя формальные модели программных приложений, можно создавать множества тестов, удовлетворяющих заданному критерию покрытия, которые в дальнейшем используются в системах тестирования.

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

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

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

— автоматизации поиска и отладки ошибок в формальных моделях;

— автоматизации анализа результатов генерации тестовых сценариев.

Для описания требований на ранних этапах разработки дизайна системы используется язык Use Case Map (UCM) [69]. Его отличительными особенностями являются простота графической нотации и ориентированность на описание поведенческих сценариев систем. Модели на языке UCM интуитивно понятны как разработчику, так и заказчику, что позволяет достичь максимального

согласования модели системы перед этапом тестирования. При этом язык UCM используется на более ранней стадии дизайна, т. е. до использования таких языков, как SDL [80], MSC [81], UML [100].

Технология интегрированной символьной верификации и тестирования VRS/TAT [2, 3, 6] позволяет осуществлять проверку требований на полноту, непротиворечивость и генерировать тестовый набор сценариев для автоматического тестирования. Упомянутая технология является на сегодняшний день реальным инструментарием статического анализа программных систем, предназначенных для применения в промышленности, и доказательства корректности спецификации. Для доказательства корректности модели проектируемой программы и формирования тестовых сценариев инструментальная система VRS/TAT использует формальный язык базовых протоколов [26, 28].

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

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

Для достижения цели в работе решены следующие задачи: — обоснован выбор высокоуровневого языка UCM для описания программной системы на стадии дизайна;

— проведен сравнительный анализ технологий работы с UCM-спецификациями и обоснован выбор технологии VRS/TAT;

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

— предложен метод автоматической проверки ограничений на элементы и конструкции языка UCM, описывающие поток данных в системе и многопоточные конструкции;

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

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

— разработан метод и инструментарий автоматизированной отладки сгенерированных символьных тестовых сценариев и анализа покрытия требований тестовыми сценариями на уровне исходной UCM-модели;

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

— применена и проверена работоспособность предложенных методов и инструментальных средств на промышленных телекоммуникационных проектах.

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

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

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

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

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

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

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

3. Разработан и реализован метод автоматической проверки ограничений на элементы и конструкции языка 11СМ, новизна которого заключается в создании иСМ-моделей, пригодных для автоматического преобразования в модель на языке базовых протоколов и автоматической генерации тестовых сценариев.

4. Разработан и реализован метод преобразования элементов и конструкций языка иСМ в формальную модель на языке базовых протоколов, отражающую поведение и структуру исходных спецификаций. Новизна метода заключается в автоматическом преобразовании иСМ-модели, содержащей параллельные потоки, временные задержки, исключения и прерывания, в модель системы на языке базовых протоколов и создании эффективной технологии генерации тестов на основе высокоуровневых иСМ-спецификаций.

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

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

Теоретическая значимость работы

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

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

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

Практическая значимость работы

На базе полученных научных результатов разработан комплекс программных средств, интегрированный в технологию VRS/TAT [32,33,42]. Усовершенствованная технология VRS/TAT применена в ряде промышленных телекоммуникационных проектов и показала высокую эффективность при проверке качества создаваемого программного обеспечения, позволив сократить трудоемкость разработки тестовых сценариев на 25 % по сравнению с принятым в настоящее время подходом [72].

Степень достоверности и апробация работы. Основные положения и результаты диссертационной работы доложены и обсуждены на региональных и международных научных конференциях. А именно: «Summer Young Researchers' Colloquium on Software Engineering» (Perm, 2012), «Third Spring Young Researchers' Colloquium on Software Engineering» (Kazan, 2013), «Program Semantics, Specification and Verification» (SPb, 2012, 2013), «Технологии Microsoft в теории и практике программирования» (СПб, 2009, 2010, 2011, 2012, 2013), XXXVIII неделя науки СПбГПУ (СПб, 2009), XXXIX неделя науки СПбГПУ

(СПб, 2010), XL неделя науки СПбГПУ (СПб, 2011), XLI неделя науки СПбГПУ (СПб, 2012), XLII неделя науки СПбГПУ (СПб, 2013).

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

Внедрение. Разработанные методы внедрены в компаниях ЗАО «Моторола Солюшнз», ООО «ЛЭПКОС» и использованы при разработке учебно-методического комплекса Санкт-Петербургского государственного политехнического университета (СПбГПУ) по учебным дисциплинам «Технология разработки программного обеспечения» и «Технология разработки промышленных приложений на базе IDE Eclipse» на кафедре «Информационные и управляющие системы» СПбГПУ. Практическое использование представляемых на защиту результатов подтверждено соответствующими актами о внедрении.

Положения, выносимые на защиту

1. Четыре метода сформулированные в работе:

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

— метод автоматической проверки ограничений на элементы и конструкции языка UCM;

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

— метод автоматизированной отладки процесса генерации тестовых сценариев на основе гидов.

2.Алгоритмическая и программная реализация разработанных методов.

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

Структура и объем работы. Диссертация состоит из введения, пяти глав, заключения, списка литературы и 11 приложений. Общий объём диссертации -149 страниц, объем приложений 56 страниц; диссертация содержит 108 рисунков, 19 таблиц, список литературы включает 123 издания.

Глава 1. Анализ подходов и средств обеспечения качества программного продукта

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

1.1. Методы повышения качества программного продукта

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

В связи с жёсткой конкуренцией на рынке информационных технологий любая компания стремится создать качественный программный продукт. Принимая во внимание определение качества программного обеспечения, данное IEEE [111], можно сказать, что целыо любой компании является создание такого программного обеспечения, которое будет максимально удовлетворять своим требованиям и, следовательно, желаниям заказчика.

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

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

Важными процессами для подтверждения желаемого качества системы являются верификация и валидация (V&V — verification and validation). В стандарте IEEE [111] дано совместное определение этих двух процессов: «Верификация и валидация — это процесс установления, являются ли требования для системы или ее компонента полными и корректными, удовлетворяют ли продукты каждой стадии разработки требованиям или условиям, выдвинутыми для них на предыдущих стадиях, и соответствует ли конечная система или ее компонента специфицированным требованиям».

Следующим немаловажным аспектом повышения качества программного продукта является нахождение ошибок при помощи тестирования. Тестирование — это процесс функционирования системы или компоненты в заранее определенных условиях, записи и анализа результатов функционирования и оценки свойств системы или компоненты (стандарт IEEE) [111]. Существует множество различных определений тестирования, но существенным является факт, что лишь тщательное тестирование в соответствии с приемочным критерием снижает как вероятность фатального сбоя в процессе эксплуатации, так и количество оставшихся в программе мелких погрешностей. На проведение тестирования при создании сложных программных продуктов требуется до 30...40% общих затрат на разработку программного продукта, и от эффективности его выполнения в значительной степени зависят трудоемкость и сроки создания программ [24].

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

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

1.1.1. Формальный подход к проблеме обеспечения качества программного продукта

Задача тестирования состоит в создании набора тестов, достаточных для проверки качества программного обеспечения в соответствии с выбранным критерием при прогоне тестов на тестируемой системе. Поскольку набор тестов конечен и ресурсы, выделяемые на тестирование, ограничены проектными сроками, то в процессе тестирования для гарантии качества используется экспертиза специалиста. Однако подобная гарантия грешит субъективизмом. Поэтому всё большее распространение для обеспечения качества программного продукта находит формальный подход. Формальный подход позволяет создавать описания действий и данных в некоторой формальной нотации, то есть нотации со строго определённым синтаксисом и семантикой, и использовать формальные методы для интерпретации формальных задач. Формальные нотации (языки) обеспечивают строгость описания, при которой не допускается двусмысленность трактовки созданной спецификации.

Термин «формальные методы» подразумевает ряд операций, в состав которых входят: создание формальной спецификации системы, анализ и доказательство корректности спецификаций, реализация системы на основе преобразования формальной спецификации в программы и верификация программ. Формальная спецификация — это системная спецификация, записанная на языке, словарь, синтаксис и семантика которого определены в соответствии с определенными правилами проектирования, без проникновения в сущность, в существо дела. Необходимость формального определения языка предполагает, что этот язык основывается на математических концепциях. Здесь

часто используется дискретная математика, которая основывается на алгебре, теории множеств и алгебре логики [108].

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

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

— преобразования неформальных требований на программную систему в формальные модели;

— верификации требований в виде формальной модели и генерации тестовых сценариев.

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

Имея формализованные требования на систему или компонент, разработчик может преобразовать их в модель (прототип системы) на формальном языке и проверить ее свойства. Нужно отметить, что всё это происходит еще на фазе проектирования, т. е. до начала фазы разработки кода, что приводит к существенному снижению затрат на исправление ошибок [65], несмотря на дополнительный этап разработки.

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

1.1.2. Тестирование программного продукта на основе формальных моделей

В настоящее время широко исследуется и используется в промышленных масштабах тестирование на основе моделей. Создание любой системы начинается с построения модели и изучения ее свойств. Модель системы сочетает в себе как структуру данных, так и поведение. Заметим, что модели структуры часто называют архитектурными, а поведенческие модели — функциональными.

Модель — формализованное описание структуры и поведения системы [111]. Модель может описываться в терминах состояния системы, входных воздействий на нее, конечных состояний, потоков данных и потоков управления, возвращаемых системой результатов и т. д. Для отражения разных аспектов системы применяются и различные нотации. Формальная спецификация представляет собой законченное описание модели системы и требований к ее поведению в терминах того или иного формального метода. Для описания характеристик системы можно использовать несколько моделей в рамках нескольких формализмов.

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

— тесты на основе спецификации функциональных требований более эффективны, так как они в большей степени нацелены на проверку функциональности, чем тесты, построенные только на знании реализации;

— на основе формальных спецификаций создаются самопроверяющиеся (self-checking) тесты, так как из формальных спецификаций часто извлекаются критерии проверки результатов целевой системы.

1.1.3. Верификация и её основные задачи

Верификация системы [111] в самом общем смысле — это проверка соответствия между требованиями к системе и свойствами реализованной системы. Существует три возможных подхода к верификации системы:

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

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

Список литературы диссертационного исследования кандидат наук Никифоров, Игорь Валерьевич, 2013 год

Литература

1.Ануреев И. С., Баранов С. Н., Белоглазов Д.М., Бодин Е.В., Дробинцев П.Д., Колчин A.B., Котляров В.П., Летичевский A.A., Летичевский A.A. мл., Непомнящий В.А., Никифоров И.В., Потиенко C.B., Прийма Л.В., Тютин Б.В. Средства поддержки интегрированной технологии для анализа и верификации спецификаций телекоммуникационных приложений // Труды СПИИРАН, 2013, № 3(26). - С. 349-384.

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

3. Баранов С.Н., Котляров В.П., Летичевский A.A. Индустриальная технология автоматизации тестирования мобильных устройств на основе верификационных поведенческих моделей проектных спецификаций требований // Космос, астрономия и программирование. Лавровские чтения. СПб.: СПбГУ, 2008. С. 134-145.

4. Баранов С.Н., Котляров В.П. Формальная модель требований, используемая в процессе генерации кода приложения и кода тестов // Моделирование и анализ информационных систем, 2011, том 18, №4, С.118-130.

5. Боэм Б. Инженерное проектирование программного обеспечения: Пер. с англ. - М.: Мир, 1985.

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

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

8. Визовитин Н.В., Непомнящий В.А., Алгоритмы трансляции UCM-спецификаций в раскрашенные сети Петри // Препринтиг 168. - Институт Систем

Информатики им. А.П. Ершова. - Новосибирск. - 2012. [Электронный ресурс]. Режим доступа: // www.iis.nsk.su/files/preprints/168.pdf

9. Воинов Н.В. Методы генерации тестовых сценариев на основе структурированных UCM-моделей проектируемой системы. Диссерт. на соискание уч. ст. канд. техн. наук. СПб.: СПбГПУ, 2011. 169 с.

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

11. Гсргель В. П.. Высокопроизводительные вычисления для многопроцессорных многоядерных систем. Нижний Новгород: Изд-во Нижегородского университета, 2010. - 544 с.

12. Годлевский А.Б., Инсерционная семантика параллельных процедурных конструктов языка UCM // Управляющие системы и машины, Киев, Академпериодика, №6-2012, с.22-34.

13. Губа A.A., Шушпанов К.И., Инсерционная семантика плоских многопотоковых моделей языка UCM // Управляющие системы и машины, Киев, Академпериодика, №6-2012, с.15-21.

14. Дробинцев П.Д., Котляров В.П., Черноруцкий И.Г. Автоматизация тестирования на основе покрытия пользовательских сценариев. // Научно-технические ведомости СПбГПУ. № 4 (152). СПб.: Изд-во Политехнического унта.-2012.-С. 123-126.

15. Дробинцев П.Д., Никифоров И.В., Котляров В.П. Методика проектирования тестов сложных программных комплексов на основе структурированных UCM моделей // Научно-технические ведомости СПбГПУ. № 3(174). СПб.: Изд-во Политехнического ун-та, -2013. -С. 99-105

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

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

18. Карпов Ю.Г., Теория автоматов. // СПб.: Питер, 2003. - 208 с.

19. Ким Р.И., Дробинцев П.Д., Подход к покрытию тестами модели системы, описанной в нотации UCM // Технологии Microsoft в теории и практике программирования. Материалы межвузовского конкурса-конференции студентов, аспирантов и молодых ученых Северо-Запада. 27 марта 2012 г. СПб.: Изд-во Политехнического ун-та. - 2013. С. 60-61.

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

21. Колчин A.B., Котляров В.П., Дробинцев П.Д., Метод генерации тестовых сценариев в среде инсерционного программирования // Управляющие системы и машины, Киев, Академпериодика, №6-2012, с.43-48.

22. Колчин A.B., Метод направления поиска и генерации тестовых сценариев при верификации формальных моделей асинхронных систем // Проблемы программирования. 2008. Вып.4., С. 5-12.

23. Котляров В.П., Петров A.B., Автоматизация формализации требований программного проекта, 2009.

24. Котляров В.П., Пинаев Д.В. Методы и средства автоматизации тестирования программного проекта. Санкт-Петербург, 1998.

25. Котляров В.П. Критерии покрытия требований в тестовых сценариях, сгенерированных из поведенческих моделей приложений // Научно-технические ведомости СПбГПУ. - 2011. - Т.6.1(138). - С.202-207.

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

27. Летичевский А.Ад., Инсерционное моделирование // Управляющие системы и машины, Киев, Академпериодика, №6-2012, с.3-14.

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

29. Маслаков А.П., Никифоров И.В., Котляров В.П., Методы поиска расхождений гайдов и трасс в анализаторе последовательностей событий // Технологии Microsoft в теории и практике программирования. Материалы межвузовского конкурса-конференции студентов, аспирантов и молодых ученых Северо-Запада. 26 марта 2013 г. СПб.: Изд-во Политехнического ун-та.

30. Мелентьев В.А., Скобочная форма описания графов и ее использование в структурных исследованиях живучих вычислительных систем // Автометрия, 2000. No 4. с. 36-52.

31. Никифоров И.В., Дробинцев П.Д., Котляров В.П., Интегральные критерии проверки требований к программному обеспечению // Научно-технические ведомости СПбГПУ. № 3(174). СПб.: Изд-во Политехнического унта, -2013.-С. 111-118.

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

33. Никифоров И.В., Котляров В.П., Дробинцев П.Д. Ограничения на многопоточные конструкции и временные задержки языка UCM // Научно-технические ведомости СПбГПУ. № 3(174). СПб.: Изд-во Политехнического унта, -2013. -С. 148-153.

34. Никифоров И.В., Петров A.B., Юсупов Ю.В., Котляров В.П., Применение различных методик формализации для построения верификационных моделей систем по UCM-спецификациям // Научно-технические ведомости СПбГПУ. № 3(126). СПб.: Изд-во Политехнического ун-та, -2011. -С. 180-184.

35. Никифоров И.В., Юсупов Ю.В., Использование динамических агентов при построении формальной модели по высокоуровневым UCM спецификациям // Технологии Microsoft в теории и практике программирования. Материалы межвузовского конкурса-конференции студентов, аспирантов и молодых ученых Северо-Запада. 23 марта 2011 г. СПб.: Изд-во Политехнического ун-та. - 2011. -С. 108-109.

36. Никифоров И.В., Юсупов Ю.В., Использование Use Case Map в современной технологической цепочке разработки программного обеспечения // XXXVIII Неделя науки СПбГПУ. Материалы межвузовской научно-технической конференции. 30 ноября - 5 декабря 2009 г. СПб.: Изд-во Политехнического ун-та. - 2009. - С. 92-93.

37. Никифоров И.В., Юсупов Ю.В., Преобразование высокоуровневого дизайна программного продукта в нотации Use Case Map в модель на формальном языке // Технологии Microsoft в теории и практике программирования. Материалы межвузовского конкурса-конференции студентов, аспирантов и молодых ученых Северо-Запада. 16-17 марта 2010 г. СПб.: Изд-во Политехнического ун-та. - 2010. -С. 161-162.

38. Никифоров И.В., Юсупов Ю.В., Автоматизированное уменьшение избыточных поведений при проектировании многопоточных систем // XXXIX Неделя науки СПбГПУ. Материалы межвузовской научно-технической конференции. 6-11 декабря 2010 г. СПб.: Изд-во Политехнического ун-та. - 2010. -С. 100-101.

39. Никифоров И.В., Петров A.B., Котляров В.П., Особенности трансляции исключений и прерываний UCM в базовые протоколы // Технологии Microsoft в теории и практике программирования. Материалы межвузовского конкурса-конференции студентов, аспирантов и молодых ученых Северо-Запада. 27 марта 2012 г. СПб.: Изд-во Политехнического ун-та. - 2012. - С. 69-71.

40. Никифоров И.В., Маслаков А.П., Котляров В.П., Использование метода генерации гайдов по структурированной UCM модели для уменьшения влияния комбинаторного взрыва // Технологии Microsoft в теории и практике программирования. Материалы межвузовского конкурса-конференции студентов, аспирантов и молодых ученых Северо-Запада. 26 марта 2013 г. СПб.: Изд-во Политехнического ун-та. - 2013. - С. 77-78.

41. Никифоров И.В., Маслаков А.П., Котляров В.П., Отладка UCM-проекта при генерации тестовых сценариев // XLI Неделя науки СПбГПУ. Материалы

межвузовской научно-технической конференции. 3-8 декабря 2012 г. СПб.: Изд-во Политехнического ун-та. - 2012. - С. 86-87.

42. Никифоров И.В., Петров A.B., Котляров В.П., Статический метод отладки тестовых сценариев, сгенерированных с помощью эвристик // Научно-технические ведомости СПбГПУ. № 4(152). СПб.: Изд-во Политехнического унта, -2012.-С. 114-119.

43. Никифоров И.В., Васин A.A., Котляров В.П., Анализ зависимостей по данным в UCM проекте // Технологии Microsoft в теории и практике программирования. Материалы межвузовского конкурса-конференции студентов, аспирантов и молодых ученых Северо-Запада. 27 марта 2012 г. СПб.: Изд-во Политехнического ун-та. - 2012. - С. 71-72.

44. Никифоров И.В., Васин A.A., Котляров В.П., Анализ трасс и эвристик, основанный на данных из UCM проекта // Технологии Microsoft в теории и практике программирования. Материалы межвузовского конкурса-конференции студентов, аспирантов и молодых ученых Северо-Запада. 27 марта 2012 г. СПб.: Изд-во Политехнического ун-та. - 2012. - С. 51-52.

45. Никифоров И.В., Васин A.A., Котляров В.П., Анализатор последовательности событий, интерпретируемых элементами UCM // XL Неделя науки СПбГПУ. Материалы межвузовской научно-технической конференции. 5 -10 декабря 2011 г. СПб.: Изд-во Политехнического ун-та. - 2011. - С. 106.

46. Овчинников П.С., Никифоров И.В., Котляров В.П., Генерация тестовых сценариев по высокоуровневым UCM-диаграммам для системы аутентификации пользователя // Технологии Microsoft в теории и практике программирования. Материалы межвузовского конкурса-конференции студентов, аспирантов и молодых ученых Северо-Запада. 26 марта 2013 г. СПб.: Изд-во Политехнического ун-та. - 2013. - С. 78-79.

47. Петренко А.К., Бритвина E.H., Грошев С.Г., Монахов A.A., Петренко O.JI. Тестирование на основе моделей // Открытые системы. - 2003. - № 9. [Электронный ресурс]. Режим доступа: http://www.osp.ru/os/2003/09/183388/

48. Сети Петри, CPN Tools. [Электронный ресурс]. Режим доступа: // http://cpntools.org/

49. Скобелев В.Г., Безопасность IT-систем // РАДЮЕЛЕКТРОНШ I КОМП'ЮТЕРШ СИСТЕМИ, 2013, No 5 (64), Институт прикладной математики НАМ Украины, г.Донецк, С.- 352-361.

50. Тихомиров В.А. Анализ взаимовлияний при интеграции новой функциональности в существующую систему средствами верификации и тестирования. Диссерт. на соискание уч. ст. канд. техн. наук. СПб.: СПбГПУ, 2009. 133 с.

51.Тютин Б.В., Никифоров И.В., Котляров В.П., Построение системы автоматизации статической и динамической проверки требований к программному продукту// Научно-технические ведомости СПбГПУ. № 4(152). СПб.: Изд-во Политехнического ун-та, -2012. -С.

52. Целлер А., Почему не работают программы //Руководство по системной отладке. М., ЭКСМО, 2011. с.70-71.

53. Юсупов Ю.В. Интегрированная методика автоматизированного построения формальных поведенческих моделей С-приложений по исходному коду Диссерт. на соискание уч. ст. канд. техн. наук. СПб.: СПбГПУ, 2009. 176 с.

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

55. AGEDIS. [Электронный ресурс]. Режим доступа: // http://www.agedis.de/

56. Alan Mark Davis, "Just Enough Requirements Management: Where Software Development Meets Marketing" - Addison-Wesley Professional, 2013, 256. -[Электронный ресурс]. Режим доступа: // http://my.safaribooksonline.com/book/software-engineering-and-development/9780133491234

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

58. Amyot D., Specification and Validation of Telecommunication System with Use Case Maps and LOTOS, Ph.D. Thesis, Ottawa, Ontario, Canada, University of Ottawa, September 2001, 128p.

59. Amyot D., "Use Case Maps Quick Tutorial", University of Ottawa, 1999.

60. Baranov S., Kotlyarov V., Letichevsky A., Drobintsev P., Yusupov Yu. Implementation of an Integrated Verification and Testing Technology in Telecommunication Project // IEEE. Russia Northwest Section. International conference "Radio - that connects time. 110 anniversary of radio invention". Proceedings. Volume II. SPb., 2005. P. 87-92.

61. Baranov S., Kapitonova J., Letichevsky A., Kolchin A., Letichevsky A. (Jr)., Radchenko V., Potiyenko S., Volkov V., Tools For Requirements Capturing Based on the Technology of Basic Protocols // Proceedings of St. Petersburg. IEEE Chapters -2005. P. 92-97.

62. Baranov S., V.Kotlyarov, A.Letichevsky, P.Drobintsev. The technology of Automation Verification and Testing in Industrial Projects. / Proc. of St.Petersburg IEEE Chapter, International Conference, May 18-21, St.Petersburg, Russia, 2005 - pp. 81-86

63. Baranov S., Kotlyarov V., Weigert T., Verifiable Coverage Criteria For Automated Testing. SDL2011: Integrating System and Software Modeling // LNCS. -2012. -Vol.7083. -P.79-89.

64. Bergstra J.A., Ponse A., Smolka S.A., (Eds) Handbook of Process Algebra, North-Holland, 2001.

65. Boehm B., "Software Engineering Economics", Englewood Cliffs, N.J., Prentice-Hall, 1981.

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

67. Bordeleau, F., A systematic and traceable progression from scenario models to communicating hierarchical state machines, Thesis (Ph.D.), Carleton University, 2000.

68. Bordeleau, F., Cameron, D., On the relationship between Use Case Maps and Message Sequence Charts, in Proceedings of The 2nd Workshop of the SDL Forum Society on SDL and MSC (SAM2000), Grenoble, France, June 2000.

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

70. Charfi L. PhD Thesis: Formal Modeling and Test Generation Automation with Use Case Maps and LOTOS, Thesis, Ottawa, Ontario, Canada, University of Ottawa, March 2001.

71. Drobintsev P., Nikiforov I., Kotlyarov V., Letichevsky A., "A Formal Approach for Generation of Test Scenarios Based on Guides"// Proceedings of Fourth Workshop "Program Semantics, Specification and Verification : Theory and Applications", Yekaterinburg, Russia, June 24, 2013, pp.31-42.

72. Drobintchev P., Kotlyarov V., Nikiforov I., "Technology Aspects of State Explosion Problem Resolving for Industrial Software Design"// Proceedings of the 7th Spring/Summer Young Researchers' Colloquium on Software Engineering, Kazan, May 30-31, 2013, pp. 46-51.

73. Drobintsev P.D., Nikiforov I.V., Kotlyarov V.P., Semantics adjustment of UCM Real Time Constructions for Implementation in Translator of UCM to Basic Protocols // Humanities and Science University Journal. № 5 (2013): научный журнал / Санкт-Петербургский университетский консорциум. - СПб., 2013. - С. 207-215.

74. GOTCHA-TCBeans. [Электронный ресурс]. Режим доступа: // www.haifa.ibm.com/projects/verification/gtcb/index.html

75. Hassine J., Rilling J„ and Dssouli R., Timed Use Case Maps. In System Analysis and Modeling: Language Proles, 5th International Workshop, SAM 2006, Kaiserslautern, Germany, May 31 - June 2, 2006, Revised Selected Papers, pages 99114, 2006.

76. Hassine J., Formal Semantics and Verification of Use Case Maps, Thesis For the PhD, Concordia University, Montreal, Quebec, Canada, April 2008, p.284.

77. Hoare C.A.R. Communicating sequential processes, Prentice Hall, London, 1985.260 р.

78. Holzmann, G., Design and Validation of Computer Protocols, Prentice Hall, 1991, New Jersey, esp. pp. 217-244.

79. International Organization for Standardization - ISO, Information Processing Systems, Open Systems Interconnection, LOTOS - A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour, IS 8807, Geneva, 1989.

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

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

82. ITU-T Recommendation Z.151 . User requirements notation (URN), 10/2012

83. Jensen K., Kristensen L.M. Coloured Petri Nets: Modelling and Validation of Concurrent Systems. // Springer 2009.

84. jUCMNav. [Электронный ресурс]. Режим доступа: // http://iucmnav.softwareengineering.ca/ucm/bin/view/ProietSEG/WebHome

85. Knightson, К., Osi Protocol Conformance Testing : IS 9646 Explained (McGraw Hill Series on Computer Communications), New York, 1993, McGraw Hill

86. Letichevsky A.A., Kapitonova J.K., Kotlyarov V.P, Volkov V.A., Letichevsky A.A. Jr., Weigert Т. Semantics of Message Sequence Charts // Proc. 12 the International SDL Forum, Grimstad, Norway -2005, -CI 17-132.

87. Letichevsky A., Kapitonova J., Letichevsky Jr., A., Volkov V., Baranov S., Weigert Т. Basic protocols, message sequence charts, and the verification of requirements specifications, Computer Networks: The International Journal of Computer and Telecommunications Networking, v.49 n.5, 5 Dec 2005. P. 661-675.

88. 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.

89. Letichevsky A., Kapitonova J., Letichevsky A. (Jr)., Volkov V., Baranov S., Kotlyarov V., Weigert Т. Basic Protocols, Message Sequence Charts, and the Verification of Requirements Specifications, ISSRE 2004, WITUL (Workshop on Integrated reliability with Telecommunications and UML Languages), Rennes, 4 November. 2005. P. 30-38.

90. Letichevsky A., Gilbert D., A Model for Interaction of Agents and Environments, In D.Bert, C.Choppy, P.Moses (Eds), Resent Trends in Algebraic Development Techniques, LNCS 1827, 311-328,-1999.

91. Leue S., Mehrmann L., Rezai M., Synthesizing ROOM Models from Message Sequence Chart Specifications, University of Waterloo, Technical Report 98-06, 1998

92. Manna Z., Pnueli A.: The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag, 1992

93. Mansurov N., Zhukov D., Automatic synthesis of SDL models in Use Case Methodology, in SDL'99: The Next Millenium, ed. R.Dssouli, G.Bochmann, Y.Lahav, proceedings of the ninth SDL Forum, Montréal, Québec, Canada, 1999, Elsevier Science.

94. Marca D.A., McGowan C.L. SADT Structured Analysis and Design

Technique. McGraw-Hill, 1988. 437 p.

95. mbt. [Электронный ресурс]. Режим доступа: //http://mbt.tigris.org

96. A. Miga, D. Amyot, F. Bordeleau, C. Cameron, M. Woodside. Deriving Message Sequence Charts from Use Case Maps Scenario Specifications. Tenth SDL Forum (SDL'01), Copenhagen, Denmark, June 2001.

97. Milner R., "Communication and Concurrency." - Prentice Hall, 1989.

98. Milne R. The Proof Theory for the RAISE specification language. RAISE Report REM/12, STC Technology Ltd, 1990.

99. MOTES. [Электронный ресурс]. Режим доступа: // www.elvior.ee

100. OMG Unified Modeling Language. [Электронный ресурс]. Режим доступа: // http ://www.omg.org/spec/UML/2.2/

101. ParTeG. [Электронный ресурс]. Режим доступа: // http://parteg.sourceforge.net

102. Promela. [Электронный ресурс]. Режим доступа: // http://spinroot.com/spin/Man/Quick.html

103. Qtronic. [Электронный ресурс]. Режим доступа: // www.conformiq.com

104. Ruoshan G., From Requirements to Scenarios through Specification: A Translation Procedure From Use Case Maps to LOTOS., Thesis, Ottawa, Ontario, Canada, University of Ottawa, 2002, 128p.

105. Sales I., A Bridging Methodology for Internet Protocols Standards Development, Ph.D. Master of Computer Science Thesis, Ottawa, Ontario, Canada, School of Information Technology and Engineering - S.I.T.E., September 30 2001, p.119.

106. Sales, I., Probert, R., From High-Level Behaviour to High-Level Design: Use Case Maps to Specification and Description Language, in proceedings of the 18Brazilian Symposium on Computer Networks, SBRC'2000, pp. 457-471, Belo Horizonte, Minas Gerais, 2000.

107. Selic, B. et al, Real-time Object-Oriented Modelling, New York, 1994, John Wiley and Sons.

108. Sommerville I., "Software Engineering", 6 edition, 2002.

109. Sousa, Rui M. Putnik, Goran D. Moreira, Francisco, Using formal description technique ESTELLE for manufacturing systems specification or description, "International Journal of Production Engineering and Computers". ISSN 1450-5096. 3 (1998) 1-10. [Электронный ресурс]. Режим доступа: // http://repositorium.sdum.uminho.pt/bitstream/1822/5489/l/Belgrado98.pdf

110. Spec Explorer: Microsoft Research. [Электронный ресурс]. Режим доступа: // http://research.microsoft.com/specexplorer

111. Standard Glossary of Software Engineering Terminology, ANSI/IEEE Standard 610.12-1990, IEEE Standard, IEEE, NY (1990).

112. Telelogic TAU G2. [Электронный ресурс]. Режим доступа: // http://www.telelogic.com/products/tau/tau/index.cfm/

113. Telelogic TTCN Suite. [Электронный ресурс]. Режим доступа: // http://www.telelogic.com/products/ttcn/index.cfm/

114. Test Designer. [Электронный ресурс]. Режим доступа: // www.smartesting.com

115. TestOptimal. [Электронный ресурс]. Режим доступа: // www.testoptimal.com

116. Turner, К., Using Formal Description Techniques: An introduction to Estelle, LOTOS, and SDL, New York, John Wiley and Sons, 1993.

117. Turner, K., An engineering approach to formal methods, in Dathine, A., Leduc, G., Wolper, P., editors, proceedings of Protocol Specification, Testing and Verification XIII, Amsterdam, Netherlands, 1993, North Holland Publishers, pp. 357380.

118. Tyutin B.V., Nikiforov I.V., Kotlyarov V. P., "Distributed Testing of Multicomponent Systems", Proceedings of the 6th Spring/Summer Young Researchers' Colloquium on Software Engineering, Perm, May 30-31, 2012, pp. 75-78.

119. UniTESK. [Электронный ресурс]. Режим доступа: // http://www.unitesk.ru/

120. VDM [Электронный ресурс]. Режим доступа: //httpy/www.vienna.cc/e/evdmhtm

121. VDM-SL. [Электронный ресурс]. Режим доступа: // http://www.overturetool.org/?q=Documentation

122. Vizovitin N.V., Nepomniashcy V.A., Stenenko A.A., Verification of UCM-Specifications of Distributed System Using Colored Petri Nets

123. 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.

150