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

На правах рукописи

Никифоров Игорь Валерьевич

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

Специальность 05.13.11 — Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей

Автореферат

диссертации на соискание ученой степени кандидата технических наук

17 АПР 2014

005547093

Ганкт-Петербург - 2013

005547093

Работа выполнена в федеральном государственном бюджетном образовательном учреждении высшего профессионального образования «Санкт-Петербургский государственный политехнический университет».

Научный руководитель: КОТЛЯРОВ Всеволод Павлович

кандидат технических наук, доцент

Официальные оппоненты: ТЕРЕХОВ Андрей Николаевич,

доктор физико-математических наук, профессор, заведующий кафедрой системного программирования Математико-механического факультета Санкт-Петербургского государственного университета

ИВАНОВСКИЙ Сергей Алексеевич, кандидат технических наук, доцент, заведующий кафедрой математического обеспечения и применения ЭВМ Санкт-Петербургского государственного электротехнического университета

Ведущая организация: ОАО «Научно-производственное объединение

«Импульс», г. Санкт-Петербург

Защита состоится «15» мая 2014 г. в 1600 часов на заседании диссертационного совета Д. 212.229.18 при ФГБОУ ВПО «Санкт-Петербургский государственный политехнический университет» по адресу: 195251, г. Санкт-Петербург, Политехническая ул., д. 29, уч. корп. 9, ауд. 325.

С диссертацией можно ознакомиться в Фундаментальной библиотеке ФГБОУ ВПО «Санкт-Петербургский государственный политехнический университет». Автореферат диссертации доступен на официальном сайте СПбГПУ (http://www.spbstu.ru/).

Автореферат разослан «05 » 2014 г.

Ученый секретарь

диссертационного совета г----

Д 212.229.18 к.т.н., доцент К--' Васильев Алексей Евгеньевич

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

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

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

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

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

— автоматизации преобразования требований, понятных заказчику и разработчику, в

модели на языке, воспринимаемом системой верификации;

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

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

Проведенный в работе анализ области автоматизации доказательства корректности

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

Для описания требований на ранних этапах разработки системы в технологии VRS/TAT использован язык спецификаций Use Case Map (UCM). Его отличительными особенностями являются простота графической нотации и ориентированность на описание поведенческих сценариев систем. Для доказательства корректности UCM-модели проектируемой системы и формирования тестовых сценариев инструментальная система VRS/TAT использует промежуточный формальный язык базовых протоколов, разработанный А. А. Летичевским.

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

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

Для достижения цели в работе решены следующие задачи:

— представлен анализ языков описания спецификаций требований и обоснован выбор языка UCM;

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

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

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

— создан метод автоматического преобразования иСМ-модели, содержащей многопоточные конструкции, временные задержки и прерывания, в формальную модель на языке базовых протоколов, с которым работают инструменты верификации и автоматизации тестирования УКБ/ТАТ;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

На базе полученных научных результатов разработан комплекс программных средств, интегрированный в технологию УГ^/ТАТ. Усовершенствованная технология УЯ5/ТАТ применена в ряде промышленных телекоммуникационных проектов и показала высокую эффективность при проверке качества создаваемого программного обеспечения, позволив сократить трудоемкость разработки тестовых сценариев на 25 % по сравнению с принятым в настоящее время подходом.

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

спецификаций. Применяются стандарты языков Use Case Map (UCM) и Message Sequence Charts (MSC).

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

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

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

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

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

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

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

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

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

Основные положения и результаты диссертационной работы доложены и обсуждены на региональных и международных научных конференциях: «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» на кафедре «Информационные и управляющие системы» СПбГПУ. Практическое использование представляемых на защиту результатов подтверждено соответствующими актами о внедрении.

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

СОДЕРЖАНИЕ РАБОТЫ

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

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

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

Для сравнения технологий повышения качества программного продукта были выделены только технологии, использующие формальные модели систем на языке UCM. К ним относятся: SPEC-VALUe, RT-TROOP, UCM/SDL IILTD, UCM CPN и инструментарий автоматизации верификации и тестирования VRS/TAT. На основе сравнительного анализа выделена технология VRS/TAT как технология, занимающая преимущественное положение по сравнению с остальными за счет того, что позволяет проводить не только верификацию модели, но и генерацию и исполнение тестовых сценариев. Как показано в работе, несмотря на указанные преимущества, и эта технология не свободна от недостатков.

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

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

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

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

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

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

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

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

Во второй главе представлен анализ методов и подходов к доказательству корректности исходных требований, которые используются в автоматизированной технологии верификации и тестирования УЯ5/ТАТ.

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

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

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

2. Использование представленных методов в системе позволяет осуществить проверку программных проектов больших размеров.

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

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

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

Рисунок 1 - Схема модернизированной технологической цепочки У118/ТАТ с интегрированными методами построения формальной модели и анализа тестовых сценариев

Ниже приведен список разработанных методов, а также особенностей их реализации.

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

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

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

По неформальному описанию требований (рисунок 2, столбец «Requirements», переход. I) выделяются согласуемые с заказчиком сценарии проверки (рисунок 2, столбец «Scenario of requirement», переход. 2). Сиенарни проверки представляют собой последовательность действий пользователя и откликов системы на входные воздействия, которые необходимо осуществить и наблюдать для доказательства корректности требования. Затем сценарии проверки требований формализуются последовательностью событий (рисунок 2, столбец «Traceability», переход. 3) на языке UCM, которые затем наносятся на UCM-диаграмму.

Identifier [Requiraments {scenario of requirementjTraceabiifty

_I_I_II_J_

1 Включение и вынл<оче«уе "Автомобильного pattern"

1 RAD05 Нажат»« на киоску 'Of екгг>очг«<г раамо Ф 1. Hi>43'i> wr-игчу ''0«' HAD Яе-з К

2 КАО Мзжагие "О"" выкачает рцзио 1. -Off" 2 У5са*'ы;», -Ус *аг»<£< .RADC-2 Я-х; Ra-lOfl

Рисунок 2 - Схема реализации метода перехода от требований к формальной модели на языке иСМ

Проектируемая система «S» может быть представлена в виде совокупности требований «req»:

s= Ure4(^)-

/<s!l,\¡

где р — номер требования; N — общее число пунктов требования. Каждый из пунктов требований может быть представлен кортежем:

Req = (Pre, Events, Post), где Pre — описание состояния системы, в котором под действием событий Events, система переходит в состояние Post.

Выделяя подпоследовательность событий из множества событий Events, пользователь формирует критериальную цепочку (Chain):

Chain = Cj —» в2 —> ■ ■ ■ —> еп,

где каждое событие ее Events, п - размер множества событий Chain.

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

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

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

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

Предложенный метод автоматического анализа метаданных проекта включает три типа проверок:

— проверку корректности описания окружения, разработка которого осуществляется согласно правилам описания грамматики окружения;

— проверку корректности описания метаданных элементов проекта, заданных согласно правилам описания грамматики метаданных;

— проверку пересечения имен атрибутов системы, имен иСМ-элементов, состояний и имен агентов.

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

Таблица 1 - Ограничения на разработку многопоточных систем

№ п/п Название иСМ-диаграмма Ограничение

1 Неограниченное рекурсивное порождение потоков 51зг*Рс!г* А Ог*И1 а Ап^Гогк С Запрещается использовать неограниченное рекурсивное порождение потоков

2 11арушение баланса скобок ""¡Г и . А(|.5.|«с<> Запрещается использовать параллельные конструкции с нарушением структуры потоков

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

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

Под потоком Т будем понимать четверку Т = (5,Р,С,Е), где 5" — элемент диаграммы, который порождает поток; Р — множество всех потоков, которые являются «родителями» данного; С — множество всех потоков, которые являются «дочерними» к данному; Е — множество элементов диаграммы, которые входят в этот поток.

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

Гб Г — ;'-й поток, содержащийся во всех потоках Т: иСМ-модели, где /е ¡1: Д'|;

Т.*' — ;'-й поток, порожденный на элементе^, где 5 е 5;

———> 5™'" — иСМ-элемент 5]"", достижимый из элемента за < п > шагов;

Т —» С— поток Т., приводящий к порождению дочернего потока С.;

Т1 1. Т — поток Т. .синхронизирующийся с потоком Т.;

йе Г— поток Т, использующий ресурс Л.

Критерий, определяющий неограниченное рекурсивное порождение потоков, определяется формулой:

О/Т*' е Т ) н> (С/- еТ)&(5, <Л,,||> >5,„)&(5. = 5,„).

Критерий использования параллельных конструкций с нарушением структуры потоков определяется формулой:

(УТ"' бГ)1 (С,'" еТ)&(Т^С,).

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

(Те Г)||(Ге Г)&(/?е Г)&(Яе Т.).

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

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

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

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

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

Таблица 2 - Трактовка иСМ-конструкций формулами инсерцнониого программирования

Название конструкции иСМ-днаграмма Семантическая трактовка Комментарии

Апс1Рогк н:: 7],..., Тг созданные в системе процессы.

Апс1.1ои1 ^ 5 = с/н'ск (соишег^) > 0 & ...&со1ткт{Тп)>()). арр1у(сошиег(Т11) + \).3 соип1ег(Т) - счетчик вошедших на элемент потоков по определенной ветке, 5 - состояние агента на элементе, п - номер потока

\Vaiting Р)асе I Г*1 I 5 = с/итк(с).Т «с» — условие ожидания наступления события; «Т»— состояние перехода агента.

Типег Б=с1}еск((с1 чсг)& 1пжсг{Т)> 0). арр1у{1П£$ег := 0 ).Т « С| », « С-, » — уел о в и я исходящих ветвей таймера. «1г1 Т )>0» — условие наступления события отмены таймера

РаПиге Рот! & < Т1 _ Т2 о- Тс О- 5 = с1к'ск((\с).Т\ + с/}сск(с)мрр1у{с\р1{Т,) := 1 & ...&схр1(Т„)--\).1шсг1{Т2.....Г) «с» — условие наступления прерывания, Т1 — состояние нормального исполнения, следующее за прерыванием. ехрЦТп) — установка флага прерываний и запуск обработчика прерывания на исполнение

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

на основе гидов.

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

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

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

формализация

исм-

модель

Верифицировав модель

Генерация гг.егтсв

Днлпт ре 1упьт.1тлв

Набор тестов

1

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

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

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

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

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

В пятой главе представлены результаты внедрения разработанных методов в автоматизированную технологическую цепочку верификации и тестирования VRS/TAT. Здесь проанализированы показатели эффективности применения в четырех экспериментальных проектах: «Автомобильное радио» — проект, моделирующий поведение автомобильного радио; SMTP - модуль широко используемого сетевого протокола, предназначенного для передачи электронной почты в сетях TCP/IP ; C'DMA модуль базовой станции системы, реализующей технологию Control Division Multiple Access; «Спутниковый терминал» — модуль системы, отвечающий за взаимодействие базовой станции оператора со спутником и обеспечивающий ее подключение к необходимому контроллеру.

Результаты, полученные в рамках применения технологии VRS/'ТАТ после интеграции метода автоматической проверки ограничений на элементы и конструкции языка UCM, свидетельствуют о более чем трехкратном сокращении трудоемкости поиска и исправления ошибок по сравнению с ручным подходом. Рисунок 4 иллюстрирует показатели сокращения трудоемкости в экспериментальных проектах.

Лькмжлшж« 1»яио SMTP

Рисунок 4 - Диаграмма сопоставления ручного и автоматизированного подхода поиска и исправления ошибки Результаты, полученные в рамках применения технологии УЯБ/ТАТ после интеграции метода автоматического преобразования многопоточных модели на языке С1С'М в модель на языке базовых протоколов, свидетельствуют о сокращении трудоемкости в 2,5 раза по сравнению с ручным подходом.

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

Рисунок 5 - Диаграмма сопоставления ручного и автоматизированного подходов создания одного базового протокола Таблица 3 демонстрирует преимущества применения технологической цепочки У'ЯЗ/ТАТ (с использованием разработанных методов) по сравнению с неавтоматизированным подходом.

Таблица 3 - Оценка преимущества технологии \ К8/ТЛТ при разработке тестовых сценариев

Проект Количество требовании Количество базовых протоколов Трудоемкость создания тестовых сценариев с применением разработанных методов (человеко-недель) Трудоем кость разработки тестовых сценариев без использования разработанных методов (человеко-недель) Оценка сокращения трудоемкости <%)

Автомобильное радио 30 35 2,5 3,2 22

SMTP 24 30 2,3 2.9 21

CDMA 148 205 3,2 4,3 17

Спутниковый терминал 430 392 5 6,9 28

Результаты, полученные в рамках применения модернизированной технологической цепочки У118/ТАТ на четырех экспериментальных проектах, свидетельствуют в среднем о 25 % - ном сокращении трудоемкости по сравнению с существовавшим подходом. Учитывая, что сокращение трудоемкости проекта эквивалентно сокращению себестоимости тестирования, полученный результат является существенным для промышленного производства программного продукта.

На рисунке 6 изображена диаграмма сравнения трудоемкости разработки тестовых сценариев вручную и автоматически при использовании технологии УГ^/ТАТ с интегрированными методами.

Мшм

....... Двтомагтоироеанный подход

ж Ручной подход

24

3(1

148

430

Кол-во базовых протоколов

Рисунок 6 - Графики трудоемкости разработки тестовых сценариев

Проведенный в главе 5 анализ результатов применения разработанных методов технологии УЯБ/ТАТ для приведенных проектов позволяет сделать следующие выводы:

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

— каждый из методов дает значительный выигрыш во времени по сравнению с ручным подходом при решении аналогичных задач. Так, например, применение метода анализа покрытия и автоматизированного поиска причины расхождения трассы и гида приводит к сокращению трудоемкости на один порядок. Метод проверки ограничений на элементы и конструкции языка иС'М позволяет добиться как минимум 3-кратного сокращения трудоемкости поиска ошибок (рисунок 4). Метод автоматического построения формальной модели на языке базовых протоколов сокращает до 2,5 раза время создания формальной модели на языке базовых протоколов;

- в рамках всей технологии УК8П'ЛТ после интеграции разработанных методов трудоемкость создания и отладки тестовых сценариев по сравнению с неавтоматизированными этапами сокращается более чем на 25 %;

- использование инновационных методов вне зависимости от особенностей проекта и детальности критериальных цепочек позволяет обеспечить покрытия требований на 100 %;

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

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

ЗАКЛЮЧЕНИЕ

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

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

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

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

— метод автоматического анализа UCM-модели на наличие синтаксических и семантических ошибок;

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

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

— методика автоматизированного поиска и анализа ошибок в гидах, участвующих в процессе генерации тестовых сценариев.

3. Внедрена при разработке промышленных телекоммуникационных проектов в компаниях ЗАО «Моторола Солюшнз», ООО «ЛЭПКОС» усовершенствованная технология VRS/TAT, которая доказала свою эффективность при проверке качества разработанного программного обеспечения, обеспечив 25 % сокращение трудоемкости разработки тестовых сценариев по сравнению с традиционным подходом без использования методов.

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

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

350 KLOC на языке программирования Java. Объем документации на программное обеспечение и методы автоматизации составил более 200 страниц.

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

СПИСОК ОСНОВНЫХ ПУБЛИКАЦИЙ ПО ТЕМЕ ДИССЕРТАЦИИ

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

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

3. Никифоров И.В., Петров A.B., Юсупов Ю.В., Генерация формальной модели системы по требованиям, заданным в нотации USE CASE MAP // Научно-технические ведомости СПбГПУ. № 4(103). СПб.: Изд-во Политехи, ун-та, 2010. — С. 191-195. (Издание из перечня ВАК).

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

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

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

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

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

9. Никифоров И.В., Маслаков А.П., Котляров В.П., Отладка UC'M-проекта при генерации тестовых сценариев // XLI Неделя науки СПбГПУ. Материалы межвузовской научно-технической конференции. 3-8 декабря 2012 г. СПб.: Изд-во Политехи, ун-та, 2012. — С. 86-87.

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

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

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

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

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

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

16. 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. (Издание из перечня ВАК).

17. Tyutin В.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.

Подписано в печать 07.04.2014. Формат 60x84/16. Печать цифровая. Усл. печ. л. 1,0. Тираж 100. Заказ 11766Ь.

Отпечатано с готового оригинал-макета, предоставленного автором, в типографии Издательства Политехнического университета. 195251, Санкт-Петербург, Политехническая ул., 29. Тел.: (812)550-40-14 Тел./факс: (812) 297-57-76

Федеральное государственное бюджетное образовательное учреждение

Высшего профессионального образования «Санкт-Петербургский государственный политехнический университет»

На правах рукописи

04201457674 Никифоров Игорь Валерьевич

МЕТОДЫ АВТОМАТИЗАЦИИ ПОСТРОЕНИЯ ПОВЕДЕНЧЕСКОЙ МОДЕЛИ ПРОГРАММОГО ПРОДУКТА НА ОСНОВЕ иСМ-СПЕЦИФИКАЦИЙ

Специальность 05.13.11 -Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей

Диссертация на соискание ученой степени кандидата технических наук

Научный руководитель -кандидат технических наук, доцент, В. П. Котляров

Санкт - Петербург - 2013

Оглавление

Введение...........................................................................................................................5

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

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

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

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

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

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

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

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

1.2.3. Язык Use Case Map..................................................................................24

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

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

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

1.4. Выводы..............................................................................................................37

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

проекта................................................................................................................66

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

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

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

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

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

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

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

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

гидов....................................................................................................................80

3.6. Выводы..............................................................................................................81

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

5.5. Выводы............................................................................................................132

Заключение..................................................................................................................134

Литература...................................................................................................................137

ПРИЛОЖЕНИЯ...........................................................................................................150

Приложение 1.........................................................................................................150

Приложение 2.........................................................................................................153

Приложение 3.........................................................................................................158

Приложение 4.........................................................................................................169

Приложение 5.........................................................................................................173

Приложение 6.........................................................................................................176

Приложение 7.........................................................................................................182

Приложение 8.........................................................................................................190

Приложение 9.........................................................................................................193

Приложение 10.......................................................................................................198

Приложение 11.......................................................................................................200

Введение

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, описыв�