Содержание к диссертации
Введение
1. Обзор подходов проверки качества программного обеспечения 9
1.1. Методы обеспечения качества программного обеспечения 9
1.2. Методы и особенности тестирования 10
1.2.1. Методы автоматизации тестирования 13
1.2.2. Инструментарий тестирования 16
1.3. Формальный подход к проблеме обеспечения качества ПО 20
1.3.1. Математический аппарат моделей программ 23
1.3.2. Обзор моделей программ 24
1.4. Методы верификации 25
1.4.1. Нотации описания систем 26
1.4.2. Дедуктивные методы верификации 27
1.4.3. Методы проверки на модели 27
1.5. Инструментарий верификации 30
1.5.1. Сравнительный анализ средств верификации 33
Выводы 39
2. Методики интегрированной технологии верификации и тестирования 40
2.1. Общая схема технологии автоматизированной верификации и тестирования 40
2.2. Используемые формальные языки 42
2.3. Основы метода базовых протоколов 43
2.3.1. Базовые протоколы 44
2.3.2. Язык базовых протоколов 45
2.3.3. Базовый протокол в MSC 47
2.4. Система верификации VRS 49
2.5. Система автоматизации тестирования ТАТ 51
2.6. Обзор методик интегрированной технологии верификации и тестирования 52
2.6.1. Поиск ошибок в спецификациях 54
2.7. Методика формализации требований на основе базовых протоколов (МВР) 55
2.7.1. Создание БИА 57
2.7.2. Создание БИС 59
2.7.3. Создание БИФ 60
2.8. Методика доказательства заданных свойств системы на основе её модели на языке SDL с последующей генерацией кода (SAC) 65
2.9. Методика генерации тестового набора (TG) 69
2.10. Методика доказательства детерминированности поведения системы (ТСС) 75
2.11. Методика проверки аннотированных сценариев поведения системы (АС) 77
2.12. Методика автоматизации тестирования (ТАТ) 79
Выводы 82
3. Программная поддержка технологий автоматизации тестирования и верификации 84
3.1. Программная поддержка интеграции подсистем верификации и тестирования 84
3.2. Модуль генерации кода системы по множеству базовых протоколов 88
3.2.1. Блок запуска генерации 90
3.2.2. Блок анализа конфигурации 92
3.2.3. Блок генерации 97
3.3. Подсистема настройки на область тестирования 105
3.3.1 Графический пользовательский интерфейс 106
3.3.2 Генератор интерфейсного модуля 108
3.4. Характеристика разработанных программных средств 109
Выводы ПО
4. Результаты применения разработанных методов и средств автоматизации тестирования и верификации 112
4.1. Состав экспериментального комплекса 112
4.2. Применение технологии в телекоммуникационных проектах 113
4.3. Применение технологии в проектах связанных с мобильной телефонией 118
4.4. Применение технологии в проектах встроенных применений 120
4.5. Учебные проекты 125
4.6. Общая статистика и анализ результатов применения технологии 126
4.7. Оценки применения технологии в больших промышленных проектах 130
Выводы 133
Заключение 135
Литература
- Формальный подход к проблеме обеспечения качества ПО
- Основы метода базовых протоколов
- Модуль генерации кода системы по множеству базовых протоколов
- Применение технологии в проектах связанных с мобильной телефонией
Введение к работе
Одной из основных проблем, которую решают разработчики программного обеспечения (ПО), является проверка корректности его функционирования. Из практики известно, что проверка качества программного обеспечения начинается с разработки требований к проектируемой системе, продолжается до момента вьшода системы из эксплуатации и занимает до 50% времени всего жизненного цикла ПО. Этим определяется повьппепие требований к полноте и производительности подобных проверок, что приводит к появлению на рынке новых технологий и инструментария автоматизации контроля правильности функционирования ПО.
Для создания качественного ПО прежде всего необходимо обеспечить ясность в постановке задачи и методах её решения. Поэтому с ростом сложности ПО возрастает потребность в средствах визуального моделирования и проектирования, а также в специалистах, знающих и умеющих использовать их на практике. Программистское сообщество осознаёт, что резервы повышения производительности труда при создании качественного ПО связаны с системным подходом и использованием передовых методов и средств автоматизации разработки больших программных проектов. В данном направлении ведётся значительное количество исследований по созданию новых стандартов и инструментальных средств, которые объединяются в рамках такого направления как Computer Aided Software Engineering (CASE).
Стоимость исправления ошибок в пределах жизненного цикла продукта экспоненциально растёт в соответствии с фазой разработки [Воет]. Самой дешёвой фазой, на которой необходимо по возможности искоренить как можно больше ошибок является разработка требований и спецификаций.
Когда изменяются требования, основной проблемой становится корректировка тех частей продукта, которые уже прошли стадии кодирования и тестирования. Естественно, что подобные действия являются достаточно трудоёмкими, так как возвращают разработчиков на начальные этапы проекта в тот момент, когда код уже практически написан и ли тестируется. Подобного рода корректировки расходуют 30-50 % общего бюджета разработки [Воет], а ошибки в требованиях обходятся в 70-85% общей стоимости корректировки кода [Leffingwell].
требования разработка кодирование тестирование работа с
продуктом
Рис. 1 Стоимость исправлении ошибок в зависимости от стадии проекта
Как показывает рис. 1, гораздо сложнее исправить дефекты, которые найдены при эксплуатации продукта, чем в процессе его создания [Grady]. Следовательно, предотвращение ошибок в требованиях и обнаружение их на ранних этапах проекта сильно уменьшает объём корректировок продукта и таким образом сокращает общую стоимость разработки ПО. Именно поэтому в последнее время всё большее внимание специалистов в области разработки ПО уделяется различным стандартам позволяющим разрабатывать формальные требования на систему. Наиболее известными графическими стандартами являются UML [uml], SDL [sdl], MSC [msc]. Использование формального языка или процедуры для создания требований позволяет значительно сократить вероятность появления ошибки в спецификациях.
Во время разработки требований может быть порождено большое количество различных типов ошибок. Одной из основных проблем является несоответствие требований, разработанных техническим специалистом, с требованиями заказчика. Зачастую разработчики и заказчики говорят на языках разного уровня, что приводит к некорректному пониманию задачи и необходимости последующих корректировок в продукте, который уже прошел стадию составления требований и дизайна. Неоценимую помощь в решении данного вопроса оказывает использование формальных языков и нотаций для создания требований, которые позволяют заказчику и разработчику вести диалог на одном языке и служат процессу искоренения различного рода двусмысленностей в спецификациях.
В настоящее время крайне актуальна проблема безопасности программных комплексов. При этом безопасность может трактоваться двояко: с одной стороны система не должна вести себя непредсказуемо в какой бы то ни было ситуации, с другой доступ в
7 систему должен быть жёстко ограничен. В последнее время часто приходится слышать о хакерских атаках, которые наносят огромный ущерб за счёт несанкционированного, использования функциональности программных комплексов. С точки зрения спецификаций проблема безопасности связана с полнотой требований на систему, в случае если требования не полны, в программе может образоваться потенциально опасное место для несанкционированного доступа. По этой причине при разработке критичных к вторжению систем всё чаще используются формальные методы позволяющие проводить доказательства правильности функционирования.
Существующие в настоящее время на рынке технологии и инструменты для разработки ПО далеко не во всем обеспечивают решение поставленной проблемы. Это является следствием их узкой направленности на определённые этапы жизненного цикла. Существуют эффективные нотации для описания требований, такие как: UML, MSC, SDL, VDM, Alloy, NP, В, RSL, LOTOS, ML, Isar, PVS, CASL, SMV, Promela, Esterel, SCR, Murphi и другие. Представленные нотации основаны на таких широко известных моделях программ как сети Петри (Петри), конечные автоматы (Мили, Мура и др.), темпоральные логики (Приора), алгебры параллельных процессов(Милнера, Хоара, Бергстры и Клоппа), транзициоиные системы(Парка), агенты и среды(Летичевского и Гилберта). В тоже время существует множество инструментов верификации, разработанных в различных научных лабораториях по всему миру: LOTOS (организация ISO), 8ріп(лаборатория BellLabs), Кгопоз(лаборатория VERIMAG), SCR(na6opaTopra NavalResearch), VRS (организация ISS) и другие, и инструменты автоматизации тестирования созданные известными компаниями по разработке ПО, это Rational Rose компании IBM, Telelogic TAU компании Telelogic AB, TAT компании Motorola, Together компании Borland и другие.
Тем не менее, в настоящее время практически нет промышленных технологий, позволяющих совместно использовать инструментарий тестирования и верификации. Особенно актуальна данная проблема в области создания реактивных систем встроенного применения, где очень важны поведенческие свойства и где для полноценного обеспечения корректности поведения системы необходимо проверить множество сценариев за время не превышающее сроки, предусматриваемые на эту деятельность в программном проекте.
Настоящая работа посвящена созданию технологии, обеспечивающей совместное использование верификации и тестирования на основе требований, описанных в формальных нотациях и поддерживающей все этапы жизненного цикла ПО. Технология основывается на создании требований в виде множества базовых протоколов, каждый из которых описывает элементарное событие в рамках поведения системы. На основе
8 разработанных протоколов технология позволяет проводить верификацию различных свойств, а также автоматическую генерацию кода тестов и системы. Она также учитывает возможность применения сопутствующих технологий, использующих формальные нотации UML, SDL и MSC.
В ходе работы создан программный продукт, обеспечивающий интеграцию всех частей технологии. Результирующая система опробована на реальных проектах. Её применение позволяет сократить время работы над проектом и обеспечить выигрыш во времени на всех этапах разработки ПО.
Для достижения поставленной цели в работе выполнено следующее:
Проведён анализ существующих на рынке инструментов автоматизации тестирования с целью оценки возможностей интеграции с инструментами верификации и тестирования при условии использования формальных языков.
Описаны и проанализированы наиболее известные формальные модели программ, служащие базисом известных инструментов верификации и тестирования.
Проведён анализ инструментов верификации с целью выявления возможностей по их использованию в промышленном процессе создания ПО.
Предложена и описана методика создания формальных спецификаций к программному обеспечению на основе теории базовых протоколов.
Предложены и описаны методики по совместному использованию инструментов верификации и тестирования на различных стадиях разработки ПО.
Разработан и программно реализован алгоритм преобразования модели, основанной на представлении свойств системы в виде базовых протоколов, в язык SDL.
Разработан программный комплекс, позволяющий автоматизировать переход от фазы верификации к фазе тестирования.
Проверена работоспособность предложенной технологии и инструментальных средств в нескольких проектах по производству ПО.
Проанализированы результаты применения интегрированной технологии в различных проектах и проведено прогнозирование результатов использования технологии в больших промышленных проектах.
Формальный подход к проблеме обеспечения качества ПО
Программное обеспечение часто используется в критичных к ошибкам областях человеческой деятельности. Именно поэтому гарантии качества производимого продукта являются неотъемлемой частью современного процесса производства ПО. В п. 1.2-1.4 были рассмотрены основные подходы обеспечения качества ПО средствами тестирования, этапы, подлежащие автоматизации и инструментарий, позволяющий проводить различного рода автоматизацию тестирования. Как было отмечено, задача тестирования состоит в создании входного набора тестов достаточных для проверки качества ПО, в соответствии с выбранным критерием и его прогоне на тестируемом приложении. Поскольку набор тестов конечен и урезается в соответствии с ограничениями проектных сроков, то только экспертиза человека в процессе тестирования позволяет гарантировать качество, но эта гарантия грешит субъективизмом. Поэтому в последнее время всё большее распространение получает формальный подход. Формальный подход - это подход позволяющий создавать описания действий и данных в некоторой формальной нотации, то есть нотации со строго определённым синтаксисом и семантикой, и использовать формальные методы для интерпретации формальных задач. Формальные нотации (языки) обеспечивают, строгость описания, при которой не может быть допущена двусмысленная трактовка созданной спецификации.
Формальные методы используют математическую логику и дискретную математику в процессе разработки ПО. В [ms] приведено следующее определение формальных методов: "Методы спецификации и производства программного обеспечения, основанные на математических системах и включающие в себя: множества математических нотаций для создания спецификаций, описания фаз дизайна и производства ПО, логические системы, предназначенные для верификации, и методологическую среду на основании которой может быть проведена формальная верификация".
Если требования и спецификации на ПО, заданные в проектных документах, формализовать - то есть описать на формальных языках проектирования, то к таким описаниям могут быть применены формальные методы. В настоящее время существует множество формальных языков для подобного описания. Основной их задачей является описание процесса, данных, структуры и архитектуры программных средств или тестов для облегчения и ускорения процесса создания ПО. Здесь стоит упомянуть такие языки как RSL [Mil90a], LOTOS [LOTOS88], SDL [sdl], UML [uml], MSC [MSC], Estelle [ESTELLE88], ML [ml], CASL [cats], SMV [SMV92] и множество других. Такое разнообразие связано с тем, что каждый из перечисленных языков создавался для решения задач в определённой области производства ПО. Переход к унифицированному стандарту произошёл в конце 90-х с появлением языка UML (Unified Modeling Language). UML включает набор различных типов диаграмм, удобных для описания архитектурных решений приложений через протоколы, конечно - автоматные реализации, описывающие структурные и поведенческие характеристики, потоки данных и т.п.
В общем случае формальные описания требований, тестов и программ позволяют добавить в процесс создания ПО два мощных метода - генерацию и верификацию. В работе рассмотрено применение генерации и верификации к процессам проектирования и тестирования
Как указывалось выше, к сложным задачам для тестировщика относится создание набора тестов в соответствии с некоторым критерием. Для решения этой задачи перспективно применение генерации, однако если требования на программу заданы на не формальном языке (например, на естественном языке) применение метода генерации не возможно. Поэтому для генерации перевод требований в некоторую формальную нотацию необходим, он же очень полезен как для разработчика, который будет точно знать и понимать, требования на входе и выходе системы, так и для тестировщика, который получает чёткое представление о поведении тестируемой системы. Когда требования представлены в формальном виде, то применение генерации становится возможным.
Другим методом, который может быть применён при формальном подходе, является верификация. В данной работе применение верификации сопряжено с тестированием, что позволит сократить усилия на этапе тестирования и повысить качество ПО. В случае когда требования на систему описаны формально, с достаточной степенью точности верификация позволяет проверить утверждение о правильности спецификации ещё на этапе разработки требований. Однако в настоящее время, когда применение формального подхода ещё не достаточно распространено, для разработчиков, а тем более для заказчика ПО разработка детальных формальных требований представляет достаточно большую проблему. Поэтому верификация в существующей практике применяется только для проверки компонент системы или их свойств. Имея формальные требования на систему или компоненту, разработчик может преобразовать их в прототип системы (модель) на формальном язьпсе и проверить её свойства. Нужно отметить что всё это происходит ещё до начала фазы разработки кода что приводит к существенному снижению затрат на исправление ошибок [Воет]. В процессе верификации проводите я анализ, значений переменных и состояний системы, что позволяет сократить мощность множества тестов, необходимых для проверки системы. Процесс верификации более детально рассмотрен во второй части работы.
Рассмотрим историю развития формального подхода. Первые эксперименты в этом направлении проводились в рамках применения логик 1 и 2-го порядков для доказательства корректности последовательных программ. Прорыв в области теории формальных методов произошёл в конце 70х годов, когда А. Пнуэли предложил использовать темпоральную логику (ТЛ) для спецификации свойств программ и разработал алгоритм проверки правильности формул на модели программы. Это стало стартовой точкой в развитии формального подхода к проблеме анализа параллельных программ. С тех пор появилось множество публикаций на тему использования ТЛ для верификации распределенных программ, был создан ряд исследовательских и коммерческих систем для спецификации и верификации параллельных программ [12]. В то же время началось бурное развитие в области создания нотаций моделей программ, в результате появились наиболее известные в настоящее время модели: это сети Петри, конечные автоматы, регулярные выражения и алгебры процессов (см. приложение 1). Объединение формализмов ТЛ и моделей программ привело к созданию первых реализаций алгоритмов верификации известных как алгоритмы проверки на модели (model checking). В то же время формальные нотации стали применяться для использования в математических доказательствах дедуктивных методов.
В настоящее время формальный подход бурно развивается. В 90-х годах большинство систем верификации и тестирования реализовывались как автономные программные
продукты, в которых использовались внутренние языки спецификаций и описания моделей. Для их практического применения требовалось преобразовывать код программы во внутреннее представление системы верификации. При обнаружении ошибки возникали сложности при переносе результатов верификации на спецификацию или код реальной системы, после исправлений которых, нужно бьшо корректно перенести результаты исправлений в систему верификации. В настоящее время существует тенденция к объединению различных подходов к верификации и их стандартизации, также к упрощению формальных нотаций. Всё это позволяет участвовать в процессе проверки качества ПО не только разработчикам и тестировщикам, но и заказчикам. Как уже упоминалось, ярким представителем данной тенденции является стандарт UML-нотации появившийся в начале 90-х годов.
Основы метода базовых протоколов
В качестве языков нотации в интегрированной технологии выбрана тройка популярных языков спецификации UML, SDL, MSC. UML является более общим языком чем SDL и MSC. В текущем стандарте существует более 10 типов диаграмм описывающих систему с различных сторон. В этом множестве диаграмм представлены и диаграммы состояний, являющиеся основополагающими для языка SDL и диаграммы последовательностей событий (обмена событиями) по сути представляющие собой диаграммы языка MSC. Язык UML не включает в полной мере всего синтаксиса языков SDL и MSC, но средства описания систем и их поведения, реализованные в этих трёх языках, очень схожи.
Существующие инструменты верификации преимущественно применяют собственные специализированные языки: VDM-SL, NP, AMN, RSL, LOTOS, Estelle, ML, SMV, CASL, Promela, MSC, SDL, UML. Как видно из представленного множества (таблица 3) только языки MSC, SDL, UML используются как в инструментах верификации, так и в инструментах тестирования, что явилось одной из причин, выбора инструментов VRS и ТАТ, поддерживающих данные языки.
Как видно из таблицы 4 все использованные языки являются промышленными стандартами в области разработки ПО и обладают хорошей степенью визуализации, за счёт использования набора интуитивно понятных диаграмм. Однако имеют различные области применения: UML достаточно новый и перспективный язык и он может быть использован на всех стадиях разработки ПО, в то же время SDL и MS С более просты в использовании, зато практика их применения в промышленных проектах разработки ПО исчисляется десятилетиями. Таким образом, комбинация представленных языков является оптимальной для использования в рамках разрабатываемой технологии.
Метод базовых протоколов является одним из основных методов реализованных в инструменте верификации VRS. Целью применения данного метода является представление функциональных требований на систему в формальном виде, который в дальнейшем может быть использован для автоматической верификации и тестирования. В соответствии с методом базовых протоколов каждый вариант использования системы может быть представлен в виде последовательности событий. В большинстве случаев отдельное событие представляет собой посылку на систему или приём от системы какого-то сообщения. При этом каждое событие приводит к изменению состояния системы. Базовый протокол определяется как некоторая элементарная последовательность, приводящая к однократному изменению состояния системы. Таким образом, все возможные поведения системы, то есть её спецификация может быть представлена в виде множества базовых протоколов. В общем случае базовые протоколы представляют требования в виде троек Хоара [4] а —» и Д где и процесс, а и Д — логические формулы, определяющие пред и постусловия для процесса и. Требования, представленные в виде Хоаровских троек, по форме близки к требованиям и функциональным спецификациям, используемым в инженерной практике. Основным, отличием формулировки требований в современной технической документации, является использование естественного языка для выражения пред и постусловий, а также описания последовательностей действий, составляющих процесс базового протокола. Теория агентов и сред лежащая в основе метода базовых протоколов, детально описана в [agent].
Подробное описание метода базовых протоколов может быть найдено в [Ьр], в данном контексте рассмотрим только основные понятия и определения. Формально каждый базовый протокол представляет собой выражение вида \/х(а - и /?), где х - список (типизированных) параметров, а и /5 — формулы базового языка, и - процесс протокола (вполне определенное поведение). Формула а называется предусловием, а формула /3 -постусловием базового протокола. При этом, выражение для процесса параметризируется через параметризацию действий и разметок состояний. Сам базовый протокол может рассматриваться как формула темпоральной логики, выражающая тот факт, что, если (для подходящих значений параметров) состояние системы имеет разметку, удовлетворяющую условию а, то, процесс и может быть инициирован и, после его завершения, разметка будет удовлетворять условию р. Система, удовлетворяющая этому условию, называется реализацией системы базовых протоколов.
Модуль генерации кода системы по множеству базовых протоколов
Блок предназначен для получения начальной информации от пользователя, её обработки, вывода ошибок и запуска генерации при помощи блоков БАКФ и БГФП. Модуль ГКСБП реализован в виде консольного приложения на языке C++. Модуль запускается с использованием командной строки. bp2sdl -/filename [- d] f-hj
Где ключ f определяет наличие файла с конфигурацией в формате XML, d — ключ, указывающий на необходимость вывода отладочной информации на стадии анализа множества базовых протоколов и на стадии генерации SDL представления системы, h — ключ позволяющий выводить вспомогательную информацию о работе модуля ГСКБП.
Файл конфигурации автоматически генерируется модулем TG Client в процессе создания проекта разработки базовых протоколов и содержит всю необходимую информацию о конфигурации проекта и о множестве базовых протоколов. Схема работы блока запуска генерации в виде диаграммы состояний представлена на рис. 28.
Блок запуска генерации обрабатывает информацию, полученную из командной строки, и в случае появления ошибок выводит соответствующую информацию об ошибке. На данном этапе возможно возникновение следующих ошибок: "Error і: Wrong keys number" - ошибка множества ключей запуска. Возникает в случае если пользователь указал ключи не обрабатываемые системой. "Error 2: use -f key for input file" - ошибка нахождения ключа f. Возникает в случае если пользователь не указал обязательный ключ определяющий имя файла с конфигурацией. "Error 3: input file not found" - ошибка нахождения указанного файла конфигурации. Возникает, в случае если блоку БЗГ не удается открыть указанный конфигурационный файл. "Error 4: Pile format error" - ошибка формата файла конфигурации. Возникает в случае если указанный файл конфигурации не является файлом в формате XML.
В случае если все проверки выполняемые запуска анализа конфигурационного файла были успешно завершены, и не было обнаружено ошибок. Запускается блок БАКФ, который в свою очередь может вернуть сообщения об ошибках. Данные сообщения также обрабатываются в рамках работы блока БЗГ и выдаются пользователю.
Информация о имени и положении конфигурационного файла, а также информация о наличии опции вывода отладочной информации автоматически передаётся в модуль БАКФ при его запуске.
В случае если пользователь указал опцию вывода вспомогательной информации, на экран будет выдана краткая справка об использовании инструмента.
Блок анализа конфигурации
Данный блок предназначен для сбора информации о системе, на основе поступающего на вход конфигурационного файла. Блок запускается после проведения предварительного анализа в блоке БЗГ. Общая схема работы блока представлена на рис. 29. Рис. 29 Схема работы блока БАКФ
На вход блока поступает конфигурационный файл, на выходе формируется структурированный набор данных об агентах, сигналах и протоколах описанных в системе, представленных в виде структур языка C++. Таким образом на выходе блока пользователь получает информацию которая может быть использована для последующей генерации. Разделение блоков генерации БГФП и блока анализа БАКФ позволяет использовать, полученную в результате анализа информацию о базовых протоколах при генерации не только на языке SDL, но и при генерации любого другого текстового представления. Вся информация о протоколах представляется в виде набора структур: Информации об агентах typedef struct my_agents { string name; //Имя агента vector param params_info; //Список параметров } BP_agents; Информации о параметрах: typedef struct my_param { string name; string type; } param; //Имя параметра //Тип параметра Информации о сигналах typedef struct myBP_signals { string name; vector string paramtype; int paramnum; } BP_signals; Информации о базовых протоколах typedef struct myBP_information { char name[50]; vector string ins; char precondition[max_string]; vector mes mes_info; char postcondition[max_string] } BP_information; //Имя сигнала //Тип параметра //Количество параметров //Имя протокола //Список инстанций //Формула предусловия //Список сообщений ;//Формула пост условия Информации о сообщении typedef struct my_mess { string name; //Имя сообщения string from; //Источник сообщения string to; //Приёмник сообщения } mes ;
Для получения описанной выше информации в рамках блока реализованы следующие функции: int analyse_agents (char filename) - функция сбора информации об агентах. int analyse_signals (char filename) - функция сбора информации о сигналах. int analyse_protocols (char filename) - функция сбора информации о протоколах.
Представленные функции получают на вход конфигурационный файл и возвращают идентификатор ошибки, если она была обнаружена в процессе работы. Также на выходе функции изменяют структуры данных на основе полученной информации. Рассмотрим более подробно принципы работы функций. Функция analyse_agents анализирует информацию об агентах представленную в конфигурационном файле. Данная информация предоставлена в формате XML и имеет следующий вид: . AgentTypes AgentType name ( ) AgentTypeParameters AgentTypeParam name Type ( ) ParamTypes ParamType name Type Comment ( ) Agents Agent name typelD ( ) AgentParameters AgentParameter name parmld Type Initial ( ) ParamTypesInitial ParamTypelnitial name parmld Type Initial InitialState Comment Таким образом, для получения информации об агенте функция проводит поиск открывающего и закрывающего тега "AgentTypes". Внутри данной части XML представления проводится анализ: Тега " /AgentTypeParam " - для получения информации о типах агентов, представленных в конфигурации. Тега " /Agent " - для получения имён агентов рассматриваемого типа. Тега " /initiaistate " - для получения информации о начальном состоянии агента. Тега " /туре " - для получения информации о типах параметра агента. Тега " /initiai " - для получения информации о начальных состояниях параметров агентов. На основе полученной информации заполняются структуры "рагат" и "BP_agents". В процессе работы функции могут возникнуть следующие предупреждения и ошибки: "Error 5: wrong name of agent" - ошибка имени агента. Возникает в случае совпадения имени агента с зарезервированным в SDL словом. "Error 6: Wrong initial state name" - Ошибка ИМЄНИ начального состояния агента. Возникает в случае совпадения имени начального состояния агента с зарезервированным в SDL словом. "Warning 1: Undefined initial value of parameter" - ошибка определения начального значения параметра агента. Возникает в случае, если отсутствует определение начального значения. "Warning 2: No agents defined in project" - ошибка количества агентов. Возникает в случае, если в проекте отсутствует описание агентов.
В случае возникновения ошибки информация, содержащая её номер, передаётся в блок запуска генерации для дальнейшего анализа и выдачи пользователю.
Применение технологии в проектах связанных с мобильной телефонией
В работе была поставлена цель: создать интегрировашгую технологию автоматизированной верификации и тестирования, позволяющую совместно использовать инструментарий верификации и автоматизации тестирования в процессе производства промьшшенного ПО. Эта технология должна быть основана на верификации поведенческих функциональных спецификаций реактивных систем и их дальнейшем использовании для автоматической генерации тестового набора. Спецификации, подаваемые на вход технологии, должны быть созданы на формальных графических языках высокого уровня.
Для достижения цели в работе были решены следующие задачи: 1. Проведён анализ существующих методов и средств автоматизации тестирования и верификации, существующих в настоящее время на рынке ПО. 2. Проведён анализ наиболее распространённых формальных нотаций моделей программ. 3. Разработан и описан набор методик, позволяющих провести интеграцию верификационного инструментария и инструментария автоматизации тестирования в процессе разработки качественного ПО. 4. Усовершенствован инструментарий, выбранный в рамках анализа, что позволило автоматизировать переход от процесса верификации требований к процессу тестирования. 5. Разработаны программные реализации, позволяющие объединять различные методики с целью повышения качества ПО. 6. Предложенные методики и разработанная программная поддержка применены в реальных промышленных программных проектах. 7. Полученные в результате применения технологии результаты были проанализированы и показали эффективность применения технологии, также были сделаны оценки по применению технологии в промышленных программных проектах различной сложности.
Полученные в ходе работы основные результаты:
1. Проведен обзор существующих инструментальных средств верификации требований и автоматизации тестирования ПО. На основе их анализа сформулированы соответствующие требования к системам, которые могут быть использованы в рамках интегрированной технологии.
2. Определены недостатки существующих инструментальных средств поддержки верификации и автоматизированного тестирования. Среди недостатков отмечены отсутствие интерфейсов, позволяющих обеспечить совместное взаимодействие средств верификации и тестирования и отсутствие общей хорошо развитой, формальной графической нотации, понятной пользователю.
3. Проведен обзор и анализ существующих формальных моделей программ и их совместимости с существующим инструментарием верификации и тестирования. На основе анализа были показаны основные недостатки моделей, среди которых особо отмечены: невозможность описания в рассмотренных нотациях требований для крупных промышленных проектов и невозможность применения моделей к программным проектам различной направленности.
4. Разработана методика формализации на основе базовых протоколов (МВР), позволяющая описывать поведенческие требования в интуитивно понятной графической нотации.
5. Разработана методика доказательства заданных свойств системы (SAC) на основе её модели на языке SDL. В рамках методики описаны особенности верификации моделей на языке SDL с использованием инструмента VRS и предложены подходы к автоматическому переходу на стадию тестирования.
6. Разработана методика генерации тестового набора (TG), обеспечивающего полное покрытие функциональности системы, на основе инструментария верификации. В методику вошли рекомендации по описанию окружения генерации и стратегии ограничения тестового набора.
7. Разработана методика доказательства детерминированности поведения системы (ТСС), позволяющая определять возможные места возникновения недетерминизмов.
8. Разработана методика проверки аннотированных сценариев поведения системы (АС), позволяющая проводить проверку полноты описания системы в виде множества базовых протоколов.
9. Разработана методика автоматизации тестирования (ТАТ), позволяющая использовать результаты верификации на стадии тестирования.
10. Создан программный комплекс поддержки интеграции подсистем верификации и тестирования, обеспечивающий автоматизацию перехода с фазы разработки требований на фазу верификации и в дальнейшем на фазу тестирования.
11. Разработан модуль генерации кода системы по множеству базовых протоколов, позволяющий получать SDL код системы по множеству базовых протоколов с целью дальнейшей генерации целевого кода.
12. Доработана подсистема настройки на область тестирования, включённая в состав инструмента ТАТ.
13. Проведено пилотирование технологии в ряде промышленных программных проектов, проанализированы результаты эффективности применения технологии и сделана оценка использования технологии в больших проектах.
Анализ результатов использования технологии подтверждает работоспособность и эффективность разработанных методов и средств интегрированной технологии обеспечения качества программных продуктов с помощью верификации и тестирования.
В практическом плане на базе полученных научных результатов был разработан комплекс программных средств, предназначенных для совместного использования верификации и тестирования. Программный комплекс был использован в компании Motorola в 6 программных проектах по разработке встроенных систем в таких областях как: разработка мобильных устройств, телекоммуникационных и телематических систем. Кроме того, созданная технология и программные средства были внедрены в проекте разработки функциональной программной подсистемы управления узлами связи "83Т54-2М" в ОАО "Интелтех" и проекте "Исследование работы контроллера в системе распределённого электропитания железнодорожного вагона" в ЗАО "Северо-Западная лаборатория Лтд". Созданные методики и программные средства могут быть использованы для обеспечения качества реактивных систем в широком спектре встроенных применений.
Разработанные методы и средства технологии интегрированной верификации и тестирования программных изделий использованы в курсе лекций "Введение в технологии верификации" кафедры "Информационные и Управляющие Системы" СПбГТУ.
Общий объем разработанного программного обеспечения, вошедшего в программный комплекс поддержки интегрированной технологии, составил около 500 килобайт исходного кода на языках Tel и C++; объем документации на разработанное программное обеспечение -более 200 страниц.
