Автоматизация тестирования соответствия для телекоммуникационных протоколов

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

тестирование соответствия, UniTESK, формальные методы, автоматизация тестирования, тестирование, основанное на моделях, тестирование протоколов, формальные спецификации, моделирование протоколов

1. CCITT Recommendation Z.100. Specification and Description Language (SDL). Geneve, Switzerland: ITU, 1993. 245 с.

2. ISO/IEC 9074. Information Processing Systems — Open Systems Interconnection. Estelle — A Formal Description Technique based on an Extended State Transition Model. Geneve, Switzerland: ISO, 1989 1 я редакция,1997 2-я редакция. Отозван 06.05.1999.

3. ISO/IEC 8807. Information Processing Systems — Open Systems Interconnection. LOTOS — A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour. Geneve, Switzerland: ISO, 1989. 142 с.

4. ITU-T X.680 (11/08) Information technology - Abstract Syntax Notation One (ASN.1): Specification of basic notation. ITU-T, 2008. 194 c.

5. OMG Unified Modeling LanguageTM (OMG UML), Infrastructure. OMG, 2011. 230 c.

6. Кларк Э.М., Грамберг О., Пелед Д. Верификация моделей программ. // Изд-во Моск. центра непрерыв. мат. образования, 2002. 416 c.

7. Карпов Ю.Г. MODEL СHECKING. Верификация параллельных и распределенных программных систем. // БХВ-Петербург, 2010г. 560 с.

8. M. Diaz. Petri Nets: Fundamental Models, Verification and Applications. // Willey, 2013г. 656с.

9. Utting, M., Legeard, B.: Practical Model-Based Testing: A Tools Approach. Morgan Kaufmann, San Francisco (2007).

10. Blackburn, M., Busser, R., Nauman, A.: Why Model-Based Test Automation is Different and What You Should Know to Get Started. Software Productivity Consortium, NFP (2004).

11. Dalal, S.R., Jain, A., Karunanithi, N., Leaton, J.M., Lott, C.M., Patton, G.C., Horowitz, B.M.: Model-Based Testing in Practice. In: Proceedings of the ICSE 1999 (May 1999).

12. I. Bourdonov, A. Kossatchev, V. Kuliamin, A. Petrenko. UniTesK Test Suite Architecture. Proceedings of FME’2002, Kopenhagen, Denmark, LNCS 2391:77-88, Springer-Verlag, 2002.

13. В. В. Кулямин, А. К. Петренко, А. С. Косачев, И. Б. Бурдонов. Подход UniTesK к разработке тестов. Программирование, 29(6):25-43, 2003.

14. В. В. Кулямин, А. К. Петренко. Развитие подхода к разработке тестов UniTESK. Труды ИСП РАН, 24, 2014.

15. F. C. Hennie. Fault detecting experiments for sequential circuits. // Proc. 5-th Ann. Symp. Switching Circuit Theory and Logical Design, 1964. С. 95-110.

16. [Василевский] М. П. Василевский. Диагностика ошибок в автоматах. // Кибернетика и системный анализ, т. 9, № 4, 1973. С. 98-108.

17. T. S. Chow. Testing software design modeled by finite-state machines. // IEEE Trans. on Software Engineering, vol. 4, no. 3, 1978. С. 178-187.

18. J. A. Bergstra, J. W. Klop. Algebra of Communicating Processes with Absraction. Theoretical Computer Science, 37(1), 1985. С. 77-121.

19. C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985; электронное издание, 2004. 260 с. [PDF] (http://www.usingcsp.com/cspbook.pdf).

20. R. Milner. Communication and Concurrency. Prentice-Hall, 1989. 260 с.

21. N.A. Lynch, M.R. Tuttle, “An Introduction to Input/Output Automata” // CWI-Quaterly 3, 1989, P. 219-246. [PDF] http://www.markrtuttle.com/papers/lt89-cwi.pdf.

22. F. Maraninchi. Operational and compositional semantics of synchronous automaton compositions. // CONCUR'92 Proceedings, LNCS 630. Springer-Verlag, 1992. [PS] http://www-verimag.imag.fr/~maraninx/ArgosCONCUR92.ps.gz

23. ISO/IEC 7498. Information technology – Open Systems Interconnection – Basic Reference Model. Geneva, Switzerland: ISO, 1994.

24. Ed. Brinksma. A theory for the derivation of tests. Proc. IFIP WG6.1 8th Intl. Symp. on Protocol Specification, Testing, and Verification, North-Holland, S. Aggarwal and K. Sabnani Ed. pp. 63-74, 1988.

25. K. K. Sabnani and A. T. Dahbura. A protocol test generation procedure. Computer Networks and ISDN Systems, vol. 15, no. 4, pp. 285-297, 1988.

26. S. Fujiwara, G. v. Bochmann, F. Khendek, M. Amalou, and A. Ghedamsi. Test selection based on finite state models. IEEE Trans. on Software Eng., vol. 17, pp. 591-603,1991.

27. G. Luo, A. Petrenko, and G. v. Bochmann. Selecting test sequences for partially specified nondeterministic finite state machines, Proceedings of the IFIP Seventh International Workshop on Protocol Test Systems, Japan, 1994, pp. 95-110.

28. Н. В. Евтушенко, А. В. Лебедев, А. Ф. Петренко. Построение проверяющего множества для компоненты последовательной автоматной сети. Автоматика и телемеханика, № 8. стр. 145-153, 1994.

29. J. C. Fernandez, C. Jard, T. Jeron, C. Viho. Using on-the-Fly Verification Techniques for the Generation of Test Suites // Proceedings of the 8th International Conference on Computer Aided Verification, LNCS 1102, Springer-Verlag, 1996, P. 348-359.

30. J. Tretmans. Test Generation with Inputs, Outputs, and Repetitive Quiescence. Software — Concepts and Tools, 17(3):103-120, 1996.

31. D. P. Sidhu and T.-K. Leung. Formal methods for protocol testing: a detailed study. IEEE Trans. Soft. Eng., vol. 15, no. 4, pp. 413-426, 1989.

32. D. Lee, M. Yannakakis. Principles and methods of testing finite state machines — a survey. Proc. IEEE, 84(8):1090-1123, 1996.

33. G. v. Bochmann, A. Petrenko. Protocol Testing: Review of Methods and Relevance for Software Testing. Proc. of ACM SIGSOFT ISSTA'1994, Software Engineering Notes, Special Issue, pp. 109—124.

34. A. Petrenko. Fault Model-Driven Test Derivation from Finite State Models: Annotated Bibliography. In F. Cassez, C. Jard, B. Rozov, M. Dermot, eds. Modeling and Verification of Parallel Processes: 4-th Summer School, Nantes, France, LNCS 2067, pp. 196-200, Springer-Verlag, 2000.

35. ISO/IEC 9646. Information technology – Open Systems Interconnection – Conformance testing methodology and framework – Part 1: General concepts. Geneva: ISO, 1994. 46 с.

36. ITU-T Recommendation Z.500. Framework on formal methods in conformance testing. Geneve, Switzerland: ITU, 1997. 49 с.

37. Glenford J. Myers, Corey Sandler, Tom Badgett. The Art of Software Testing, 3rd Edition. Wiley, 2011. C. 240.

38. J. Tretmans, An Overview of OSI Conformance Testing. Translated and adapted from: J. Tretmans and J. van de Lagemaat, Conformance Testen, in Handboek Telematica, Vol. II, pages 1--19. Samson, 1991. [PDF] http://people.cs.aau.dk/~kgl/TOV03/iso9646.pdf

39. ISO/IEC 9646. Information technology – Open Systems Interconnection – Conformance testing methodology and framework – Part 2: Abstract Test Suite specification. Geneva: ISO, 1994. 33 с.

40. Information technology – Open systems interconnection – Conformance testing methodology and framework – Part 3: The Tree and Tabular Combined Notation (TTCN). 1-е издание. Geneva, Switzerland: ISO, 1992.

41. Information technology – Open systems interconnection – Conformance testing methodology and framework – Part 3: The Tree and Tabular Combined Notation (TTCN). 2-е издание. Geneva, Switzerland: ISO, 1998.

42. ETSI ES 201 873-1 V3.1.1. Methods for Testing and Specification (MTS); The Testing and Test Control Notation version 3; Part 1: TTCN-3 Core Language. Sophia-Antipolis, France: ETSI, 2005. 210 с.

43. OMG formal/05-07-07. UML Testing Profile. Version 1.0. Needham, USA: Open Management Group, 2005. [PDF, PostScript] (http://www.omg.org/cgi-bin/doc?formal/05-07-07).

44. L. Ebrecht, M. Schacher, C. Bühler. Test Specification in XML – the most important Element for Test Automation. // ARTiSAN Benutzerforum D.A.CH, 2005.

45. Программный комплекс для разработки тестов. [URL] http://www.junit.org.

46. Проект TAHI по разработке тестового набора для стека протоколов IPv6. [HTML] (http://www.tahi.org/).

47. Digital cellular telecommunications system (Phase 2+) (GSM); Handover procedures (GSM 03.09 version 5.1.0) // ETSI, Sophia-Antipolis, France, 1997. 81 c.

48. ETSI ETS 300 838. Integrated Services Digital Network (ISDN); Harmonized Programmable Communication Interface (HPCI) for ISDN. // ETSI, Sophia-Antipolis, France, 1998. 546 c.

49. C. Jard, T. Jéron. TGV: Theory, principles and algorithms. // International Journal on Software Tools for Technology Transfer (STTT), vol. 7(4). Berlin: Springer, 2005. С. 297 – 315

50. E. Farchi, A. Hartman, S.S. Pinter. Using a Model-based Test Generator to Test for Standard Conformance. // IBM System Journal - special issue on Software Testing. Volume 41(1), 2002. С. 89 - 110.

51. G. Friedman, A. Hartman, K. Nagin, T. Shiran. Projected State Machine Coverage for Software Testing. // Proceedings of ISSTA 2002 International Symposium on Software Testing and Analysis. New York, USA: ACM Press, 2002. С. 134 – 143.

52. Margus Veanes, Colin Campbell, Wolfgang Grieskamp, Wolfram Schulte, Nikolai Tillmann, and Lev Nachmanson, Model-Based Testing of Object-Oriented Reactive Systems with Spec Explorer, in Formal Methods and Testing, vol. 4949, pp. 39-76, Springer Verlag, 2008

53. A. Belinfante, J. Feenstra, R. de Vries, J. Tretmans, N. Goga, L. Feijs, S. Mauw, L. Heerink. Formal test automation: A simple experiment. // G. Csopaki, S. Dibuz, K. Tarnay, editors. 12th Int. Workshop on Testing of Communicating Systems. Budapest, Hungary: Kluwer Academic Publishers, 1999. С. 179-196.

54. Axel Belinfante. JTorX: a Tool for On-Line Model-Driven Test Derivation and Execution. In: Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2010. LNCS vol. 6015, pp. 266-270. Springer.

55. N. Goga. A probabilistic coverage for on-the-fly test generation algorithms. // Automated Verification of Critical Systems (AVoCS '03), 2003.

56. Н.В. Пакулин, А.В. Хорошилов. Разработка формальных моделей и тестирование соответствия для систем с асинхронными интерфейсами и телекоммуникационных протоколов. // Журнал "Программирование" № 5, 2007 г., ISSN 0132-3474, с. 1-29.

57. V. V. Kuliamin, A. K. Petrenko, N. V. Pakoulin, A. S. Kossatchev, I. B. Bourdonov. Integration of Functional and Timed Testing of Real-time and Concurrent Systems. // Proceedings of the 5-th International Conference on Perspectives of System Informatics, July 9-12, 2003, Novosibirsk, Russia; LNCS 2890, Springer, 2003, pp. 450-461.

58. V. V. Kuliamin, A. K. Petrenko, N. V. Pakoulin. Practical Approach to Specification and Conformance Testing of Distributed Network Applications. // Proceedings of the 2-nd International Service Availability Symposium, April 25-26, 2005, Berlin, Germany; LNCS 3694, Springer, 2005, pp. 68-83.

59. V. V. Kuliamin, A. K. Petrenko, N. V. Pakoulin. Extended Design-by-Contract Approach to Specification and Conformance Testing of Distributed Software. // Proceedings of the 9-th World Multiconference on Systemics, Cybernetics, and Informatics, Model Based Development and Testing Workshop, July 10-13, 2005, Orlando, Florida, USA, pp. 65-70

60. C. A. R. Hoare. An axiomatic basis for computer programming. // Communications of the ACM, volume 12 №10, 1969. С. 576-580.

61. R. P. Draves, A. Mankin, B. D. Zill. Implementing IPv6 for Windows NT. Proceedings of the 2nd USENIX Windows NT Symposium, Seattle, WA, August 3–4, 1998

62. Агамирзян И., Грошев С.Г., Хорошилов А.В., Ключников Г.В., Косачев А.С., Омельченко В.А., Пакулин Н.В., Петренко А.К., Шнитман В.З. Применение формальных методов для тестирования MSR IPv6. // Интернет нового поколения. Сборник тезисов международной конференции. Ярославль, 2002. С. 29-33.

63. Ключников Г.В., Косачев А.К., Пакулин Н.В., Петренко А.К., Шнитман В.З. Применение формальных методов для тестирования реализации IPv6. // Труды ИСП РАН, Том 4. М., 2003. С. 121-140.

64. Ключников Г.В., Косачев А.С., Пакулин Н.В., Петренко А.К., Шнитман В.З. Применение формальных методов для тестирования Mobile IPv6. // Интернет нового поколения. Сборник тезисов II международной конференции. Ярославль, 2003. С. 20-25.

65. Зацепин Д.В., Шнитман В.З. Особенности применения технологии UniTESK для тестирования функций мобильности в протоколе IPv6. // Труды ИСП РАН 13 (1). М. , 2007. С. 143-170

66. CTesK 2.1: SeC Language Reference. М.: ИСП РАН, 2005. 167 с.

67. Ключников Г.В., Пакулин Н.В., Шнитман В.З. Автоматизированное тестирование сетевых сервисов Интернет-протокола // Труды Всероссийской научной конференции «Научный сервис в сети ИНТЕРНЕТ: технологии распределенных вычислений», г. Новороссийск, 19-24 сентября 2005 г. С. 168-170.

68. Н.В. Пакулин "Применение формальных методов для тестирования реализаций сложных современных протоколов", Сборник трудов международного семинара "Go4IT - шаг к новым технологиям Интернета", ИСП РАН, М., 2007 г., с. 11-18.

69. А.В. Никешин, Н.В. Пакулин, В.З. Шнитман. Особенности тестирования сервисов безопасности сетевого уровня IPsec второй версии. // Научный сервис в сети Интернет: решение больших задач: Труды Всероссийской научной конференции (22-27 сентября 2008 г., г. Новороссийск). - М.: Изд-во МГУ, 2008. - 468 с. ISBN 978-5-211-05616-9.

70. А.В. Никешин, Н.В. Пакулин, В.З. Шнитман. Разработка тестового набора для верификации реализаций протокола безопасности IPsec v2. // Труды Института системного программирования РАН, том 18, 2010 г. Стр. 151-182.

71. А.В. Никешин, Н.В. Пакулин, В.З. Шнитман. Верификация функций безопасности протокола IPsec v2. // Программирование, том 37 № 1. М., 2011. С. 36-56.

72. Bourdonov I.B., Demakov A.V., Jarov A.A., Kossatchev A.S., Kuliamin V.V., Petrenko A.K. and Zelenov S.V. Java Specification Extension for Automated Test Development // Proceedings of PSI’2001. Novosibirsk, Russia July 2-6 2001, LNCS 2244:301-307. Springer-Verlag, 2001.

73. А.В. Никешин, Н.В. Пакулин, В.З. Шнитман. Разработка тестового набора для верификации реализаций протокола безопасности TLS. // Труды ИСП РАН, том 23, 2012 г. Стр. 387-404.

74. А.Н. Тугаенко. Тестирование соответствия почтовых протоколов сети Интернет. // Материалы Международного молодежного научного форума «ЛОМОНОСОВ-2010» (тезисы), стр.25-27.

75. Н.В.Пакулин, А.Н.Тугаенко. Разработка тестовых наборов для тестирования соответствия почтовых протоколов. // Конференция АППИ-2009, стр. 154-160.

76. А.Н. Тугаенко. Метод тестирования соответствия для расширяемых протоколов сети Интернет. // Материалы Международного молодежного научного форума «ЛОМОНОСОВ-2011».

77. N. Pakulin, A. Tugaenko. Model Based Conformance Testing for Extensible Internet Protocols // Proceedings of SYRCoSE 2011.Н.В. Пакулин, А.Н. Тугаенко.

78. Пакулин Н.В., Тугаенко А.Н., Шнитман В.З. Тестирование протоколов электронной почты Интернета с использованием моделей. // Труды ИСП РАН, том 20, 2011 г. Стр. 125-141.

79. Пакулин Н.В., Тугаенко А.Н., Шнитман В.З. Тестирование протоколов электронной почты Интернета с использованием моделей. // Программирование. т. 37 №5 - Москва: МАИК “Наука/Интерпериодика”, 2012.

80. J. Jacky, "PyModel: Model-based testing in Python", Northwest Python Day 2010.

81. Errfix: библиотека классов для тестирования с использованием моделей на Ruby. https://code.google.com/p/errfix/

82. I. Bourdonov, A. Kossatchev, A. Petrenko, and D. Galter. KVEST: Automated Generation of Test Suites from Formal Specifications. FM’99: Formal Methods. LNCS, volume 1708, Springer-Verlag, 1999, pp. 608–621.

83. А.И.Гриневич, В.В.Кулямин, Д.А.Марковцев, А.К.Петренко, В.В.Рубанов, А.В.Хорошилов. Использование формальных методов для обеспечения соблюдения программных стандартов.// Труды Института системного программирования РАН, №10, 2006.

84. В.В.Кулямин, А.К.Петренко, В.В.Рубанов, А.В.Хорошилов. Формализация интерфейсных стандартов и автоматическое построение тестов соответствия. Информационные технологии, 8:2-7, М. Новые технологии, 2007.