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

• Автор: Дробинцев, Павел Дмитриевич
• Шифр специальности: 05.13.11
• Научная степень: Кандидатская
• Год защиты: 2006
• Место защиты: Санкт-Петербург
• Количество страниц: 238 с. : ил.

Введение.

1. Обзор подходов проверю качества программного обеспечения

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

1.2. Методы и особенности тестирования.

1.2.1. Методы автоматизации тестирования.

1.2.2. Инструментарий тестирования.

1.3. Формальный подход к проблеме обеспечения качества ПО.

1.3.1. Математический аппарат моделей программ.

1.3.2. Обзор моделей программ

1.4. Методы верификации

1.4.1. Нотации описания систем

1.4.2. Дедуктивные методы верификации.
1.4.3. Методы проверки на модели
1.5. Инструментарий верификации
1.5.1. Сравнительный анализ средств верификации.
Выводы
2. Методики интегрированной технологии верификации и тестирования
2.1. Общая схема технологии автоматизированной верификации и тестирования
2.2. Используемые формальные языки
2.3. Основы метода базовых протоколов
2.3.1. Базовые протоколы
2.3.2. Язык базовых протоколов
2.3.3. Базовый протокол в .
2.4. Система верификации V.
2.5. Система автоматизации тестирования ТАТ
2.6. Обзор методик интегрированной технологии верификации и тестирования.
2.6.1. Поиск ошибок в спецификациях.
2.7. Методика формализации требований на основе базовых протоколов МБР.
2.7.1. Создание БИА.
2.7.2. Создание БИС.
2.7.3. Создание БИФ.
2.8. Методика доказательства заданных свойств системы на основе е модели на языке
с последующей генерацией кода .
2.9. Методика генерации тестового набора
2 Методика доказательства детерминированности поведения системы ТСС.
2 Методика проверки аннотированных сценариев поведения системы АС.
2 Методика автоматизации тестирования ТАТ.
Выводы.
3. Программная поддержка технологий автоматизации тестирования и верификации.
3.1. Программная поддержка интеграции подсистем верификации и тестирования
3.2. Модуль генерации кода системы по множеству базовых протоколов
3.2.1. Блок запуска генерации
3.2.2. Блок анализа конфигурации.
3.2.3. Блок генерации
3.3. Подсистема настройки на область тестирования.
3.3.1 Графический пользовательский интерфейс
3.3.2 Генератор интерфейсного модуля
3.4. Характеристика разработанных программных средств.
4. Результаты применения разработанных методов и средств автоматизации тестирования и верификации.
4.1. Состав экспериментального комплекса.
4.2. Применение технологии в телекоммуникационных проектах.
4.3. Применение технологии в проектах связанных с мобильной телефонией.
4.4. Применение технологии в проектах встроенных применений
4.5. Учебные проекты.
4.6. Общая статистика и анализ результатов применения технологии.
4.7. Оценки применения технологии в больших промышленных проектах
Заключение
Литература


Самым простым примером в данном случае является использование формальных языков, при разработке требований и спецификаций в виде, который может быть использован для автоматической проверки созданного или создаваемого ПО. В следующей части работы проведён обзор формальных методов, языков и инструментов для работы с ними. Программное обеспечение часто используется в критичных к ошибкам областях человеческой деятельности. Именно поэтому гарантии качества производимого продукта являются неотъемлемой частью современного процесса производства ПО. В п. ПО средствами тестирования, этапы, подлежащие автоматизации и инструментарий, позволяющий проводить различного рода автоматизацию тестирования. Как было отмечено, задача тестирования состоит в создании входного набора тестов достаточных для проверки качества ПО, в соответствии с выбранным критерием и его прогоне на тестируемом приложении. Поскольку набор тестов конечен и урезается в соответствии с ограничениями проектных сроков, то только экспертиза человека в процессе тестирования позволяет гарантировать качество, но эта гарантия грешит субъективизмом. Поэтому в последнее время всё большее распространение получает формальный подход. Формальный подход - это подход позволяющий создавать описания действий и данных в некоторой формальной нотации, то есть нотации со строго определённым синтаксисом и семантикой, и использовать формальные методы для интерпретации формальных задач. Формальные нотации (языки) обеспечивают, строгость описания, при которой не может быть допущена двусмысленная трактовка созданной спецификации. Формальные методы используют математическую лотку и дискретную математику в процессе разработки ПО. В [ms] приведено следующее определение формальных методов: “Методы спецификации и производства программного обеспечения, основанные на математических системах и включающие в себя: множества математических нотаций для создания спецификаций, описания фаз дизайна и производства ПО, логические системы, предназначенные для верификации, и методологическую среду на основании которой может бьггь проведена формальная верификация”. Если требования и спецификации на Г, заданные в проектных документах, формализовать - то есть описать на формальных языках проектирования, то к таким описаниям могут быть применены формальные методы. В настоящее время существует множество формальных языков для подобного описания. Основной их задачей является описание процесса, данных, структуры и архитектуры программных средств или тестов для облегчения и ускорения процесса создания ПО. Здесь стоит упомянуть такие языки как RSL [Mila], LOTOS [LOTOS], SDL [sdl], UML [uml], MSC [MSC], Estelle [ESTELLE], ML [ml], CASL [cats], SMV [SMV] и множество других. Такое разнообразие связано с тем, что каждый из перечисленных языков создавался для решения задач в определённой области производства ПО. Переход к унифицированному стандарту произошёл в конце -х с появлением языка UML (Unified Modeling Language). UML включает набор различных типов диаграмм, удобных для описания архитектурных решений приложений через протоколы, конечно - автоматные реализации, описывающие структурные и поведенческие характеристики, потоки данных и т. В общем случае формальные описания требований, тестов и программ позволяют добавить в процесс создания ПО два мощных метода - генерацию и верификацию. В работе рассмотрено применение генерации и верификации к процессам проектирования и тестирования ПО. Как указывалось выше, к сложным задачам для тестировщика относится создание набора тестов в соответствии с некоторым критерием. Для решения этой задачи перспективно применение генерации, однако если требования на программу заданы на не формальном языке (например, на естественном языке) применение метода генерации не возможно. Поэтому для генерации перевод требований в некоторую формальную нотацию необходим, он же очень полезен как для разработчика, который будет точно знать и понимать, требования на входе и выходе системы, так и для тестировщика, который получает чёткое представление о поведении тестируемой системы. Когда требования представлены в формальном виде, то применение генерации становится возможным.