Спецификация и тестирование систем с асинхронным интерфейсом
       

Литература




1. Euler E.E., Jolly S.D., Curtis H.H. The Failures of the Mars Climate Orbiter and Mars Polar Lander: A Perspective from the People Involved // Proceedings of Guidance and Control 2001. American Astronautical Society, AAS 01-074, 2001.
2. Report on the Loss of the Mars Climate Orbiter Mission. JPL D-18441, 1999.
3. Porrello A.M. Death and Denial: The Failure of the Therac-25, A Medical Linear Accelerator.
4. Leveson N.G., Clark S.T. An Investigation of the Therac-25 Accidents // Computer. July, 1993. P. 18-41.
5. Patriot missile defense: Software problems led to system failure at Dhahran, Saudi Arabia. Report GAO/IMTEC-92-26, Information Management and Technology Division, US General Accounting Office. Washington DC, Feb. 11992.
6. Berry D. M. Formal methods: the very idea, some thoughts about why they work when they work. // Science of Computer Programming #42(1). P. 11-27.
7. Floyd R. W. Assigning meanings to programs // Proceedings Symp. Appl. Math., 19. in: J.T.Schwartz (ed.), Mathematical Aspects of Computer Science. P. 19-32. American Mathematical Society, Providence, R.I., 1967.
8. Francez N. Verification of programs. Addison-Wesley Publishers Ltd., 1992.
9. Manna Z. Mathematical theory of computation. McGraw-Hill, 1974.
10. Manna Z., Pnueli A. The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag, 1991.
11. Blackburn M., Busser R., Nauman A., Knockerbocker R., Kasuda R. Mars Polar Lander Fault Identification Using Model-Based Testing // 26th Annual NASA Goddard Software Engineering Workshop. 27-29 November, 2001.
12. Dalal S. R., Jain A., Karunanithi N., Leaton J. M., Lott C. M. Model-Based Testing of a Highly Programmable System // Proceedings of ISSRE-98. 5-7 November 1998.
13. Dalal S. R., Jain A., Karunanithi N., Leaton J. M., Lott C. M., Patton G. C., Horowitz B. M. Model-Based Testing in Practice // Proceedings of the ICSE'99. May 1999.
14. Farchi E., Hartman A., Pinter S. S. Using a Model-Based Test Generator to Test for Standard Conformance // IBM Systems Journal, 2002. V. 41, No. 1, P. 89-110.
15. Gronau A., Hartman A., Kirshin A., Nagin K., Olvovsky S. A Methodology and Architecture for Automated Software Testing // IBM Research Laboratory in Haifa Technical Report, 2000.
16. Offutt A. J., Liu S., Abdurazik A. Generating Test Data from State-Based Specifications // Journal of Software Testing, Verification & Reliability. V. 13, No. 1, March 2003.
17. Al-Ghafees M., Whittaker J. A. Markov Chain-based Test Data Adequacy Criteria: a Complete Family. // IS June 2002. P. 13-37.
18. Bourdonov I., Kossatchev A., Kuliamin V., Petrenko A. UniTesK Test Suite Architecture // Proceedings of FME, 2002. LNCS 2391. P. 77-88. Springer-Verlag.
19. Кулямин В.В., Петренко А.К., Косачев А.С., Бурдонов И.Б. Подход UniTesK к разработке тестов // Программирование, 29(6). 2003. С. 25-43.
20. Баранцев А.В., Бурдонов И.Б., Демаков А.В., Зеленов С.В., Косачев А.С., Кулямин В.В., Омельченко В.А., Пакулин Н.В., Петренко А.К., Хорошилов А.В. Подход UniTesK к разработке тестов: достижения и перспективы // Труды Института системного программирования РАН, №5, 2004. .
21. Meyer B. Applying 'Design by Contract' // IEEE Computer, vol. 25, October 1992. P. 40 51.
22. [,PDF].
23. Burdonov I., Kossatchev A., Petrenko A., Cheng S., Wong H. Formal Specification and Verification of SOS Kernel // BNR, NORTEL Design Forum, June 1996.
24. Monin J. F., Hinchey M. G. Understanding Formal Methods. Springer-Verlag, 2003.
25. Бурдонов И.Б., Косачев А.С., Кулямин В.В. Использование конечных автоматов для тестирования программ. // Программирование, 2000, №2.
26. Бурдонов И.Б., Косачев А.С., Кулямин В.В. Неизбыточные алгоритмы обхода ориентированных графов. Детерминированный случай. // Программирование. 2003. №5. С. 11 30.
27. Бурдонов И.Б., Косачев А.С., Кулямин В.В. Неизбыточные алгоритмы обхода ориентированных графов. Недетерминированный случай. // Программирование. 2004. №1. С. 4 24.
28. Бурдонов И.Б., Косачев А.С., Кулямин В.В. Асинхронные автоматы: классификация и тестирование. // Труды ИСП РАН. 2003. №4. С. 7 84.
29. Хорошилов А.В. Спецификация и тестирование компонентов с асинхронным интерфейсом. Диссертация на соискание ученой степени кандидата физико-математических наук. Москва, ИСП РАН, 2006.
30. Липский В. Комбинаторика для программистов. Москва, Мир, 1988.
31. Message Sequence Charts. ITU recommendation Z.120.
32. Agamirzian I., Groshev S.G., Khoroshilov A.V., Kluchnikov G.N., Kossatchev A.S., Omelchenko V.A., Pakoulin N.V., Petrenko A.K., Shnitman V.Z. MSR IPv6 verification project, December 2001. [].
33. Agamirzian I., Groshev S.G., Khoroshilov A.V., Kluchnikov G.N., Kossatchev A.S., Omelchenko V.A., Pakoulin N.V., Petrenko A.K., Shnitman V.Z. MSR IPv6 Verification within the CTesK-lite Framework, April 2002. [].
34. [].
35. Linux Standard Base Core 3.1. ISO/IEC IS-23360. [].
<
1(обратно к тексту) В данной работе рассматриваются только не более чем счетные множества.
2(обратно к тексту) Здесь под процессом тестирования понимается процесс выполнения уже разработанного теста. Если под процессом тестирования понимать процесс разработки теста, то данное утверждение будет не совсем верно.
3(обратно к тексту) Данные правила приводятся только для целей иллюстрации, поэтому их определение дано на поверхностном уровне, не рассматриваются вопросы, касающиеся области их применимости, и т.д.
4(обратно к тексту) Множества Xstack, Ystack и Vstack определяются с точностью до изоморфизма.
5(обратно к тексту) В указанной работе этот алгоритм обозначается символом A2.
6(обратно к тексту) Определение обозначений XI, YI и VI смотрите в разделе "Описание модели требований".
7(обратно к тексту) Более детальное обсуждение проблемы нарушения предусловия интерфейсных операций-стимулов смотрите в разделе "Нарушение предусловий асинхронных воздействий".
8(обратно к тексту) Здесь и далее идентификатор Unit будет обозначать множество, состоящее из единственного элемента &#x0065;, а идентификатор Bool - множество, состоящее из двух элементов true и false.
9(обратно к тексту) В рамках данного доказательства мы считаем, что ei = ( vi, xi, v'i ).

Содержание раздела