ВВЕДЕНИЕ 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], что позволяет охватить достаточно широкий класс рассматриваемых систем и автоматизировать проведение эксперимента. Однако, существующие генераторы не обладают достаточным функционалом для генерации недетерминированных конечных автоматов требуемого класса, что демонстрируется проведёнными в работе компьютерными экспериментами и приводит к необходимости разработать генератор недетерминированных конечных автоматов, чему и посвящена первая половина работы.
Вторая половина работы содержит результаты компьютерных экспериментов по оценке длины и вероятности существования адаптивных различающих последовательностей.
Таким образом, данная работа посвящена разработке генератора недетерминированных конечных автоматов с возможностью настройки количества недетерминированных переходов и проведению экспериментов по оценки длины и вероятности существования адаптивных различающих последовательностей.
В работе было проведено экспериментальное исследование длины и вероятности существования адаптивных различающих последовательностей и получены следующие результаты.
1. Разработано программное обеспечение для генерации недетерминированных конечных автоматов с заданной степенью недетерминизма.
2. Показано, что для недетерминированных автоматов с небольшим (не более 10) числом состояний адаптивные различающие последовательности могут быть построены при степени недетерминизма достигающей значения 6, в то время как длина таких последовательностей не достигает экспоненциальной оценки.
3. Увеличение числа выходных символов приводит к значительному росту вероятности существования и уменьшению длины адаптивных различающих последовательностей, однако точная оценка характера таких зависимостей требует дальнейших исследований.
Проведенные эксперименты позволяют оценить возможность и эффективность использования адаптивных различающих последовательностей при тестировании телекоммуникационных систем с недетерминизмом в неформальных описаниях. Однако, подбор оптимального значения степени недетерминизма между опциональностью и сложностью синтеза тестов для автоматов различных классов требует дальнейших исследований.
1. Lee, D., Yannakakis, M. (1996) Principles and methods of testing finite state machines-a survey. Proceedings of the IEEE. 84(8) (1996) 1090-1123.
2. Rita Dorofeeva, Khaled El-Fakih, Stephane Maag, Ana R. Cavalli, Nina Yevtushenko FSM-based conformance testing methods: A survey an-notated with experimental evaluation // Information and Software Technology, 2010, 52, pp. 1286-1297.
3. N. Kushik, J. Lopez, A. Cavalli, N. Yevtushenko: Improving Protocol Passive Testing through "Gedanken" Experiments with Finite State Machines. In Proceedings of QRS 2016. Pp. 315-322 (2016)
4. Бурдонов И. Б. Теория соответствия для систем с блокировками и разрушениями / И.Б. Бурдонов, А.С. Косачев, В.В. Кулямин. - М. : ФИЗМАТЛИТ. - 2008. - 412 с.
5. Petrenko A. and Yevtushenko N. Conformance Tests as Checking Experiments for Partial Nondeterministic FSM. In Proceedings of the 5th International Workshop on Formal Approaches to Testing of Software (FATES 2005), LNCS 3997, 2005, pp. 118-133.
6. Гилл А. Введение в теорию конечных автоматов / А. Гилл. - М.: Издательство Наука, 1966. - 272 с.
7. Агибалов Г. П. Лекции по теории конечных автоматов. / Г. П. Агибалов, А. М. Оранов. - Томск : Издательство ТГУ, 1984. - 185 с.
8. El-Fakih K., Yevtushenko N., Kushik N. Adaptive distinguishing test cases of nondeterministic finite state machines: test case derivation and length estimation. Formal Aspects of Computing vol. 30, issue 2, 2018, pp. 319-332
9. Aleksandr Tvardovskii. Refining the Specification FSM When Deriving Test Suites w.r.t. the Reduction Relation //Lecture Notes in Computer Science. 2017. Vol. 10533. P. 333-339.
10. Твардовский А.С., Евтушенко Н.В. К синтезу адаптивных различающих последовательностей для конечных автоматов. Труды ИСП РАН, том 30, вып. 4, 2018 г., стр. 139-154.
11. Ambiguity of Uppercase vs Lowercase in RFC 2119 Key Words/ S. Bradner, 1997, URL: https://tools.ietf.org/html/bcp14(дата обращения: 07.06.2020)
12. Key words for use in RFCs to Indicate Requirement Levels/ S. Bradner, 1997, URL:https://tools.ietf.org/html/rfc2119(дата обращения: 07.06.2020)
13. Ambiguity of Uppercase vs Lowercase in RFC 2119 Key Words/ B. Leiba, May 2017, URL:https://tools.ietf.org/html/rfc8174(дата обращения: 07.06.2020)
14. Petrenko A. Adaptive Testing of Deterministic Implementations Specified by Nondeterministic FSMs / A. Petrenko, N. Yevtushenko // Proceedings of ICTSS / Lecture Notes in Computer Science. - Vol. 7019. - 2011. - P. 162-178.
15. Lee D. Testing finite-state machines: state identification and verification / D. Lee, M. Yannakakis // IEEE Transactions on Computers. - 1994. - Vol. 43. - Issue 3. - P. 306-320.].
16. Shabaldina N. FSMTest-1.0: a manual for researches / N. Shabaldina, M. Gromov // Proceedings of the 13th Intern symposium on IEEE EAST-WEST DESIGN & TEST SYMPOSIUM (EWDTS’15). - 2015. - P. 216-219.
17. Pierre-Cyrille Heam On the Uniform Random Generation of NonDeterministic Automata Up to Isomorphism / Pierre-Cyrille Heam, Jean-Luc Joly// Implementation and Application of Automata. - 2015. - P. 140-152.
18. Hartmanis J. Algebraic structure theory of sequential machines / J. Hartmanis, R. Stearns. - Prentice-Hall, New York, 1966. - 210 p.
19. Страуструп Б. Язык программирования C++ / Б. Страуструп. - М.: Радио и связь 1991. - 349 с.