Тестирование на основе формальных спецификаций в процессах разработки программных комплексов

• Автор: Петренко, Александр Константинович
• Шифр специальности: 05.13.11
• Научная степень: Докторская
• Год защиты: 2003
• Место защиты: Москва
• Количество страниц: 59 с. : ил.; 20х14 см

Работа выполнена в Институте Системного Программирования Российской Академии Наук.

Официальные оппоненты членкорреспондент РАН,

доктор физикоматематических наук, профессор

Королев Лев Николаевич

доктор технических наук, профессор, заслуженный деятель науки и техники РФ

Липаев Владимир Васильевич

доктор физикоматематических наук, профессор

Терехов Андрей Николаевич

Ведущая организация Вычислительный Центр РАН

Защита диссертации состоится ноября г. в часов на заседании диссертационного совета Д 2.7. при Институте Системного Программирования РАН по адресу
, Москва, Б. Коммунистическая , Институт Системного Программирования РАН, конференцзал.
С диссертацией в форме научного доклада можно ознакомиться в читальном зале библиотеки Института Системного Программирования РАН.
Диссертация в форме научного доклада разослана 3 октября г.
Ученый секретарь диссертационного совега кандидат физикоматематических С.П.Прохоров
Общая характеристика работы
Аннотация
Диссертация посвящена актуальной проблеме разработки единой методологической базы, позволяющей использовать формальные методы в тестировании реальных программных комплексов.
Соискателем предложен новый подход для автоматизации тестирования. Суть подхода состоит в придании новой роли формальной спецификации программ в жизненном цикле разработки программного обеспечения. Помимо традиционного использования формальных спецификаций на фазе проектирования, было предложено использовать их на всех фазах, начиная от фазы уточнения требований, кончая фазами тестирования и приемных испытаний.
В практическом плане под руководством соискателя была разработана технология спецификации и тестирования программных интерфейсов. Эта технология позволяет создавать формальные спецификации на расширениях языков программирования и автоматически генерировать компоненты тестирующих программ, которые, в свою очередь, в автоматическом режиме выполняют генерацию тестовых воздействий и анализ результатов тестирования. Технология прошла апробацию в проектах тестирования операционных систем реального времени, телекоммуникационных протоколов и компиляторов, тем самым была показана применимость данного подхода для широкого класса программных систем.
Актуальность


Сомнение может быть в другом не слишком ли рано мы пытаемся внедрить формальные методы в реальные программистские проекты, причем не в относительно простые фазы, типа прототипирования и эскизного проектирования, а в самые дорогостоящие фазы, такие как в тестирование, где приходится иметь дело не с моделями, сложностью которых исследователь может управлять, а с реальными комплексами, которые приходится тестировать как есть то есть, не меняя размеров, структуры и сложности целевого ПО. Попыткой снять эти сомнения является данная диссертационная работа. Методы, которые рассматриваются в ней, показали возможность использования формальных спецификаций в тестировании реального ПО, включая операционные системы реального времени, компиляторы и реализации телекоммуникационных протоколов. В пользу растущей актуальности этой тематики говорит заметное увеличение числа публикаций по использованию формальных методов для задач тестирования в последние лет. Целью данной работы является разработка теории и методики автоматизации тестирования программных комплексов на основе формальных спецификаций программ. Достижение этой цели требует решения нескольких подзадач. Первой из них является построение рамочной концепции организации тестирования на основе использования формальных спецификаций в контексте индустриальных процессов разработки ПО. Предложенный подход к тестированию рассматривает формальные спецификации или формальные модели программ как отправную точку для организации процессов тестирования и построения собственно тестов. Эта позиция в корне отличается, с одной стороны, от традиционного подхода к тестированию, который за отправную точку берет структуру реализации, и, с другой стороны, от традиционного рассмотрения моделей и спецификаций как средства для поддержки только проектирования и прототипирования. Предложенный подход позволил поновому позиционировать сами формальные спецификации и пересмотреть их роль во всех фазах жизненного цикла, начиная со спецификаций требований, заканчивая приемными испытаниями и сопровождением программных комплексов. Традиционная схема разработки программных комплексов, которые должны отвечать высоким требованиям качества, в первую очередь, надежности, выглядит следующим образом Майерс, i, i, Липаев разрабатываются функциональные требования, затем создается проект, на основе проекта выполняется реализация программирование и отладка. На этапе проектирования создаются формализованные спецификации. Они используются как часть постановки задачи для разработчиковпрограммистов и для разработчиков системных тестов. После тестирования отдельных модулей создаются тесты для подсистем это так называемое интетрационное тестирование. В самом конце очередного витка жизненного цикла дорабатываются системные тесты, и проводится системное тестирование, а потом приемосдаточные испытания. Недостатки этой схемы следующие разработка тестов модулей начинается поздно, поэтому общие сроки разработки удлиняются проектные решения могут оказаться несогласованными с функциональными требованиями, и нет автоматизированной процедуры, позволяющей проверить эту согласованность между ними. Для обеспечения предложенного подхода были разработаны новые нотации для описания спецификаций, тестовых сценариев, моделей тестового покрытия. Была разработана унифицированная архитектура верификационного набора, включающего в себя компоненты спецификаций и компоненты тестовой программы. Были разработаны методики для построения спецификаций и тестов для программных компонентов модулей иили подсистем, предоставляющих программный интерфейс ii I I, и для процессоров сложных структур данных, таких как блоки компиляторов, трансляторы и конверторы протокольных сообщений методы генерации тестов для реализаций телекоммуникационных протоколов. При решении технических проблем разработки инструментов генерации тестов были решены теоретические и методические проблемы автоматической генерации метрик тестового покрытия, автоматической генерации тестовых оракулов программ автоматического анализа поведения тестируемой программы, автоматической генерации тестовых последовательностей наиболее сложной проблемы тестирования объектноориентированного ПО, проблемы тестирования ПО на соответствие с моделями разного уровня детализации.