Preview

Труды Института системного программирования РАН

Расширенный поиск

Развитие теории конформности: семантики, формальные модели, алгоритмы

https://doi.org/10.15514/ISPRAS-2014-26(1)-2

Аннотация

Статья посвящена теоретическим и практическим работам по тестированию конформности (conformance testing), которые выполнялись в ИСП РАН c 1994-го года и по настоящее время. Развитие теории конформности шло по нескольким направлением и в целом носило характер обобщения используемых семантик взаимодействия, моделей и конформностей. Необходимость такого обобщения диктовалась, прежде всего, требованиями практического тестирования. Это касается таких свойств систем как недетерминизм, частичная определённость, асинхронность, разнообразие тестовых воздействий и наблюдений над поведением реализации и т.п. При этом в центре внимания всегда находилась эффективность тестирования, определяемая как оптимизацией тестовых наборов, так и алгоритмами генерации тестов, в том числе on-fly. Мы рассматриваем основные вехи этого пути в кратком и неформальном обсуждении, уделяя внимание не деталям, а основным проблемам и способам их решения, пытаясь выявить общую тенденцию развития.

Об авторах

И. Б. Бурдонов
ИСП РАН
Россия


А. С. Косачев
ИСП РАН
Россия


Список литературы

1. Burdonov I., Kossatchev A., Petrenko A., Cheng S., Wong H. Formal Specification and Verification of SOS Kernel. BNR/NORTEL Design Forum, June 1996.

2. Баранцев А.В., Бритвина Е.Н., Бурдонов И.Б., Косачев А.С., Гоманюк С.В., Демаков А.В., Иванов А.В., Максимов А.В., Петренко А.К., Сазанов Ю.Л., Сортов А.А., Стефанов В.П., Сумар Г.М. Архитектура системы генерации и пропуска тестов // Вопросы кибернетики, Москва 1998.

3. Bourdonov I., Kossatchev A., Petrenko A., Galter D. KVEST: Automated Generation of Test Suites from Formal Specifications // Proceedings of Formal Method Congress, Toulouse, France, 1999, LNCS, № 1708, pp.608-621.

4. Бурдонов И.Б., Косачев А.С., Демаков А.В., Петренко А.К., Максимов А.В. Формальные спецификации в технологиях обратной инженерии и верификации программ // Труды ИСП РАН, № 1, 1999, стр. 31-43.

5. Bourdonov I.B., Kossatchev A.S., Petrenko A.K., Kuliamin V.V. UniTESK Test Suite Architecture // Proceedings of FME’2002 conference, Copenhagen, Denmark, LNCS, № 2391, 2002, pp. 77-88.

6. Бурдонов И.Б., Косачев А.С., Кулямин В.В., Петренко А.К. Подход UniTESK к разработке тестов // «Программирование»,-2003, №6, стр.25-43.

7. Bourdonov I.B., Kossatchev A.S., Kuliamin V.V., Petrenko A.K., Pakoulin N.V. Integration of Functional and Timed Testing of Real-Time and Concurrent Systems // Perspectives of System Informatics // LNCS. № 2890, Springer-Verlag, 2003, pp.450‑461.

8. Bourdonov I.B., Kossatchev A.S., Kuliamin V.V., Petrenko A.K. UniTESK: Model Based Testing in Industrial Practice // Proceedings of 1-st European Conference on Model-Driven Software Engineering, Nurnberg, December 2003, pp. 55-63.

9. Бурдонов И.Б., Баранцев А.В., Демаков А.В., Зеленов С.В., Косачев А.С., Кулямин В.В., Омельченко В.А., Пакулин Н.В., Петренко А.К., Хорошилов А.В. Подход UniTESK к разработке тестов: достижения и перспективы // Труды ИСП РАН, № 5, 2004, стр.121‑156.

10. Калинов А.Я., Косачев А.С., Посыпкин М.А,, Соколов А.А. Автоматическая генерация тестов для графического пользовательского интерфейса по UML диаграммам действий // Труды ИСП РАН, № 6, 2004, стр.7-84.

11. V.Kuliamin, A.K.Petrenko. Applying Model Based Testing in Different Contexts // Proceedings of Seminar on Perspectives on Model Based Testing, Dagstuhl, Germany, September 2004.

12. V.Kuliamin. Multi-paradigm Models as Source for Automated Test Construction // Proceedings of Workshop on Model Based Testing, Barcelona, Spain, March 2004. Electronic Notes in Theoretical Computer Science 111:137-160, 2005, Elseveir.

13. А.А.Сортов, А.В.Хорошилов. Функциональное тестирование Web-приложений на основе технологии UniTESK. //Труды ИСП РАН, №8, 2004, стр.77-97.

14. V.Kuliamin. Model Based Testing of Large-scale Software: How Can Simple Models Help to Test Complex System. //Proc of ISOLA 2004, Cyprus, October 2004, pp. 311-316.

15. В.П. Иванников, А.С. Камкин, В.В. Кулямин, А.К. Петренко. Применение технологии UniTESK для функционального тестирования моделей аппаратного обеспечения // Препринт ИСП РАН, 2005.

16. V.Kuliamin, A.Petrenko, N.Pakoulin. Extended Design-by-Contract Approach to Specification and Conformance Testing of Distributed Software. Proc. of 9-th WMSCI, Orlando, USA, July 2005, v. VII. Model Based Development and Testing, pp. 65-70.

17. V.Kuliamin, A.Petrenko, N.Pakoulin. Practical Approach to Specification and Conformance Testing of Distributed Network Applications. Proc. of 2-nd ISAS 2005, Berlin, Germany, April 2005, pp. 60-73 M. Malek, E. Nett, N. Suri, eds. Service Availability. LNCS 3694, pp. 68-83, Springer-Verlag, 2005.

18. С.Грошев. Применение технологии UniTESK для тестирования систем с различной конфигурацией активных потоков управления. //Труды ИСП РАН, №9, 2006, стр. 67-81.

19. А.В.Хорошилов. Спецификация и тестирование систем с асинхронным интерфейсом. //Препринт ИСП РАН, №12, 2006.

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

21. В.С. Мутилин. Паттерны проектирования тестовых сценариев. //Труды ИСП РАН, №9, 2006.

22. A.Grinevich, A.Khoroshilov, V.Kuliamin, D.Markovtsev, A.Petrenko, V.Rubanov. Formal Methods in Industrial Software Standards Enforcement. Proc. of PSI'2006, Novosibirsk, Russia, June 2006.

23. Н.В.Пакулин, А.В.Хорошилов. Разработка формальных моделей и тестирование соответствия для систем с асинхронными интерфейсами и телекоммуникационных протоколов. Программирование, №6, 2007.

24. В.П.Иванников, А.С.Камкин, А.С.Косачев, В.В.Кулямин, А.К.Петренко. Использование контрактных спецификаций для представления требований и функционального тестирования моделей аппаратуры.// Программирование, №5, 2007, стр. 47-61.

25. Kamkin. Coverage-Directed Verification of Microprocessor Units Based on Contract Specifications. EWDTS 2008, pp. 84-87.

26. А. Камкин. Генерация тестовых программ для микропроцессоров. // Труды ИСП РАН, 2008.

27. А.К. Петренко. Унификация в автоматизации тестирования. Позиция UniTESK // Препринт ИСП РАН, т. 14, ч. 1, 2008, стр. 7-22.

28. A.Petrenko. Formal Methods and Innovation Economy: Facing New Challenges. //Proceedings of the 6th IEEE International Conference on Software Enginering and Formal Methods, Cape Town, South Africa, 10-14 November 2008.

29. S.G.Groshev. Bug localization by constructing reduced traces.// Programming and Computer Software, Volume 35, Number 3, pp. 145-157, may 2009.

30. S. Frenkel, A.Kamkin. Verification Methodology Based on Algorithmic State Machines and Cycle-Accurate Contract Specifications. // East-West Design & Test Symposium, September 18-21, 2009, pp. 39-42.

31. В. В. Кулямин. Интеграция методов верификации программных систем. // Программирование, 35(4):41-55, 2009.

32. В. В. Кулямин. Перспективы интеграции методов верификации программного обеспечения. // Труды ИСП РАН, 16:73-88, 2009.

33. M. Chupilko. Constructing Test Sequences for Hardware Designs with Parallel Starting Operations Using Implicit FSM Models. // EWDTS-2009 (East-West Design and Test Symposium 2009). Proceedings of IEEE East-West Design & Test Symposium (EWDTS 2009), 393-396 pp.

34. M. Chupilko, A. Kamkin. Specification-Driven Testbench Development for Synchronous Parallel-Pipeline Designs. // NorChip-2009, pp.1-4.

35. Я.С. Губенко, А.С. Камкин, М.М. Чупилко. Сравнительный анализ современных технологий разработки тестов для моделей аппаратного обеспечения. // Труды ИСП РАН 2009, том17, стр.133-143.

36. С.А. Смолов. Разработка тестового набора для функционального тестирования инфраструктурного программного обеспечения Грид с применением технологии UniTESK. // Сборник научных трудов научно-практической конференции «Актуальные проблемы программной инженерии», 2009, стр.183-189.

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

38. В.В. Кулямин. Архитектура среды тестирования на основе моделей, построенная на базе компонентных технологий. // Труды ИСП РАН, N 18, 2010, стр. 9-44.

39. С.Г. Грошев. Технология создания гетерогенных трасс, их анализа и генерации из них отчётов. // Труды ИСП РАН, N 18, 2010, стр. 45-66.

40. М.М. Чупилко. Автоматизация системного тестирования моделей аппаратуры на основе формальных спецификаций. // Труды ИСП РАН, N 18, 2010, стр. 115-128.

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

42. M. Chupilko. Models of Synchronous Hardware Designs Based on FSM at Different Abstraction Levels: Application to Functional Verification // EWDTS-2010 (East-West Design and Test Symposium 2010). Proceedings of IEEE East-West Design & Test Symposium (EWDTS 2010), 127-130 pp.

43. M. Chupilko, A. Kamkin. Developing cycle-accurate contract specifications for synchronous parallel-pipeline hardware: application to verification. // BEC-2010 (Baltic Electronics Conference 2010). Proceedings of the 12th Biennial Baltic Electronics Conference (BEC 2010), 185-188 pp.

44. N. Pakulin, A. Tugaenko. Specification Based Conformance Testing for Email Protocols. // Proceedings of ISoLA 2010, pp.371-382. Heraclion, Greece, 2010.

45. В. В. Кулямин. Компонентная архитектура среды для тестирования на основе моделей. // Программирование, 36(5):54-75, 2010.

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

47. Kamkin. Simulation-Based Verification with Time-Abstract Models. EWDTS, 2011.

48. M. Chupilko, A. Kamkin. A TLM-based approach to functional verification of hardware components at different abstraction levels. LATW, 2011.

49. А. Камкин, М. Чупилко. Механизмы поддержки функционального тестирования моделей аппаратуры на разных уровнях абстракции, Труды ИСП РАН, 2011.

50. M.Chupilko. C++TESK-SystemVerilog united approach to simulation-based verification of hardware designs. EWDTS-2011.

51. V. Kuliamin, N. Pakulin, A. Tugaenko. Case Studies of Summer Model-based Testing Framework, Model-based Testing User Conference, October 18-20, 2011.

52. В.П. Иванников, А.К. Петренко. Модели в разработке и анализе программных систем. Ломоносовские чтения, 2011.

53. Y. Gerlits, A. Khoroshilov. «Model-Based Testing of Safety Critical Real-Time Control Logic Software» // In Proceedings of the Seventh Workshop on Model-Based Testing (MBT 2012), Tallin, Estonia, March 25, 2012.

54. N. Pakulin. Integrated Modular Avionics: New Challenges for MBTБ. // ETSI TTCN-3 User Conference and Model Based Testing Workshop, Bangalore, India, 11-14 June 2012.

55. Шнитман В.З., Никешин А.В., Пакулин Н.В. Применение моделей для тестирования протоколов безопасности. // Всероссийская конференция «Инфокоммуникационные технологии в научных исследованиях», ИКИ РАН, 14-16 ноября 2012 г.

56. Чупилко М.М. Разработка тестовых систем для многомодульных моделей аппаратуры. Программирование, 2012, №1, с.47-58

57. http://www.UniTESK.com

58. Бурдонов И.Б., Косачев А.С., Кулямин В.В. Использование конечных автоматов для тестирования программ. «Программирование». 2000. № 2.

59. Бурдонов И.Б., Косачев А.С., Кулямин В.В. Неизбыточные алгоритмы обхода ориентированных графов. Детерминированный случай. «Программирование». 2003. № 5.

60. И.Б.Бурдонов, А.С.Косачев, В.В.Кулямин. Асинхронные автоматы: классификация и тестирование. // Труды Института системного программирования РАН, №4, 2003, стр.7-84.

61. Бурдонов И.Б., Косачев А.С., Кулямин В.В. Неизбыточные алгоритмы обхода ориентированных графов. Недетерминированный случай. «Программирование». 2004. № 1.

62. И.Б.Бурдонов. Проблема отката по дереву при обходе неизвестного ориентированного графа конечным роботом. Программирование, №6, 2004.

63. И.Б.Бурдонов. Обход неизвестного ориентированного графа конечным роботом. Программирование, №4, 2004.

64. I.B.Bourdonov, A.S.Kossatchev, V.V.Kuliamin. Formal Conformance Testing of Systems with Refused Inputs and Forbidden Actions. Proceedings of the Workshop on Model Based Testing (MBT 2004), Elsevier, 2006.

65. И.Б.Бурдонов, А.С.Косачев, В.В.Кулямин. Формализация тестового эксперимента.// Программирование, №5, 2007, стр. 3-32.

66. И.Б.Бурдонов, А.С.Косачев, В.В.Кулямин. Безопасность, верификация и теория конформности. «Материалы второй международной научной конференции по проблемам безопасности и противодействия терроризму. МГУ 2006», М., МЦНМО, 2007, стр. 135-158.

67. И.Б.Бурдонов, Косачев А.С., В.В.Кулямин. Теория соответствия для систем с блокировками и разрушением. // «Физ-мат лит» Наука, Москва, 2008. 412 с.

68. И.Б.Бурдонов, Косачев А.С. Системы с приоритетами: конформность, тестирование, композиция. // Труды ИСП РАН, N 14.1, 2008, стр.23-54.

69. И.Б.Бурдонов, Косачев А.С. Обобщённые семантики тестового взаимодействии. // Труды ИСП РАН, N 15, 2008, стр.69-106.

70. И.Б.Бурдонов, Косачев А.С. Эквивалентные семантики взаимодействия. // Труды ИСП РАН, N 14.1, 2008, стр.55-72.

71. И.Б.Бурдонов. Теория конформности (функциональное тестирование программных систем на основе формальных моделей). LAP Lambert Academic Publishing, 2011, 428 стр. (докторская диссертация И.Б.Бурдонова 2008 г.)

72. И.Б. Бурдонов, А.С. Косачев. Системы с приоритетами: конформность, тестирование, композиция. // «Программирование», -2009, №4–стр. 24-40.

73. И.Б. Бурдонов, А.С. Косачев. Полное тестирование с открытым состоянием ограниченно недетерминированных систем. // Труды ИСП РАН, N 17, 2009, стр.161-192.

74. И.Б. Бурдонов, А.С. Косачев. Полное тестирование с открытым состоянием ограниченно недетерминированных систем. // «Программирование», -2009, №6–стр 3-18.

75. И.Б. Бурдонов, А.С. Косачев. Тестирование с преобразованием семантик. // Труды ИСП РАН, N 17, 2009, стр.193-208.

76. И.Б. Бурдонов, А.С. Косачев. Тестирование конформности на основе соответствия состояний. // Труды ИСП РАН, N 18, 2010, стр. 183-220.

77. Kossachev, I.Burdonov. Formal Conformance Verifcation, Short Papers of the 22nd IFIP ICTSS, Alexandre Petrenko, Adenilso Simao, Jose Carlos Maldonado (eds.), Nov. 08-10, 2010, Natal, Brazil, pp.1-6.

78. А.С. Косачев, И.Б.Бурдонов. Семантики взаимодействия с отказами, дивергенцией и разрушением. // «Программирование», -2010, №5–стр 3-23.

79. И.Б.Бурдонов, А.С.Косачев, Семантики взаимодействия с отказами, дивергенцией и разрушением. Часть 1. Гипотеза о безопасности и безопасная конформность, «Вестник Томского государственного университета. Управление, вычислительная техника и информатика», №4, 2010, стр.124-133

80. И.Б.Бурдонов, А.С.Косачев, Безопасное тестирование симуляции систем с отказами и разрушением, «Моделирование и анализ информационных систем», Том 17, Номер 4, 2010. стр. 27—40.

81. И.Б.Бурдонов, А.С.Косачев. Пополнение спецификации для ioco. // Программирование, №1, 2011, с. 3-18.

82. Бурдонов И.Б., Грошев С.Г., Демаков А.В., Камкин А.С., Косачев А.С., Сортов А.А., Параллельное тестирование больших автоматных моделей, Вестник ННГУ, №3, 2011 г., стр. 187-193

83. Demakov, A. Kamkin, A. Sortov. High-Performance Testing: Parallelizing Functional Tests for Computer Systems Using Distributed Graph Exploration. Open Cirrus, 2011.

84. И.Б.Бурдонов, А.С.Косачев. Удаление из спецификации неконформных трасс // Препринт ИСП РАН, Препринт 23, 2011 г, с. 1-219.

85. I.B.Bourdonov, A.S.Kossatchev. Safe simulation testing of systems with refusals and destructions // Automatic Control and Computer Sciences, Vol. 45, №7, 2011, pp. 380-389.

86. И.Б.Бурдонов, А.С.Косачев. Семантики взаимодействия с отказами, дивергенцией и разрушением. Часть 2. Условия конечного полного тестирования // Вестник Томского Государственного Университета, № 2(15), 2011.

87. И.Бурдонов, А.Косачев, Финальные модели спецификации, Труды ИСП РАН, том 22, 2012 г., ISSN 2079-8156, с. 233-276

88. И.Бурдонов, А.Косачев, Зависимости между ошибками на классах тестируемых реализаций, Труды ИСП РАН, том 23, 2012 г., ISSN 2079-8156

89. И.Б.Бурдонов, А.С.Косачев. Формализация тестового эксперимента –II. // Программирование, №4, 2013, с. 3-27.

90. И.Б.Бурдонов, А.С.Косачев. Согласование конформности и композиции // Программирование, №6, 2013, с. 3-15.

91. И.Бурдонов, А.Косачев, Обход неизвестного графа коллективом автоматов, Труды Международной суперкомпьютерной конференции «Научный сервис в сети Интернет: все грани параллелизма», 2013, изд. МГУ, стр. 228-232.

92. Milner R. Modal characterization of observable machine behaviour. In G. Astesiano & C. Bohm, editors: Proceedings CAAP 81, LNCS 112, Springer, pp. 25-34.

93. van Glabbeek R.J. The linear time – branching time spectrum. In J.C.M. Baeten and J.W. Klop, editors, CONCUR’90, Lecture Notes in Computer Science 458, Springer-Verlag, 1990, pp 278–297.

94. Vaandrager F. On the relationship between process algebra and Input/Output Automata. In Logic in Computer Science, pp. 387-398. Sixth Annual IEEE Symposium, IEEE Computer Society Press, 1991.

95. van Glabbeek R.J. The linear time - branching time spectrum II; the semantics of sequential processes with silent moves. Proceedings CONCUR ’93, Hildesheim, Germany, August 1993 (E. Best, ed.), LNCS 715, Springer-Verlag, 1993, pp. 66-81.

96. De Nicola R., Segala R. A process algebraic view of Input/Output Automata. Theoretical Computer Science, 138:391-423, 1995.

97. D. Lee and M. Yannakakis. Principles and Methods of Testing Finite-State Machines. A survey. Proceedings of the IEEE, Vol. 84, № 8, 1996, pp. 1090–1123.

98. Tretmans J. Test Generation with Inputs, Outputs and Repetitive Quiescence. In: Software-Concepts and Tools, Vol. 17, Issue 3, 1996.

99. Heerink L. Ins and Outs in Refusal Testing. PhD thesis, University of Twente, Enschede, The Netherlands, 1998.

100. Marine Tabourier, Ana Cavalli and Melania Ionescu , A GSM-MAP Protocol Experiment Using Passive Testing, Proceeding of FM'99 (World Congress on Formal methods in development of Computing Systems), Toulouse (France), 20-24 September 1999.

101. Jard C., Jéron T., Tanguy L., Viho C. Remote testing can be as powerful as local testing. In Formal methods for protocol engineering and distributed systems, FORTE XII/ PSTV XIX’ 99, Beijing, China, J. Wu, S. Chanson, Q. Gao (eds.), pp. 25-40, October 1999.

102. van der Bijl M., Rensink A., Tretmans J. Compositional testing with ioco. Formal Approaches to Software Testing: Third International Workshop, FATES 2003, Montreal, Quebec, Canada, October 6th, 2003. Editors: Alexandre Petrenko, Andreas Ulrich ISBN: 3-540-20894-1. LNCS volume 2931, Springer, pp. 86-100.

103. van der Bijl M., Rensink A., Tretmans J. Component Based Testing with ioco. CTIT Technical Report TR-CTIT-03-34, University of Twente, 2003.

104. Alexandre Petrenko, Nina Yevtushenko: Testing from Partial Deterministic FSM Specifications. IEEE Trans. Computers 54(9): 1154-1165 (2005).

105. Adenilso da Silva Simão, Alexandre Petrenko, Nina Yevtushenko: Generating Reduced Tests for FSMs with Extra States. TestCom/FATES 2009: 129-145.

106. Maurice P. Herllihy, Jeannette M. Wing. Linearizability: A Correctness Condition for Concurrent Objects //ACM Transactions on Programming Languages and Systems, Vol. 12, No. 3, July 1990, pp. 463-492.


Рецензия

Для цитирования:


Бурдонов И.Б., Косачев А.С. Развитие теории конформности: семантики, формальные модели, алгоритмы. Труды Института системного программирования РАН. 2014;26(1):27-72. https://doi.org/10.15514/ISPRAS-2014-26(1)-2

For citation:


Burdonov I., Kossatchev A. Conformance theory development: semantics, formal models, algorithms. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2014;26(1):27-72. (In Russ.) https://doi.org/10.15514/ISPRAS-2014-26(1)-2



Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 2079-8156 (Print)
ISSN 2220-6426 (Online)