Финальные модели спецификации

Работа посвящена исследованию формальных методов тестирования соответствия (конформности) исследуемой системы требованиям, заданным в форме спецификации. Такое тестирование основано на семантике взаимодействия, которая определяет тестовые возможности по управлению (заданный набор тестовых воздействий) и наблюдению действий и отказов (отсутствие действий). Допускаются также ненаблюдаемые (внутренние) действия. Семантика параметризуется семействами наблюдаемых и ненаблюдаемых отказов. Вводится разрушение - запрещённое действие, которого следует избегать при взаимодействии. Определяется понятие безопасного тестирования, при котором не возникают ненаблюдаемые отказы и разрушение, и тестовые воздействия не подаются при дивергенции (бесконечной последовательности ненаблюдаемых действий). На этой основе определяются реализационная гипотеза о безопасности и безопасная конформность, а также генерация полного набора тестов по спецификации. В работе исследуются различные модели для описания спецификационных требований. Наиболее распространенной моделью является система помеченных переходов - LTS (Labelled Transition System). В то же время для рассматриваемой семантики взаимодействия существенны только трассы (последовательности наблюдений), но не состояния LTS. Поэтому естественной оказывается трассовая модель как множество трасс LTS. Такая семантика позволяет определять только конформности типа редукции, в отличие от конформностей типа симуляций, для проверки которых требуется дополнительная тестовая возможность - опрос состояния реализации [10],[11],[12],[19],[22]. При безопасном тестировании тесты генерируются по безопасным трассам спецификации, для прохождения которых используются только безопасные тестовые воздействия. Целью данной работы является выделение подмножества трасс спецификации, достаточного для генерации полного набора тестов. Такое подмножество мы назвали финальной трассовой моделью спецификации. С другой стороны, LTS-модель удобна тем, что является способом конечного представления регулярных множеств трасс. Для представления финальной трассовой модели в работе предлагается разновидность LTS, названная финальной RTS (Refusal Transition System). Переходы по наблюдаемым отказам задаются явно (эти отказы входят в алфавит RTS). Такая модель обладает целым рядом полезных для генерации тестов свойств: 1) она детерминирована, 2) трасса наблюдений безопасна тогда и только тогда, когда она заканчивается в нетерминальном состоянии, где нет разрушения, 3) тестовое воздействие безопасно после трассы тогда и только тогда, когда оно безопасно в конечном состоянии трассы, то есть в этом состоянии нет дивергенции, тестовое воздействие не вызывает разрушения и ненаблюдаемых отказов . В работе предложены алгоритмы преобразования LTS-модели в финальную RTS-модель и определены достаточные условия построения конечной RTS за конечное время.

Семантика взаимодействия, отказы, разрушение, дивергенция, конформность, безопасное тестирование, трассы, LTS, генерация тестов

1. Bourdonov I., Kossatchev A., Kuliamin V. Formal Conformance Testing of Systems with Refused Inputs and Forbidden Actions. Proc. of MBT 2006, Vienna, Austria, March 2006.

2. Бурдонов И.Б., Косачев А.С., Кулямин В.В. Формализация тестового эксперимента. «Программирование», 2007, No. 5.

3. Бурдонов И.Б., Косачев А.С., Кулямин В.В. Безопасность, верификация и теория конформности. Материалы Второй международной научной конференции по проблемам безопасности и противодействия терроризму, Москва, МНЦМО, 2007.

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

5. Игорь Бурдонов. Теория конформности (функциональное тестирование программных систем на основе формальных моделей). LAP LAMBERT Academic Publishing, Saarbrucken, Germany, 2011, ISBN 978-3-8454-1747-9, 428 стр. (содержание книги доступно по адресу: http://www.ispras.ru/~RedVerst/RedVerst/Publications/TR-01-2007.pdf)

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

7. Бурдонов И.Б., Косачев А.С. Эквивалентные семантики взаимодействия. Труды Института системного программирования РАН, N 14.1, 2008.

8. Бурдонов И.Б., Косачев А.С. Системы с приоритетами: конформность, тестирование, композиция. «Программирование», 2009, No. 4.

9. Бурдонов И.Б., Косачев А.С. Аналитическая верификация конформности. Научный сервис в сети Интернет: масштабируемость, параллельность, эффективность: Труды Всероссийской суперкомпьютерной конференции (21-26 сентября 2009 г., г. Новороссийск). - М.: Изд-во МГУ, 2009.

10. Бурдонов И.Б., Косачев А.С. Тестирование конформности на основе соответствия состояний. Труды Института системного программирования РАН, N 18, 2010.

11. Бурдонов И.Б., Косачев А.С. Симуляция систем с отказами и разрушением. 5-ый Международный симпозиум по компьютерным наукам в России. Семинар «Семантика, спецификация и верификация программ: теория и приложения».Казань 2010.

12. Бурдонов И.Б., Косачев А.С. Тестирование безопасной симуляции. 5-ый Международный симпозиум по компьютерным наукам в России. Семинар «Семантика, спецификация и верификация программ: теория и приложения».Казань 2010.

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

14. I.Burdonov, A.Kosachev. Formal conformance verification. Short Papers of the 22nd IFIP ICTSS, Alexandre Petrenko, Adenilso Simao, Jose Carlos Maldonado (eds.), Nov. 08-10, 2010, Natal, Brazil.

15. Бурдонов И.Б., Косачев А.С. Семантики взаимодействия с отказами, дивергенцией и разрушением. «Программирование», 2010, No. 5.

16. Бурдонов И.Б., Косачев А.С. Пополнение спецификации для ioco. «Программирование», 2011, No. 1.

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

18. Bernot G. Testing against formal specifications: A theoretical view. In S. Abramsky and T.S.E. Maibaum, editors, TAPSOFT’91, Volume 2, pp. 99-119. Lecture Notes in Computer Science 494, Springer-Verlag, 1991.

19. Edmonds J. Johnson E.L. Matching. Euler Tours, and the Chinese Postman. Math. Programming 5, 88-124 (1973).

20. 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.

21. 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.

22. Lee D., Yannakakis M. Principles and Methods of Testing Finite State Machines – A Survey. Proceedings of the IEEE 84, No. 8, 1090–1123, 1996.

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

24. Tretmans J. Conformance testing with labelled transition systems: implementation relations and test generation. Computer Networks and ISDN Systems, v.29 n.1, p.49-79, Dec. 1996.

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