Systems and Means of Informatics

2015, Volume 25, Issue 1, pp 54-73

CONTROL FLOW BASED TEST SUITE GENERATION

N. Voinov
P. Drobintsev
I. Nikiforov
V. Kotlyarov
I. Selin

Abstract

The article is devoted to description of an approach to test suite generation in accordance with standard structured coverage criteria based on the control flow model. The approach is based on automatic test generation with usage of symbolic verification. The main advantage of the approach is reducing the number of generated tests obtained due to analysis of control flow data and reducing the state space for the verification system. The article contains the main ideas of the approach, the formal model of control flow, and the tools for model analysis. The results of piloting the approach in a set of projects devoted to software development are also presented.

[+] References (37)

IEEE Standard. 1990. IEEE Standard Glossary of Software Engineering Terminology. ANSI/IEEE Standard 610.12-1990. New York, N.Y.: IEEE.
ITU-T. 2002. Specification and description language (SDL). Protocol Z.100. Telecommunication standardization sector of UTI. 206 p. Avail- able at: https://www.itu.int/ITU-T/2005-2008/com17/languages/Z100.pdf (accessed March 26, 2015).
Unified Modeling Language (UML) Resource Page. Available at: http://www. uml.org/ (accessedMarch 26, 2015).
Nikiforov, I.V., A.V. Petrov,Yu.V.Yusupov, andV.P.Kotlyarov. 2011. Primenenie razlichnykh metodik formalizatsii dlya postroeniya verifikatsionnykh modeley sistem po UCM-spetsifikatsiyam[Application of miscellaneous formalization methods for cre- ating verification system models based on UCM-specifications]. Nauchno-Tehnicheskie Vedomosti SPbSPU [St. Petersburg State Polytechnical University J.] 3(126):180- 184.
Kulyamin, V.V. 2008. Metody verifikatsii programmnogo obespecheniya [Methods of software verification]. 117 p. Available at: http://www.ict.edu.ru/ft/005645/ 62322e1-st09.pdf (accessed March 25, 2015).
Broy, M., B. Jonsson, J.-P. Katoen, M. Leucke, and A. Pretschner. 2005. Model- based testing of reactive systems. Lecture notes in combustion science ser. Springer. Vol. 3472. 659 p.
Utting, M., and B. Legeard. 2007. Practical model-based testing: A tools approach. Morgan-Kaufmann. 456 p.
Ambert, F., F. Bouquet, S. Chemin, S. Guenaud, B. Legeard, F. Peureux, N. Vacelet, and M. Utting. 2002. BZ-TT: A tool-set for test generation from Z and B using constraint logic programming. Formal Approaches to Testing of Software, FATES 2002 (Workshop of CONCUR'02) Proceedings. 105-119.
Abrial, J.-R. 1996. The B-Book: Assigning programs to meanings. Cambridge Univer- sity Press. 813 p.
Farchi, E., A. Hartman, and S. S. Pinter. 2002. Using a model-based test generator to test for standard conformance. IBM Syst. J. 41(1):89-110.
GOTCHA-TCBeans: Model driven engineering technology. IBM Haifa Research Lab. Available at: www.haifa.ibm.com/projects/veri¦cation/gtcb/index.html (ac- cessed March 26, 2015).
Rational TAU: Standards-based, model-driven development solution for complex sys- tems. Available at: http://www-03.ibm.com/software/products/en/ratitau (accessed March 26, 2015).
Brinksma, E. 1988. A theory for the derivation of tests. 8th Conference (International) on Protocol Specification, Testing and Verification Proceedings.NorthHolland. 63-74.
Tretmans, J. 1992. A formal approach to conformance testing. Enschede, The Nether- lands: University of Twente. PhD Thesis. 282 p.
Tretmans, J., and A. Belinfante. 1999. Automatic testing with formal methods. 7th European Conference on Software Testing, Analysis and Review Proceedings. Barcelona, Spain. 8-10.
Fernandez, J.-C., C. Jard, T. J‚eron, and C. Viho. 1996. Using on-the-fly verification techniques for the generation of test suites. Computer aided verification. Eds. R. Alur and T.A. Henzinger. Lecture notes in computer science ser. Springer. 1102:348-359.
UPPAAL. 2012. Design verification for embedded systems. Uppsala, Swe- den: UP4ALL International AB. Available at: http://www.uppaal.com/ (accessed March 26, 2015).
Kulyamin, V.V., A.K. Petrenko, A. S.Kosachev, and I.B. Burdonov. 2003. Podkhod UniTesK k razrabotke testov. [UniTesk approach to software tests development]. Programmirovanie [Software Development] 29(6):25-43.
UniTESK: Industrial technology of reliable testing. ISP RAS. Available at: http:// www.unitesk.com/ (accessed March 26, 2015).
Model-based testing with Spec Explorer. Microsoft Research. Available at: http:// research.microsoft.com/specexplorer (accessed March 26, 2015).
Spec Explorer. MSDN Library. Available at: http://msdn.microsoft.com/en-us/ library/ee620411.aspx (accessed March 26, 2015).
Ammann, P., and P.E. Black. 1999. Abstracting formal specifications to generate soft- ware tests via model checking. 18th Digital Avionics Systems Conference Proceedings. IEEE. 2:10A.6-1-10.A.6-10.
Gargantini, A., and C. Heitmeyer. 1999. Using model checking to generate tests from requirements specifications. ACM SIGSOFT Software Engineering Notes 24(6):146- 162.
Visser, W., C. S. Pasareanu, and S. Khurshid. 2004. Test input generation with Java PathFinder. ACM SIGSOFT Software Engineering Notes 29(4):97-107.
Myers, G. J. 1979. The art of software testing. JohnWiley & Sons. 192 p.
Engel, C., and R. Hahnle. 2007. Generating unit tests from formal proofs. Tests and proofs. Eds. Yu. Gurevich and B. Meyer. Lecture notes in computer science ser. Springer-Verlag. 4454:169-188.
Gotlieb, A., B. Botella, and M. Rueher. 1998. Automatic test data generation using constraint solving techniques. ACM SIGSOFT Software Engineering Notes 23(2):53- 62.
Boyapati, C., S. Khurshid, and D. Marinov. 2002. Korat: Automated testing based on Java predicates. Symposium (International) on Software Testing and Analysis Proceedings. 123-133.
Sen, K., and G. Agha. 2006. CUTE and jCUTE: Concolic unit testing and explicit pathmodel-checking tools.Conference (International) on Computer Aided Verification Proceedings. 419-423.
Burdonov, I.B., A. S. Kosachev, V.N. Ponomarenko, and V. Z. Shnitman. 2006. Obzor podkhodov k verifikatsii raspredelennykh sistem [Review of approaches to distributed software systems verification]. ISP RAS. Preprint No. 16. 61 p.
Utting M., A. Pretschner, and B. Legeard. 2006. A taxonomy of model-based testing. Waikato, New Zealand: Department of Computer Science, The University ofWaikato. Technical Report. 17 p.
Drobintsev, P.D. 2006. Integrirovannaya tekhnologiya obespecheniya kachestva pro- grammnykh produktov s pomoshch'yu verifikatsii testirovaniya [Integrated technology for support of software systems quality based on verification and testing]. St.Petersburg: St. Petersburg State Polytechnical University. PhD Thesis.
ITU. 2004. Message Sequence Chart (MSC). Recommendation Z.120. http://www. itu.int/ITU-T/2005-2008/com17/languages/Z120.pdf (accessed March 26, 2015).
Kolchin, A.V. 2009. Razrabotka instrumentalnykh sredstv dlya proverki formalnykh modeley asinkhronnykh sistem [Development of software tools for checking of formal models of asynchronius systems]. Kiev: V.M. Glushko Institute of Cybernetics NAS. PhD Thesis. 140 p.
Beizer, ‚. 1990. Software testing techniques. 2nd ed. International ThomsonComputer Press. 580 p.
Buhr,R. J.A., andR. S.Casselman. 1995.Use Case Maps for object-oriented systems. Prentice Hall. 302 p.
Use Case Map Navigator. Available at: http://jucmnav.softwareengineering.ca (ac- cessed March 26, 2015).

[+] About this article