Методы синтеза проверяющих тестов с гарантированной полнотой для контроля дискретных управляющих систем на основе временных автоматов тема диссертации и автореферата по ВАК РФ 05.13.01, кандидат технических наук Жигулин, Максим Владимирович

• Жигулин, Максим Владимирович
• кандидат технических наук
• 2012

Оглавление диссертации кандидат технических наук Жигулин, Максим Владимирович

Введение

1. Основные понятия и краткий обзор литературы

1.1. Конечные автоматы

1.2. Конечные автоматы с временными задержками

1.3. Отношения между временными автоматами

1.4. Модели неисправности и проверяющие тесты с гарантированной полнотой

1.4.1. Полные проверяющие тесты

1.4.2. Построение теста перечислением неисправностей

1.4.3. Модель «черного ящика» для классических конечных автоматов

1.4.4. Синтез проверяющего теста для конечного автомата на основе обхода графа переходов

1.4.5. Модель «серого ящика» (мутационный автомат) для классических конечных автоматов

1.5. Синтез полных проверяющих тестов для временных автоматов

1.5.1. Автоматная модель Алюра и Дилла

1.5.2. Автоматная модель с задержками на переходах и выходах

1.6. Выводы по главе

2. Построение проверяющих тестов для временных автоматов на основе классического конечного автомата

2.1. Построение соответствующего конечного автомата

2.1.1. Метод построения конечного автомата для удаления переходов по задержке

2.1.2. Соответствие между временным автоматом и построенным конечным автоматом

2.2. Построение проверяющих тестов для временного автомата на основе соответствующего конечного автомата

2.2.1. Алгоритм построения проверяющего теста на основе соответствующего конечного автомата

2.2.2. Построение проверяющих тестов на основе явного перечисления неисправностей

2.2.3. Построение полных проверяющих тестов относительно выходных неисправностей

2.2.4. Построение проверяющих тестов для проверки переходов временного автомата

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

2.3.1. Временной автомат, описывающий поведение протокола ТРТР, и построение проверяющего теста по временному автомату

2.3.2. Экспериментальные результаты

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

2.5. Результаты главы

3. Метод синтеза проверяющих тестов для временных автоматов относительно модели «черного ящика»

3.1. Модель «черного ящика» для временных автоматов

3.2. Необходимые и достаточные условия эквивалентности временных автоматов

3.3. Синтез полного проверяющего теста для временных автоматов относительно модели «черного ящика»

3.3.1. Множества различимости и достижимости для временного автомата

3.3.2. Построение проверяющего теста при т-п

3.3.3. Построение полного проверяющего теста при т > п

3.4. Оценка сложности проверяющих тестов относительно модели «черного ящика»

3.5. Экспериментальные результаты построения полных проверяющих тестов относительно модели «черного ящика»

3.6. Результаты главы

4. Адаптация метода синтеза тестов для различных моделей неисправности

4.1. Построение проверяющего теста для временных автоматов с фиксированным набором задержек

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

4.3. Отношения между временными автоматами в зависимости от времени обработки входных воздействий

4.4. Синтез тестов для проверки времени обработки входных воздействий

4.5. Результаты главы

Введение диссертации (часть автореферата) на тему «Методы синтеза проверяющих тестов с гарантированной полнотой для контроля дискретных управляющих систем на основе временных автоматов»

Актуальность проблемы. Тестирование является неотъемлемой частью жизненного цикла любой управляющей системы. Цена ошибки в таких системах резко возрастает по мере нарастания сложности и важности решаемых задач, и существенный прогресс в области тестирования таких систем связывается с развитием формальных методов [18, 20, 30, 32, 35, 45]. При синтезе проверяющих и диагностических тестов для дискретных управляющих систем широко используются конечно-автоматные модели [см. например, 10, 59, 60, 62, 79, 81], методы синтеза тестов с гарантированной полнотой для которых хорошо известны. Однако классические автоматные модели явно не описывают временные аспекты поведения системы, такие как таймауты для ожидания подтверждения, допустимую задержку выходного отклика на поданное входное воздействие и т.п. Поэтому в настоящее время активно исследуется вопрос о построении тестов с гарантированной полнотой на основе временных полуавтоматов и автоматов [24, 29, 31, 39, 41, 43, 44, 47, 49, 50, 53, 58, 66, 67, 72, 77, 82, 84]. Однако практически все известные методы синтеза тестов для временных автоматов доставляют конечные проверяющие тесты, полнота которых остается неизвестной, и, соответственно, синтез конечных проверяющих тестов с гарантированной полнотой для систем с явно выраженными временными аспектами требует дополнительных исследований. Достаточно выразительной моделью является конечный автомат с таймаутами, и, таким образом, разработка методов синтеза проверяющих тестов с гарантированной полнотой для таких временных автоматов является актуальной задачей.

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

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

Научная новизна работы состоит в следующем.

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

Исследовано отношение эквивалентности между детерминированными временными автоматами и установлены необходимые и достаточные условия эквивалентности временных автоматов с таймаутами на основе соответствия между множествами их состояний.

Для понижения избыточности тестов относительно модели «черного ящика» методы построения полного проверяющего теста для конечного автомата адаптированы для построения тестов непосредственно по временному автомату.

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

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

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

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

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

Реализация полученных результатов. Исследования, результаты которых изложены в диссертации, проводились в рамках следующих проектов:

1. НИР «Разработка математических и программных средств обеспечения надежного и безопасного доступа к электронным ресурсам коллективного пользования» (в рамках инновационного проекта ТГУ), 2006-2007 гг.

2. НИР «Проведение прикладных и проблемно-ориентированных поисковых исследований в области информационно-телекоммуникационных систем с участием научных организаций Франции» (шифр заявки «2009-04-1.400-02-003»), госконтракт №02.514.12.4002 от 09.06.2009г.

Апробация работы. Все теоретические и практические результаты, составившие основу диссертационной работы, по мере их получения обсуждались на семинаре кафедры информационных технологий в исследовании дискретных структур радиофизического факультета ТГУ. Кроме того, результаты работы докладывались на научных конференциях: VI (VII, VIII) Российской конференции с международным участием «Новые информационные технологии в исследовании дискретных структур», с. Шушенское, 2006 г. (Томск, 2008 г. и 2010 г.); Российской конференции «VI Всесибирский конгресс женщин-математиков», Красноярск, 2010 г.; Международной научно-практической конференции «Актуальные проблемы радиофизики», Томск, 2010 г.; Международной конференции по качеству программного обеспечения, QSIC'2011, Мадрид, Испания, 2011 г.

По результатам проведенных исследований опубликовано 9 статей в научных журналах, докладах и материалах конференций различного уровня, в том числе четыре в рецензируемых журналах из перечня ВАК:

Жигулин М.В. Преобразование спецификации при пассивном тестировании телекоммуникационных протоколов / М.В. Жигулин, С.А. Прокопенко, Н.В. Евтушенко // Вестник Томского государственного университета. Приложение. Доклады VI Всероссийской конференции с международным участием "Новые информационные технологии в исследовании сложных структур". - Томск, 2006. - № 18. - С. 62-66.

Жигулин М.В. Оценка полноты проверки при пассивном тестировании на основе автоматной модели // Новые информационные технологии в исследовании сложных структур: тезисы докладов седьмой Российской конференции с международным участием. - Томск, 2008. - С. 48.

Жигулин М.В. Оценка полноты проверки при пассивном тестировании на основе автоматной модели / М.В. Жигулин, А.В. Коломеец // Известия Томского политехнического университета. — 2009. - Т. 314, № 5. - С. 225-228.

Жигулин М.В. Необходимое и достаточное условие /-эквивалентности временных автоматов / М.В. Жигулин, И.М. Дмитриев // VI Всесибирский конгресс женщин-математиков: материалы Всероссийской конференции. -Красноярск, 2010. - С. 137-141.

Жигулин М.В. Синтез тестов с гарантированной полнотой для временных автоматов / М.В. Жигулин, И.М. Дмитриев, Н.В. Евтушенко // Известия Томского политехнического университета. — 2010. - Т. 316, № 5. — С. 104-110.

Жигулин М.В. Алгоритм синтеза проверяющего теста с гарантированной полнотой для конечных временных автоматов с фиксированным набором задержек для модели «черного ящика» / М.В. Жигулин, И.М. Дмитриев, Д.Д. Попов // Новые информационные технологии в исследовании сложных структур: тезисы докладов восьмой Российской конференции с международным участием. - Томск, 2010. - С. 50.

Дмитриев И.М. Синтез проверяющих тестов с гарантированной полнотой для временных автоматов с конечными задержками / И.М.Дмитриев, М.В. Жигулин II Известия высших учебных заведений: Физика. - Томск, 2010. - Т. 53, № 9/3. - С. 196-198.

М.В. Жигулин Тестирование программной реализации протокола IRC на основе модели расширенного автомата / М.В. Жигулин, A.B. Коломеец, Н.Г. Кушик, A.B. Шабалдин // Известия Томского политехнического университета. - Томск, 2011. - Т. 318, № 5. - С. 81-84.

Zhigulin М. FSM-Based Test Derivation Strategies for Systems with TimeOuts / M. Zhigulin, N. Yevtushenko, S. Maag, A. Cavalli // 11th International conference on quality software - Madrid, 2011. - P. 141-150.

Структура и объем работы. Диссертация состоит из введения, 4 глав, заключения и списка используемой литературы. Диссертация содержит 13 рисунков. Объем диссертации составляет 121 страница, в том числе: титульный

Заключение диссертации по теме «Системный анализ, управление и обработка информации (по отраслям)», Жигулин, Максим Владимирович

ЗАКЛЮЧЕНИЕ

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

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

2. Установлены необходимые и достаточные условия эквивалентности двух временных автоматов на основе соответствия между конечными множествами их состояний. Данное соответствие позволяет адаптировать методы построения проверяющих тестов относительно модели «черного ящика» из классической теории автоматов для построения проверяющего теста непосредственно по модели временного автомата, поскольку тесты, построенные по соответствующему классическому конечному автомату, обладают значительной избыточностью.

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

Отметим, что длину полного проверяющего теста, построенного по одному из алгоритмов, предложенных в главе 3, можно уменьшить как за счет применения более эффективных методов использования различающих последовательностей, как это делается в HSI, Н и SPY методах для классических конечных автоматов, так и за счет сокращения области неисправности как предлагается в главе 4.

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

Список литературы диссертационного исследования кандидат технических наук Жигулин, Максим Владимирович, 2012 год

1. Бурдонов И.Б. Использование конечных автоматов для тестирования программ / И.Б. Бурдонов, A.C. Косачев, В.В. Кулямин // Программирование. - 2000. - №2. - С. 12-28.

2. Василевский М.П. О распознавании неисправности автоматов // Кибернетика. 1973. - № 4. - С. 93-108.

3. Гилл А. Введение в теорию конечных автоматов / А. Гилл; под ред. П.П. Пархоменко. М.: Наука, 1966. - 272 с.

4. Громов M.JI. Разработка методов синтеза условных тестов для автоматных моделей с недетерминированным поведением: дис. на соискание ученой степени канд. физ.-мат. наук / M.J1. Громов. Томск, 2009. - 154 с.

5. Громов M.J1. Синтез условных различающих экспериментов для автоматов с недетерминированным поведением / M.JI. Громов, Н.В. Евтушенко // Прикладная дискретная математика. Томск, 2009. - № 4(6). - С. 90-101.

6. Громов M.JI. Синтез различающих экспериментов для временных автоматов / M.JI. Громов, Н.В. Евтушенко. // Программирование. 2010. -№ 4. - С. 40-50.

7. Дорофеева М.Ю. Исследование и разработка конечно-автоматных методов синтеза проверяющих тестов для управляющих систем: дис. на соискание ученой степени канд. тех. наук / Дорофеева М.Ю. Томск, 2007. - 145 с.

8. Дмитриев И.М. Синтез проверяющих тестов с гарантированной полнотой для временных автоматов с конечными задержками / И.М. Дмитриев, М.В.Жигулин // Известия высших учебных заведений: Физика. 2010. -Т. 53, № 9/3 - С. 196-198.

9. Евтушенко Н.В. Метод построения эксперимента для произвольного детерминированного автомата / Н.В. Евтушенко, А.Ф. Петренко // Автоматика и вычислительная техника. 1990. - № 5. - С. 73-76.

10. Ю.Евтушенко Н.В. Недетерминированные автоматы: анализ и синтез. 4.1. Отношения и операции: учеб. пособие / Н.В. Евтушенко, А.Ф. Петренко, М.В. Ветрова. Томск: Томский государственный университет, 2006. -142 с.

11. Жигулин М.В. Оценка полноты проверки при пассивном тестировании на основе автоматной модели / М.В. Жигулин, А.В. Коломеец // Известия Томского политехнического университета. 2009. - Т. 314, № 5. - С. 225228.

12. Жигулин М.В. Необходимое и достаточное условие /-эквивалентности временных автоматов / М.В. Жигулин, И.М. Дмитриев // VI Всесибирский конгресс женщин-математиков: материалы Всероссийской конференции. -Красноярск, 2010.-С. 137-141.

13. Жигулин М.В. Синтез тестов с гарантированной полнотой для временных автоматов / М.В. Жигулин, И.М. Дмитриев, Н.В. Евтушенко // Известия Томского политехнического университета. 2010. - Т. 316, № 5. - С. 104110.

14. Жигулин М.В. Алгоритм синтеза проверяющего теста с гарантированной полнотой для конечных временных автоматов с фиксированным набором задержек для модели «черного ящика» / М.В. Жигулин, И.М. Дмитриев,

15. Д.Д. Попов // Новые информационные технологии в исследовании сложнь1х структур: тезисы докладов восьмой Российской конференции с международным участием. Томск, 2010. - С. 50.

16. Жигулин М.В. Тестирование программной реализации протокола IRC на основе модели расширенного автомата / М.В. Жигулин, A.B. Коломеец, Н.Г. Кушик, A.B. Шабалдин // Известия Томского политехнического университета. 2011. - Т. 318, № 5 - С. 81 -84.

17. Карибский В.В. Основы технической диагностики / В.В. Карибский, П.П. Пархоменко, Е.С. Согомонян, В.Ф. Халчев -М.: Энергия, 1976. 464 с.

18. Куфарева И.Б. Применение недетерминированных автоматов в задачах синтеза проверяющих тестов в системах логического проектирования: дис. на соискание ученой степени канд. тех. наук / И.Б. Куфарева. Томск, 2000. - 168 с.

19. Матросова А.Ю. Алгоритмические методы синтеза тестов. Томск: Изд-во Томского госуниверситета, 1990. - 207 с.

20. Мур Э. Умозрительные эксперименты с последовательными машинами. / Э. Мур, Автоматы. Сб. статей под ред. К. Шеннона, Д. Маккарти. М.: Изд-во иностр. лит, 1956. - С. 179-213.

21. Трахтенброт Б.А. Конечные автоматы. Поведение и синтез / Б.А. Трахтенброт, Я.М. Барздинь. М.: Наука, 1970. - 396 с.

22. Adjar N. Testing real-time systems using TINA / N. Adjar, P. De Saqui-Sannes, К. M. Rahmouni // Testing of software and communication systems. Lecture notes in computer science. 2009. - Vol. 5826. - P. 1-15.

23. Advanced TFTP Электронный ресурс. Электрон, текст, дан. - Geeknet, 2011. - URL: http://freecode.com/projects/atftp (дата обращения: 06.09.2011).

24. Alur R. A theory of timed automata / R. Alur, D.L. Dill // Theoretical computer science.-1994.-Vol. 126, No. 2.-P. 183-235.

25. Alur R. Automata-theoretic verification of real-time systems / R. Alur, D.L. Dill // In formal methods for real-time computing, trends in software series. 1996. -P. 55-82.

26. Apache commons net Электронный ресурс. Электрон, текст, дан. - The Apache software foundation, 2001-2011. - URL: http://commons.apache.org/net (дата обращения: 06.09.2011).

27. Baumgarten В. Timed systems behaviour and conformance testing a mathematical framework / B. Baumgarten // International federation for information processing. - 1996. - P. 89-104.

28. Bochmann G.V. Protocol testing: review of methods and relevance for software testing / G. von Bochmann, A. Petrenko. // Proceedings of the international symposium on software testing and analysis. Washington, USA, 1994. - P. 109124.

29. Bosnacki D. Integrating real time into SPIN: a prototype implementation / D. Bosnacki, D. Dams // Proceeding of formal description techniques and protocol specification, testing and verification. Netherlands, 1998. - P. 423-439.

30. Brinksma E. Testing transition systems: an annotated bibliography / E. Brinksma, J. Tretmans // Modeling and verification of parallel processes. Lecture notes in computer science. 2001. - Vol. 2067 - P. 187-195.

31. Cao T.-D. Testing of web services: tools and experiments / T.-D. Cao, R. Castanet, P. Felix, G. Morales // IEEE Asia Pacific services computing conference. - Jeju, Korea, 2011. - P. 78-85.

32. Cardell-Oliver R. A practical and complete algorithm for testing real-time systems / R. Cardell-Oliver, T. Glover // Formal techniques for real-time fault tolerant systems. Denmark, 1998. - P. 251-261.

33. Chen W.H. Executable test sequences for the protocol data flow property // Proceedings of the 21st International conference on formal techniques for networked and distributed systems. 2001. - P. 285-299.

34. Chow T.S. Test software design modeled by finite state machine // IEEE Transactions on software engineering. 1978. - Vol. SE-4(3). - P. 178-187.

35. Dorofeeva M. Experimental evaluation of FSM-based testing methods / M. Dorofeeva, K. El-Fakih, A.R. Cavalli, N. Yevtushenko // IEEE International conference on software engineering and formal methods. 2005. - P. 23-32.

36. Dorofeeva M. FSM-based conformance testing methods: A survey annotated with experimental evaluation / M. Dorofeeva, K. El-Fakih, S. Maag, A.R. Cavalli, N. Yevtushenko // Information and software technology. 2010. - Vol. 52(12). -P. 1286-1297.

37. El-Fakih K. Fault diagnosis in extended finite state machines / K. El-Fakih, S. Prokopenko, N. Yevtushenko, G. Bochmann // Testing of communicating systems. Lecture notes in computer science. 2003 - Vol. 2644. - P. 197-210.

38. El-Fakih K. FSM-based incremental conformance testing methods / K. El-Fakih, N. Yevtushenko, G. von Bochmann // IEEE Transactions on software engineering. 2004. - Vol. 30(7). - P. 425-436.

39. El-Fakih K. Testing timed finite state machines with guaranteed fault coverage / K. El-Fakih, N. Yevtushenko, H. Fouchal // Formal techniques for networked and distributed systems. Lecture notes in computer science. 2009. - Vol. 5826. -P. 66-80.

40. En-Nouaary A. Timed test cases generation based on state characterization technique / A. En-Nouaary, R. Dssouli, F. Khendek, A. Elqortobi // Proceedings of the real-time systems symposium. 1998. - P. 220-229.

41. En-Nouaary A. Timed Wp-method: testing real-time systems / A. En-Nouaary, R. Dssouli, F. Khendek // In proceedings of IEEE Trans, software eng. -Vol. 28(11).-2002.-P. 1023-1038.

42. En-Nouaary A. A guided method for testing timed input output automata / A. En-Nouaary, R. Dssouli // Testing of communicating systems. Lecture notes in computer science. 2003. - Vol. 2644. - P. 211-224.

43. Favreau J.P. Automatic generation of test scenario skeletons from protocol specifications written in ESTELLE / J.P. Favreau, R.J. Linn // Proceedings of the protocol specification, testing, and verification, VI. North-Holland, 1986. -P. 191-202.

44. Fujiwara S. Test selection based on finite state models / S. Fujiwara, G. von Bochmann, F. Khendek, M. Amalou, A. Ghedamsi // IEEE Transactions. 1991. -Vol. SE-17, No. 6.-P. 591-603.

45. Gomez R. Discrete timed automata and MONA: description, specification and verification of a multimedia stream / R. Gomez, H. Bowman // Formal techniques for networked and distributed systems Berlin, Germany, 2003. - P. 177-192.

46. Gonenc G. A method for the design of fault detection experiments // IEEE Trans, computers. 1970. - Vol. C-19, No. 6. - P. 551-558.

47. Gromov M. Deriving test suites for timed finite state machines / M. Gromov, D. Popov, N. Yevtushenko // Proceedings of IEEE East-west design & test symposium. 2008. - P. 339-343.

48. Hartmanis J. Algebraic structure theory of sequential machines / J. Hartmanis, R. Stearns. New York: Prentice-Hall, 1966. - 210 p.

49. Hennie F.C. Fault detecting experiments for sequential circuits // Proceedings of the 5th Annual symposium on switching circuit theory and logical design. 1964. -P. 95-110.

50. Hierons R.M Testing from a stochastic timed system with a fault model / R.M. Hierons, M.G. Merayo, M. Nunez // Journal of logic and algebraic programming. 2009. - Vol. 72(8). - 98-115.

51. Kam T. Synthesis of finite state machines: functional optimization / T. Kam and etc.. Boston, MA, USA: Kluwer Academic Publishers, 1997 - 282 p.

52. Khoumsi A. Test cases generation for nondeterministic real-time systems / A. Khoumsi, T. Jeron, H. Marchand // Formal approaches to software testing. -2003.-Vol. 2931.-P. 131-146.

53. Koufareva I. Test generation driven by user-defined fault models / I. Koufareva, A. Petrenko, N. Yevtushenko. // Testing of communicating systems: methods and applications. Hungary, 1999. - P. 215-223.

54. Krichen M. Conformance testing for real-time systems / M. Krichen, S. Tripakis // Formal methods in system design. 2009. - Vol. 34, No. 3. - P 238-304.

55. Laroussinie F. CMC: a tool for compositional model-checking of real-time systems / F. Laroussinie, K. Larsen // Formal description techniques and protocol specification, testing and verification. 1998. - P. 439-456.

56. Lee D. Conformance testing of protocols specified as communicating finite state machines a guided random walk based approach / D. Lee, K.K. Sabnani, D.M. Kristol, S. Paul // IEEE Transactions on communications. - 1996. -Vol. 44(5). - P. 631-640.

57. Lee D. Principles and methods of testing finite state machines a survey / D. Lee, M. Yannakakis // Proceedings of the IEEE. - 1996. - Vol. 84(8). - P. 1090-1123.

58. Lynch N. An introduction to input/output automata / N. Lynch, M. Tuttle // CWI Quarterly. 1989. - Vol. 2. - P. 219-246.

59. Lynch N. Hybrid i/o automata. Hybrid systems III. / N. Lynch, R. Segala,

60. F. Vaandrager, H.B. Weinberg // Lecture notes in computer science 1996. -Vol. 1066.-P. 496-510.

61. Mammar A. A systematic approach to integrate common timed security rules within a TEFSM-based system specification / A. Mammar, W. Mallouli, A. Cavali // Information and software technology. 2012. - Vol. 54(1). - P. 8798.

62. Mattiello-Francisco F. InRob: An approach for testing interoperability and robustness of real-time embedded software / F. Mattiello-Francisco, E. Martins, A. Cavalli, E.T. Yano // Journal of systems and software. 2012. - Vol. 85. -P. 3-5.

63. Morales G. Timed extended invariants for the passive testing of web services /

64. G. Morales, S. Maag, A. Cavalli, W. Mallouli, E.M. de Oca, B. Wehbi // IEEE International conference on web services. 2010. - P. 592-99.

65. Merayo M.G. Extending EFSMs to specify and test timed systems with action durations and time-outs / M.G. Merayo, M. Nunez, I. Rodriguez // IEEE Transactions on computers. 2008. - Vol. 57(6). - P. 835-844.

66. Merayo M.G. Formal testing from timed finite state machines / M.G. Merayo, M. Nunez, I. Rodriguez // Computer networks. 2008. - Vol. 52(2). - P. 432460.

67. Petrenko A. Test suite generation for a given type of implementation errors /tV\

68. A. Petrenko, N. Yevtushenko // Proceedings of IFIP 12 International conference on protocol specification, testing and verification. 1992. - P. 229-243.

69. Petrenko A. Fault models for testing in context / A. Petrenko, N. Yevtushenko, G. von Bochmann // Formal techniques for networked and distributed systems. -1996.-P. 163-178.

70. Poage J.F. Derivation of optimal test sequences for sequential machines /th

71. J.F.Poage, E.J. McCluskey Jr. // Proceedings of the IEEE 5 Symposium on switching circuits theory and logical design. 1964. - P. 121-132.

72. Ru Dai Z. Timed TTCN-3 A real time extension for TTCN-3 / Z. Ru Dai, J. Grabowski, H. Nuekirchen // Testing of communicating systems XIV. - 2002. -P. 407-425.

73. Sabnani K. A protocol test generation procedure / K. Sabnani, A. Dahbura // Computer networks and ISDN systems. 1988. - Vol. 15, No. 4. - P. 285-297.

74. Simao A. Generating reduced tests for FSMs with extra states / A. Simao, A. Petrenko, N. Yevtushenko // Lecture notes in computer science. 2009. -Vol. 5826-P. 129-145.

75. Sollins K. RFC 1350 The TFTP protocol (revision 2) Электронный ресурс. // Internet FAQ archives : online education. - Электрон, текст, дан. - URL: http://www.faqs.org/rfcs/rfcl350.html (дата обращения: 04.09.2011).

76. Springintveld J. Testing timed automata / J. Springintveld, F. Vaandrager, P. D'Argenio // Theoretical computer science. 2001. - Vol. 254 - P. 225-257.

77. Starke P.H. Abstract automata / P.H. Starke North-Holland: American Elsevier, 1972.-419 p.

78. Tan Q.M. Test generation for specifications vodeled by input/output automata / Q.M. Tan, A. Petrenko // The Proceedings of the IFIP 11th International workshop on testing of communicating systems. Deventer, Netherlands, 1998. - P. 83100.

79. Tretmans J. Test generation with inputs, outputs and quiescence // Proceedings of the 2nd International workshop on tools and algorithms for construction and analysis of systems. London, UK, 1996. - P. 127-146.

80. Tretmans J. Model based testing with labelled transition systems // Formal methods and testing. Lecture notes in computer science. 2008. - Vol. 4949 -P. 1-38.

81. Tripakis S. Folk theorems on the determinization and minimization of timed automata // Formal modeling and analysis of timed systems. Lecture notes in computer science. 2004. - Vol. 2791. - P. 182-188.

82. Vuong S.T. The UlOv-method for protocol test sequence generation / S.T. Vuong, W.W. L. Chan, M.R. Ito // Proceedings of the 2nd IFIP International workshop on protocol test systems. 1989. - P. 161-175.

83. Walter T. Real-time TTCN for testing real-time and multimedia systems / T. Walter, J. Grabowski // The proceedings of the International workshop on testing of communicating systems. 1997. - Vol. 6. - P. 37-56.

84. Zhigulin M. FSM-Based Test Derivation Strategies for Systems with Time-Outs / M. Zhigulin, N. Yevtushenko, S. Maag, A. Cavalli // 11th International conference on quality software. Madrid, 2011. - P. 141-150.