Test scenarios generation based on formal model

A.A. Letichevsky, A.V. Kolchin

Abstract


A guided search method for automatic test scenario building during verification described. The main goal is to achieve semantic correspondence between obtained test scenarios and functional specifications of a system. The method uses user-defined regular expressions as test purposes and for model behavior traversal bounding.

Problems in programming 2010; 2-3: 209-215


References


Мур Э. Умозрительные эксперименты с последовательными машинами // Автоматы. М.: Изд-во иностр. лит. – 1956. – С. 179–210.

Hennie F. Fault-detecting experiments for sequential circuits // Proc. of 5-th annual symposium on switching theory and logical design. – 1964. – P. 95–110.

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

Bourdonov I., Kossatchev A., Petrenko A., Galter D. KVEST: Automated Generation of Test Suites from Formal Specifications // Proc. of Formal Methods’99, LNCS 1708. – 1999. – P. 608–621.

Петренко А. Спецификация тестов на основе описания трасс // Программирование. – 1993. – № 19(1). – С. 66–73.

Дейкстра Э. Дисциплина программирования. – М.: Мир, 1978.

Кулямин В. Методы верификации программного обеспечения // Всероссийский конкурсный отбор обзорно-аналитических статей по

приоритетному направлению "Информационно - телекоммуникационные системы". – 2008. – 117 С.

Broy M., Jonsson B., Katoen J., and oth. Model Based Testing of Reactive Systems // LNCS 3472. – 2005. – P. 659.

Utting M., Legeard B. Practical Model-Based Testing: A Tools Approach. Morgan-Kaufmann. – 2007. – 456 P.

Ambert F., Bouquet F., Chemin S., Guenaud S. and oth. BZ-TT: A tool-set for test generation from Z and B using constraint logic programming // Proc. of FATES’2002. – 2002. – P. 105–119.

Farchi E., Hartman A., Pinter S. Using a model-based test generator to test for standard conformance // IBM Systems Journal. – 2002. – Vol. 41(1). – P. 89–110.

Brinksma E. A theory for the derivation of tests // Proc. of 8-th International conference on protocol specification, testing and verification. – 1988. – P. 63–74.

Tretmans J. A Formal Approach to Conformance Testing // PhD thesis, University of Twente, Enschede, The Netherlands. – 1992.

Tretmans J., Belinfante A. Automatic testing with formal methods // Proc. of 7-th European Conference on Software Testing, Analysis and Review, Barcelona, Spain. – 1999. – P. 8–10.

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

http://www.uppaal.com

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

Ammann P., Black P. Abstracting formal specifications to generate software tests via model checking // Proc. of 18-th Digital Avionics Systems Conference, IEEE. – 1999. – Vol. 2. – P. 10.A.6–1–10.A.6–10.

Gargantini A., Heitmeyer C. Using model checking to generate tests from requirements specifications // ACM SIGSOFT Software Engineering Notes. – 1999. – Vol. 24(6). – P. 146–162.

Visser W., Pasareanu C., Khurshid S. Test input generation with Java PathFinder // ACM SIGSOFT Software Engineering Notes. – 2004. – № 29(4). – P. 97–107.

Майерс Г. Искусство тестирования программ. М.: Финансы и статистика. – 1982. – 174 C.

Engel C., Hahnle R. Generating unit tests from formal proofs // Y. Gurevich, B. Meyer, eds. Proc. of TAP 2007, LNCS 4454. – 2007. –

P. 169–188.

Boyapati C., Khurshid S., Marinov D. Korat: automated testing based on Java predicates // Proc. of International Symposium on Software Testing and Analysis. – 2002. – P. 123–133.

Gotlieb A., Botella B., Rueher M. Automatic test data generation using constraint solving techniques // ACM SIGSOFT Software Engineering Notes. – 1998. – Vol. 23(2). – P. 53–62.

Utting M., Pretschner A., Legeard B. A. Taxonomy of Model-Based Testing // Technical Report, Department of Computer Science,

The University of Waikato, New Zealand. – 2006. – 17 P.

Бурдонов И., Косачев А., Пономаренко В., Шнитман В. Обзор подходов к верификации распределенных систем. М.: ИСП РАН. – 2006. – 61 С.

Bourdonov I., Kossatchev A., Kuliamin V., and Petrenko A. UniTesK Test Suite Architecture // In Proc. of FME 2002, LNCS 2391, SpringerVerlag. – 2002. – P. 77–88.

Fernandez J., Jard C., Jeron T., Nedelka L., and Viho C. An experiment in automatic generation of test suites for protocols with verification technology // Science of Computer Programming. – 1997. – Vol. 29. – № 1–2. – P. 123–146.

Grabowski J., Hogrefe D., Nahm R. Test case generation with test purpose specification by MSCs // In Elsevier Science B.V. (North-Holland), editor, 6th SDL Forum. – 1993. – P. 253–266.

Edelkamp, S., Leue S. and Lafuente A. Directed explicit-state model checking in the validation of communication protocols // International journal on software tools for technology transfer. – 2003. – № 5. – P. 247–267.

Lafuente A. Directed Search for the Verification of communication protocols // Doctorial thesis, Institute of computer science, University of Freiburg. – 2003. – 157 P.

Ben-Ari. M. Principles of Spin // Springer Verlag. – 2008. – 216 P.

Burch J., Clarke E., McMillan K., Dill D., and Hwang L. Symbolic model checking: 10^20 states and beyond // Information and Computation. – 1992. – Vol. 98. – № 2. – P. 142–170.

Cimatti A., Clarke E. M., Giunchiglia E., and others. NuSMV 2: An OpenSource Tool for Symbolic Model Checking // In Proceeding of

International Conf. on Computer-Aided Verification, Copenhagen, Denmark. – 2002. – P. 359–364.

Колчин А. Метод направления поиска и генерации тестовых сценариев при верификации формальных моделей асинхронных систем // Проблемы программирования. – № 4. – 2008. – С. 5–12.

Колчин А. Направленный поиск в верификации формальных моделей // Тези доп. міжнар. конф. «Теоретичні та прикладні аспекти побудови програмних систем TAAPSD'2007» – Бердянск. НаУКМА, Національний ун-т ім. Т.Г. Шевченка, Ін-т програмних систем НАН України. – 2007. – С. 256–258.

Баранов С., Котляров В., Летичевский А. Индустриальная технология автоматизации тестирования мобильных устройств на основе верифицированных поведенческих моделей проектных спецификаций требований // Труды междунар. науч. конф. «Космос, астрономия и программирование» – СПбГУ, С-Пб. – 2008. – С. 134–145.

Aho A. Algorithms for finding patterns in strings // Handbook for theoretical computer science, MIT Press. – 1990. – Vol. A. – P. 257–300.

Smyth B. Computing Patterns in Strings // ACM Press Books. – 2003. – 440 P.

Tarjan R. Depth first search and linear graph algorithms // SIAM Journal on Computing. – 1972. – Vol. 1. – № 2. – P.146–160.


Refbacks

  • There are currently no refbacks.