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

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

Оглавление
Введение

Глава 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. Результаты анализа и выводы по главе
Глава 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. Проверка корректности формализации метаданных ИСМ-
проекта
3.4. Метод преобразования элементов и конструкций языка ИСМ в модель
на языке базовых протоколов
3.4.1. Описание семантики ИСМ в терминах базовых протоколов
3.4.2. Сокращение модели системы, построенной из базовых протоколов
3.5. Метод автоматизированной отладки процесса генерации тестовых сценариев на основе гидов
3.5.1. Автоматическое преобразование тестовых сценариев в последовательность ИСМ-событий
3.5.2. Анализ покрытия иСМ-модели сгенерированными тестовыми сценариями па основе заданного критерия
3.5.3. Отладка процесса генерации тестовых сценариев на основе
гидов
3.6. Выводы
Глава 4. Реализация методов построения и отладки формальной модели программной системы
4.1. Реализация метода преобразования неформальных требований в формальную модель системы на языке иСМ
4.1.1. Выделение критериальных цепочек из требований
4.1.2. Алгоритм нахождения критических точек параллельных потоков
4.2. Выполнение метода проверки ограничений на элементы и конструкции языка ИСМ
4.2.1. Структура статического анализатора ИСМ-модели
4.2.2. Признаки некорректных многопоточных конструкций
4.3. Реализация метода преобразования элементов и конструкций языка ИСМ в модель на языке базовых протоколов
4.3.1. Архитектура преобразователя ИСМ2РМ
4.3.2. Преобразование конструкций моделирующих параллельное исполнение
4.3.3. Преобразование конструкций моделирующих временные свойства
4.3.4. Преобразование конструкций моделирующих прерывания
4.4. Реализация метода автоматизированной отладки процесса генерации тестовых сценариев на основе гидов
4.4.1. Автоматическое преобразование тестовых сценариев в последовательность ИСМ событий
4.4.2. Отображение тестовых сценариев на ИСМ-модели
4.4.3. Реализация автоматизированного подхода к отладке сгенерированных на основе гидов тестовых сценариев
4.5 Выводы по главе

Глава 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.3 по второму критерию сравнения, можно сделать вывод, что все инструменты поддерживают автоматическое преобразование элементарных конструкций языка 11СМ, перечисленных в приложении 4.
Третий критерий показывает, что все инструменты, кроме 11СМ2РМ, позволяют автоматически преобразовывать параллельные конструкции языка иСМ. А для преобразования иСМ28БЬ требуется дополнительная ручная работа по разметке исходного иСМ-проекта, поэтому реализованный в нем подход считается полуавтоматическим.
Данные по четвертому критерию сравнения (см. табл. 1.3) указывают на отсутствие автоматического преобразования и поддержки семантики временных конструкций языка 11СМ во всех существующих преобразователях за исключением преобразователя 11СМ2Ре1:пИе18. Такое положение дел основано на том, что в исходном языке ИСМ недостаточно информации для формирования задержек и временных конструкций. Отсутствуют события, связанные с заданием временных ограничений. Для преобразования временных конструкций преобразователь иСМ25ИЬ использует дополнительную маркировку состояний, поэтому он считается не полностью автоматизированным.
Анализ преобразователей по пятому критерию позволил отметить наличие во всех преобразователях модуля проверки иСМ-модели на корректность перед процессом преобразования. Однако при этом выявлено, что практически во всех случаях анализ исходной модели на содержание ограничений по конструкциям осуществляется не в полной мере, вследствие чего модель на целевом языке может быть некорректной. Исключением является преобразователь иСМ2Ре1пКе!8, в котором реализован модуль проверки исходных ИСМ спецификаций на пригодность к преобразованию.
Основываясь на сравнении результатов анализа по шестому критерию, можно сделать вывод, что стандарт ИСМ [82] позволяет создавать семантически некорректные модели. Кроме того, он недостаточно выразителен и требует дополнительной информации для осуществления автоматического