Abstract
We present a strategy for the automatic generation of test cases from parametrised use case templates that capture control flow, state, input and output. Our approach allows test scenario selection based on particular traces or states of the model. The templates are internally represented as CSP processes with explicit input and output alphabets, and test generation is expressed as counter-examples of refinement checking, mechanised using the FDR tool. Soundness is addressed through an input–output conformance relation formally defined in the CSP traces model. This purely process algebraic characterisation of testing has some potential advantages, mainly an easy automation of conformance verification and test case generation via model checking, without the need to develop any explicit algorithm.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
ISO 8807:1989 (1989) LOTOS: a formal description technique based on the temporal ordering of observational behaviour. ISO
Alur R, Henzinger TA, Kupferman O, Vardi MY (1998) Alternating refinement relations
Andrade W et al. (2007) Interruption test case generation for mobile phone applications (in Portuguese). In: XXV Brazilian symposium in computer networks and distributed systems
Bertolino A (2007) Software testing research: achievements, challenges, dreams. In: FOSE ’07: 2007 future of software engineering. IEEE Computer Society, Washington, pp 85–103
Bezerra R (2011) Extração Automática de Modelos CSP a partir de Casos de Uso. Master’s thesis, CIn-UFPE (Center of Informatics of Federal University of Pernambuco)
Bertolino A, Gnesi S (2003) Use case-based testing of product lines. SIGSOFT Softw Eng Notes 28(5): 355–358
Broy M, Jonsson B, Katoen J-P, Leucker M, Pretschner A (2005) Model-based testing of reactive systems: advanced lectures (LNCS). Springer-Verlag New York, Inc., Secaucus
Briand L, Labiche Y (2002) A UML-based approach to system testing. Softw Syst Model 1(1): 10–42
Bertolini C, Mota A, Aranha E, Ferraz C (2010) GUI testing techniques evaluation by designed experiments. In: International conference on software testing verification and validation (ICST). IEEE, pp 235–244
Cartaxo EG, Andrade WL, Oliveira Neto FG, Machado PDL (2008) LTS-BT: a tool to generate and select functional test cases for embedded systems. In: SAC ’08: Proceedings of the 2008 ACM symposium on applied computing. ACM, New York, pp 1540–1544
Cavalcanti A, Gaudel M-C (2007) Testing for refinement in CSP. In: ICFEM. LNCS, vol 4789. Springer, Berlin, pp 151–170
Colvin R, Hayes IJ (2009) CSP with hierarchical state. In: IFM ’09: Proceedings of the 7th international conference on integrated formal methods. Springer, Berlin, pp 118–135
Clarke D, Jéron T, Rusu V, Zinovieva E (2001) STG: a tool for generating symbolic test programs and oracles from operational specifications. SIGSOFT Softw Eng Notes 26(5): 301–302
Cabral G, Sampaio A (2008) Automated formal specification generation and refinement from requirement documents. J Braz Comput Soc 14(1): 87–106
Cabral G, Tamai T (2008) Requirement-based testing through formal methods. In: Proceedings of TESTCOM-FATES 2008—short papers
Damasceno A, Farias A, Mota A (2009) A mechanized strategy for safe abstraction of CSP specifications. In: Formal methods: foundations and applications. LNCS, vol 5902. Springer, Berlin, pp 118–133
dos Prazeres Farias J (2008) NLScripts: composição assistida de scripts de testes a partir de descrições em linguagem natural controlada (in Portuguese). Master’s thesis, CIn-UFPE (Center of Informatics of Federal University of Pernambuco), June 2008
Edmund SC, Edmund SC, Clarke EM, Sharygina N, Sinha N (2004) State/event-based software model checking. In: Integr Form Methods 2999: 128–147
Ferreira F, Neves L, Silva M, Borba P (2010) TaRGeT: a model based product line testing tool. In: Proceedings of CBSoft 2010—tools panel
Formal Systems (2005) Failures-divergence refinement—FDR2 user manual. Formal Systems (Europe) Ltd, June 2005
Formal Systems (2011) Formal systems Web site. http://fsel.com. Sep 2011
Gois FNB (2010) Test script diagram—Um modelo para geração de scripts de testes (in Portuguese). Master’s thesis, Universidade de Fortaleza (UNIFOR)
Object Group (2007) OMG unified modeling language (OMG UML). Superstructure, V2.1.2. Technical report
Hierons R, Bogdanov K, Bowen J, Cleaveland R, Derrick J, Dick J, Gheorghe M, Harman M, Kapoor K, Krause P, Lüttgen G, Simons A, Vilkomir S, Woodward M, Zedan H (2009) Using formal specifications to support testing. ACM Comput Surv 41(2):1–76
Hennessy M (1988) Algebraic theory of processes. MIT Press, Cambridge
Hartmann J, Vieira M, Foster H, Ruder A (2005) A UML-based approach to system testing. Innov Syst Softw Eng 1(1): 12–24
Jard C, Jéron T (2005) TGV: theory, principles and algorithms. A tool for the automatic synthesis of conformance test cases for non-deterministic reactive systems. Int J Softw Tools Technol Transf 7(4): 297–315
Ledru Y, du Bousquet L, Bontron P, Maury O, Oriat C, Potet M-L (2001) Test purposes: adapting the notion of specification to testing. In: Proceedings of IEEE/ACM international conference on automated software engineering, 2001 (ASE 2001). IEEE Computer Society, pp 127–134, Nov 2001
Leitão D et al. (2007) NLForSpec: translating natural language descriptions into formal test case specifications. In: SEKE. Knowledge Systems Institute Graduate School, pp 129–134
Lima L, Iyoda J, Sampaio A, Aranha E (2009) Test case prioritization based on data reuse an experimental study. In: ESEM ’09: Proceedings of the 2009 3rd international symposium on empirical software engineering and measurement, Washington, DC, USA. IEEE Computer Society, pp 279–290
Mota A, Borba P, Sampaio A (2002) Mechanical abstraction of CSP-Z processes. In: FME 2002: formal methods—getting IT right. LNCS, vol 2391. Springer, Berlin, pp 163–183, Jan 2002
Milner R (1989) Communication and concurrency. Prentice Hall
Mafra J, Miranda B, Yoda J, Sampaio A (2009) Test case selector: a tool for the selection of test cases (in Portuguese). In: Proceedings of SAST09, Gramado
Nogueira S, Cartaxo EG, Torres D, Aranha E, Marques R (2007) Model based test generation: an industrial experience. In: SAST 2007—1st Brazilian workshop on systematic and automated software testing, João Pessoa
Nebut C, Fleurey F, Le Traon Y, Jezequel JM (2006) Automatic test generation: a use case driven approach. IEEE Trans Softw Eng 32(3): 140–155
Nayak A, Samanta D (2011) Synthesis of test scenarios using UML activity diagrams. Softw Syst Model 10: 63–89. doi:10.1007/s10270-009-0133-4
Nogueira S, Sampaio A, Mota A (2008) Guided test generation from CSP models. In: Proceedings of the 5th ICTAC. Springer, Berlin, pp 258–273
Nogueira S, Sampaio A, Mota A (2011) Guided test generation from CSP models. Technical report, CIn-UFPE. http://www.cin.ufpe.br/~scn/reports/TR-ATG.pdf
Ostrand TJ, Balcer MJ (1988) The category-partition method for specifying and generating fuctional tests. Commun ACM 31(6): 676–686
Peleska J, Siegel M (1997) Test automation of safety-critical reactive systems. S Afr Comput J 19: 53–77
Parashkevov AN, Yantchev J (1996) ARC—a tool for efficient refinement and equivalence checking for CSP. In: IEEE international conference on algorithms and architectures for parallel processing (ICA3PP’96), pp 68–75
Rusu V, du Bousquet L, Jéron T (2000) An approach to symbolic test generation. In: IFM ’00: Proceedings of the second international conference on integrated formal methods. Springer, London, pp 338–357
Ryser J, Glinz M (1999) A scenario-based approach to validating and testing software systems using statecharts. In: 12th International conference on software and systems engineering and their applications (ICSSEA’99)
Roscoe AW, David Hopkins (2007) SVA: a tool for analysing shared-variable programmes. In: Proceedings of AVoCS 2007, pp 177–183
Roscoe AW (1998) The theory and practice of concurrency. Prentice Hall
Roscoe AW (2011) Understanding concurrent system. Springer, Berlin
Sampaio A et al. (2005) Software test program: a software residency experience. In: Proceedings of the 27th ICSE’05 (Education & training track). ACM Press, pp 611–612
Somé SS, Cheng X (2008) An approach for supporting system-level test scenarios generation from textual use cases. In: SAC ’08: Proceedings of the 2008 ACM symposium on applied computing. ACM, New York, pp 724–729
Scattergood JB (1998) The semantics and implementation of machine-readable CSP. PhD thesis, Oxford University Computing Laboratory
Schneider S (1999) Abstraction and testing. In: FM ’99, World Congress on formal methods, vol I. Springer, Berlin, pp 738–757
Sun J, Liu Y, Dong JS (2008) Model checking CSP revisited: introducing a process analysis toolkit. In: Proceedings of the third international symposium on leveraging applications of formal methods, verification and validation (ISoLA 2008). Communications in computer and information science, vol 17. Springer, Berlin, pp 307–322
Sun J, Liu Y, Dong JS, Chen C (2009) Integrating specification and programs for system modeling and verification. In: Proceedings of the 2009 third IEEE international symposium on theoretical aspects of software engineering, TASE ’09, Washington, DC, USA. IEEE Computer Society, pp 127–135
Sampaio A, Nogueira S, Mota A (2009) Compositional verification of input-output conformance via CSP refinement checking. In: ICFEM ’09: Proceedings of the 11th international conference on formal engineering methods (invited paper). Springer, Berlin, pp 20–48
Somé SS (2006) Supporting use case based requirements engineering. Inf Softw Technol 48(1): 43–58
Tretmans J, Belinfante A (1999) Automatic testing with formal methods. EuroSTAR’99: 7th European international conference on software testing, analysis & review, Nov 8–12, 1999, pp 8–12
Torres D et al. (2006) Motorola SpecNL: a hybrid system to generate NL descriptions from test case specifications. In: International conference on hybrid intelligent systems, Los Alamitos, CA, USA. IEEE Computer Society, p 45
Tretmans J (1996) Test generation with inputs, outputs and repetitive quiescence. Softw Concepts Tools 17(3): 103–120
Tretmans J (1999) Testing concurrent systems: a formal approach. In: Baeten JCM, Mauw S (eds) CONCUR’99. LNCS, vol 1664. Springer, Berlin, pp 46–65
Utting M, Pretschner A, Legeard B (2006) A taxonomy of model-based testing. In: Working paper series. University of Waikato, Department of Computer Science. April 2006
Veanes M, Campbell C, Grieskamp W, Schulte W, Tillmann N, Nachmanson L (2008) Model-based testing of object-oriented reactive systems with spec explorer. In: Hierons R, Bowen J, Harman M (eds) Formal methods and testing. Lecture notes in computer science, vol 4949. Springer, Berlin, pp 39–76
Williams C, Paradkar A (1999) Efficient regression testing of multi-panel systems. In: ISSRE ’99: Proceedings of the 10th international symposium on software reliability engineering, Washington, DC, USA. IEEE Computer Society, p 158
Weiglhofer M, Wotawa F (2008) “On the fly” input output conformance verification. In: Proceedings of the IASTED international conference on software engineering, Innsbruck, Austria. ACTA Press, pp 286–291
Author information
Authors and Affiliations
Corresponding author
Additional information
Dong Jin Song
Rights and permissions
About this article
Cite this article
Nogueira, S., Sampaio, A. & Mota, A. Test generation from state based use case models. Form Asp Comp 26, 441–490 (2014). https://doi.org/10.1007/s00165-012-0258-z
Received:
Revised:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-012-0258-z