СИНТЕЗ ТЕСТОВЫХ ПОСЛЕДОВАТЕЛЬНОСТЕЙ ДЛЯ ДИСКРЕТНЫХ СИСТЕМ НА ОСНОВЕ РАЗЛИЧАЮЩИХ АВТОМАТОВ

ВВЕДЕНИЕ 5
1. Основные определения и обозначения 9
2. Генераторы конечных автоматов 15
2.1 Генератор конечных автоматов из программного пакета FSMTest-1.0 ... 15
2.2 Эксперименты по оценке эффективности генератора 17
2.3 Разработка генератора недетерминированных конечных автоматов 19
3. Синтез адаптивных различающих последовательностей 22
3.1 Метод синтеза адаптивной различающей последовательности 22
3.2 Экспериментальные результаты 25
ЗАКЛЮЧЕНИЕ 29
СПИСОК ИСПОЛЬЗОВАННЫХ ИСТОЧНИКОВ И ЛИТЕРАТУРЫ
Купить

Повсеместная цифровизация в различных сферах деятельности человека привела к развитию формальных методов анализа и синтеза информационных систем. В частности, передача информации сегодня требует не только разработки физических сред, таких как витая пара, оптоволоконный кабель, или мобильные сети, но и использования соответствующих протоколов передачи данных, обычно называемых телекоммуникационными протоколами. Поскольку от качества передачи данных зависит функционирование как социально значимых структур, банков, государственных институтов и т.д., так и пользовательских интернет-сервисов, которые часто связаны с проведением финансовых операций, много внимания уделяется вопросам проверки корректности телекоммуникационных систем. Одним из подходов к анализу таких систем является тестирование [1-3], которое заключается в синтезе тестовых последовательностей, их подаче на тестируемую систему и наблюдении полученных реакций, позволяющих проверить корректность системы относительно заданного эталона. Формальные методы синтеза тестов часто формулируются в терминах спецификации, описывающей эталонное поведение системы, тестируемой реализации и отношения конформности, позволяющего оценить соответствие реализации заданной спецификации [2, 4, 5]. Источником спецификации может быть техническое задание, RFC телекоммуникационного протокола, или иное неформальное описание системы, по которому формируется та или иная формальная модель для последующего анализа и построения проверяющего теста.
Конечные автоматы [6, 7] широко используются для моделирования программного и аппаратного обеспечения телекоммуникационных систем и их компонентов. Теория классических автоматов включает методы синтеза проверяющих тестов с гарантированной полнотой покрытия неисправностей, позволяющих идентифицировать реализации, описываемые заданным классом автоматов. Тем не менее, неизученным остаются многие вопросы, связанные с построением проверяющих тестов и их оптимизацией, в том числе, для неклассических автоматов [8-10].
Как уже отмечалось выше, одной из областей применения формальных методов синтеза являются телекоммуникационные протоколы, спецификации которых часто оказываются недетерминированными [8]. Под недетерминизмом в данном случае понимается существование в неформальной спецификации различных вариантов поведения системы на одно и то же входное воздействие. Недетерминизм в спецификациях телекоммуникационных протоколов часто связан с их опциональностью, например, RFC ряда протоколов содержит функционал, описание которого формулируется с использованием ключевых слов "MUST", "MUST NOT", "REQUIRED", "SHALL", "SHALL NOT", "SHOULD", "SHOULD NOT", "RECOMMENDED", "NOT RECOMMENDED", "MAY", "OPTIONAL" [11-13] и, соответственно, описывают как обязательные, так и опциональные свойства.
Недетерминированные автоматы получили широкое развитие с начала 90-ых, позволив описывать опциональные спецификации и увеличив выразительность автоматной модели. Конечно-автоматные методы синтеза тестов также были адаптированы для случая, когда спецификация является недетерминированным автоматом [14]. При синтезе тестов с гарантированной полнотой много внимания уделяется вопросам идентификации состояний [15], в частности, построению различающих последовательностей [8, 10]. Такие последовательности позволяют различить любую пару состояний автомата и используются для синтеза тестов W-подобными методами. Однако, различающие последовательности достигают экспоненциальной длины относительно числа состояний и не всегда существуют [15]. Адаптивные различающие последовательности существуют чаще и имеют меньшую длину, чем безусловные, что мотивирует их использование при построении тестовых последовательностей [8]. Алгоритм синтеза адаптивных различающих последовательностей для конечных автоматов хорошо известен [8, 10], основан на построении различающего автомата и позволяет построить такие последовательности в форме различающего тестового примера. В данной работе мы исследуем свойства адаптивных различающих последовательностей для конечных автоматов с различным количеством недетерминированных переходов.
Проведение экспериментов по исследованию свойств адаптивных различающих примеров требует решения двух подзадач: формирование экспериментальной выборки и построение различающих последовательностей для оценки их длины и вероятности существования. Генераторы конечных автоматов и программа синтеза тестовых примеров рассматривались в ряде работ по данной тематике [10, 16, 17], однако, требуют существенной доработки для исследования более широкого класса систем.
Экспериментальная выборка может содержать реальные системы, описанные конечным автоматом, однако построение автоматной модели по таким системам часто не может быть автоматизировано, что ограничивает размер выборки. Распространённый подход к формированию экспериментальной выборки заключается в генерации случайных конечных автоматов [16], что позволяет охватить достаточно широкий класс рассматриваемых систем и автоматизировать проведение эксперимента. Однако, существующие генераторы не обладают достаточным функционалом для генерации недетерминированных конечных автоматов требуемого класса, что демонстрируется проведёнными в работе компьютерными экспериментами и приводит к необходимости разработать генератор недетерминированных конечных автоматов, чему и посвящена первая половина работы.
Вторая половина работы содержит результаты компьютерных экспериментов по оценке длины и вероятности существования адаптивных различающих последовательностей.
Таким образом, данная работа посвящена разработке генератора недетерминированных конечных автоматов с возможностью настройки количества недетерминированных переходов и проведению экспериментов по оценки длины и вероятности существования адаптивных различающих последовательностей.
Купить