{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,24]],"date-time":"2026-02-24T06:11:31Z","timestamp":1771913491742,"version":"3.50.1"},"reference-count":62,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2014,5,1]],"date-time":"2014-05-01T00:00:00Z","timestamp":1398902400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2014,5]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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\u2013output 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.<\/jats:p>","DOI":"10.1007\/s00165-012-0258-z","type":"journal-article","created":{"date-parts":[[2012,8,1]],"date-time":"2012-08-01T21:18:13Z","timestamp":1343855893000},"page":"441-490","source":"Crossref","is-referenced-by-count":42,"title":["Test generation from state based use case models"],"prefix":"10.1145","volume":"26","author":[{"given":"Sidney","family":"Nogueira","sequence":"first","affiliation":[{"name":"Mobile Devices R&amp;D Motorola Industrial Ltda, Rod SP 340, Km 128, 7 A, 13820 000, Jaguariuna, SP, Brazil"},{"name":"Centro de Inform\u00e1tica, Universidade Federal de Pernambuco, Caixa Postal 7851, 50732-970, Recife, PE, Brazil"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Augusto","family":"Sampaio","sequence":"additional","affiliation":[{"name":"Centro de Inform\u00e1tica, Universidade Federal de Pernambuco, Caixa Postal 7851, 50732-970, Recife, PE, Brazil"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexandre","family":"Mota","sequence":"additional","affiliation":[{"name":"Centro de Inform\u00e1tica, Universidade Federal de Pernambuco, Caixa Postal 7851, 50732-970, Recife, PE, Brazil"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","unstructured":"ISO 8807:1989 (1989) LOTOS: a formal description technique based on the temporal ordering of observational behaviour. ISO"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Alur R Henzinger TA Kupferman O Vardi MY (1998) Alternating refinement relations","DOI":"10.1007\/BFb0055622"},{"key":"e_1_2_1_2_3_2","unstructured":"Andrade W et\u00a0al. (2007) Interruption test case generation for mobile phone applications (in Portuguese). In: XXV Brazilian symposium in computer networks and distributed systems"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Bertolino A (2007) Software testing research: achievements challenges dreams. In: FOSE \u201907: 2007 future of software engineering. IEEE Computer Society Washington pp 85\u2013103","DOI":"10.1109\/FOSE.2007.25"},{"key":"e_1_2_1_2_5_2","unstructured":"Bezerra R (2011) Extra\u00e7\u00e3o Autom\u00e1tica de Modelos CSP a partir de Casos de Uso. Master\u2019s thesis CIn-UFPE (Center of Informatics of Federal University of Pernambuco)"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/949952.940120"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"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","DOI":"10.1007\/b137241"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-002-0004-8"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"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\u2013244","DOI":"10.1109\/ICST.2010.41"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"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 \u201908: Proceedings of the 2008 ACM symposium on applied computing. ACM New York pp 1540\u20131544","DOI":"10.1145\/1363686.1364045"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Cavalcanti A Gaudel M-C (2007) Testing for refinement in CSP. In: ICFEM. LNCS vol 4789. Springer Berlin pp 151\u2013170","DOI":"10.1007\/978-3-540-76650-6_10"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Colvin R Hayes IJ (2009) CSP with hierarchical state. In: IFM \u201909: Proceedings of the 7th international conference on integrated formal methods. Springer Berlin pp 118\u2013135","DOI":"10.1007\/978-3-642-00255-7_9"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/503271.503252"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF03192554"},{"key":"e_1_2_1_2_15_2","unstructured":"Cabral G Tamai T (2008) Requirement-based testing through formal methods. In: Proceedings of TESTCOM-FATES 2008\u2014short papers"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"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\u2013133","DOI":"10.1007\/978-3-642-10452-7_9"},{"key":"e_1_2_1_2_17_2","unstructured":"dos Prazeres Farias J (2008) NLScripts: composi\u00e7\u00e3o assistida de scripts de testes a partir de descri\u00e7\u00f5es em linguagem natural controlada (in Portuguese). Master\u2019s thesis CIn-UFPE (Center of Informatics of Federal University of Pernambuco) June 2008"},{"key":"e_1_2_1_2_18_2","first-page":"128","article-title":"State\/event-based software model checking","volume":"2999","author":"Edmund SC","year":"2004","journal-title":"In: Integr Form Methods"},{"key":"e_1_2_1_2_19_2","unstructured":"Ferreira F Neves L Silva M Borba P (2010) TaRGeT: a model based product line testing tool. In: Proceedings of CBSoft 2010\u2014tools panel"},{"key":"e_1_2_1_2_20_2","unstructured":"Formal Systems (2005) Failures-divergence refinement\u2014FDR2 user manual. Formal Systems (Europe) Ltd June 2005"},{"key":"e_1_2_1_2_21_2","unstructured":"Formal Systems (2011) Formal systems Web site. http:\/\/fsel.com. Sep 2011"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Gois FNB (2010) Test script diagram\u2014Um modelo para gera\u00e7\u00e3o de scripts de testes (in Portuguese). Master\u2019s thesis Universidade de Fortaleza (UNIFOR)","DOI":"10.5753\/sbqs.2010.15422"},{"key":"e_1_2_1_2_23_2","unstructured":"Object Group (2007) OMG unified modeling language (OMG UML). Superstructure V2.1.2. Technical report"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/1459352.1459354"},{"key":"e_1_2_1_2_25_2","volume-title":"Algebraic theory of processes","author":"Hennessy M","year":"1988"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11334-005-0006-0"},{"issue":"4","key":"e_1_2_1_2_27_2","first-page":"297","article-title":"TGV: theory, principles and algorithms","volume":"7","author":"Jard C","year":"2005","journal-title":"A tool for the automatic synthesis of conformance test cases for non-deterministic reactive systems. Int J Softw Tools Technol Transf"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"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\u2013134 Nov 2001","DOI":"10.1109\/ASE.2001.989798"},{"key":"e_1_2_1_2_29_2","unstructured":"Leit\u00e3o D et\u00a0al. (2007) NLForSpec: translating natural language descriptions into formal test case specifications. In: SEKE. Knowledge Systems Institute Graduate School pp 129\u2013134"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Lima L Iyoda J Sampaio A Aranha E (2009) Test case prioritization based on data reuse an experimental study. In: ESEM \u201909: Proceedings of the 2009 3rd international symposium on empirical software engineering and measurement Washington DC USA. IEEE Computer Society pp 279\u2013290","DOI":"10.1109\/ESEM.2009.5315980"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Mota A Borba P Sampaio A (2002) Mechanical abstraction of CSP-Z processes. In: FME 2002: formal methods\u2014getting IT right. LNCS vol 2391. Springer Berlin pp 163\u2013183 Jan 2002","DOI":"10.1007\/3-540-45614-7_10"},{"key":"e_1_2_1_2_32_2","unstructured":"Milner R (1989) Communication and concurrency. Prentice Hall"},{"key":"e_1_2_1_2_33_2","unstructured":"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"},{"key":"e_1_2_1_2_34_2","unstructured":"Nogueira S Cartaxo EG Torres D Aranha E Marques R (2007) Model based test generation: an industrial experience. In: SAST 2007\u20141st Brazilian workshop on systematic and automated software testing Jo\u00e3o Pessoa"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2006.22"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-009-0133-4"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"crossref","unstructured":"Nogueira S Sampaio A Mota A (2008) Guided test generation from CSP models. In: Proceedings of the 5th ICTAC. Springer Berlin pp 258\u2013273","DOI":"10.1007\/978-3-540-85762-4_18"},{"key":"e_1_2_1_2_38_2","unstructured":"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"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/62959.62964"},{"key":"e_1_2_1_2_40_2","first-page":"53","article-title":"Test automation of safety-critical reactive systems","volume":"19","author":"Peleska J","year":"1997","journal-title":"S Afr Comput J"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"crossref","unstructured":"Parashkevov AN Yantchev J (1996) ARC\u2014a tool for efficient refinement and equivalence checking for CSP. In: IEEE international conference on algorithms and architectures for parallel processing (ICA3PP\u201996) pp 68\u201375","DOI":"10.1109\/ICAPP.1996.562859"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"crossref","unstructured":"Rusu V du Bousquet L J\u00e9ron T (2000) An approach to symbolic test generation. In: IFM \u201900: Proceedings of the second international conference on integrated formal methods. Springer London pp 338\u2013357","DOI":"10.1007\/3-540-40911-4_20"},{"key":"e_1_2_1_2_43_2","unstructured":"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\u201999)"},{"key":"e_1_2_1_2_44_2","unstructured":"Roscoe AW David Hopkins (2007) SVA: a tool for analysing shared-variable programmes. In: Proceedings of AVoCS 2007 pp 177\u2013183"},{"key":"e_1_2_1_2_45_2","unstructured":"Roscoe AW (1998) The theory and practice of concurrency. Prentice Hall"},{"key":"e_1_2_1_2_46_2","volume-title":"Understanding concurrent system","author":"Roscoe AW","year":"2011"},{"key":"e_1_2_1_2_47_2","doi-asserted-by":"crossref","unstructured":"Sampaio A et\u00a0al. (2005) Software test program: a software residency experience. In: Proceedings of the 27th ICSE\u201905 (Education & training track). ACM Press pp 611\u2013612","DOI":"10.1145\/1062455.1062565"},{"key":"e_1_2_1_2_48_2","doi-asserted-by":"crossref","unstructured":"Som\u00e9 SS Cheng X (2008) An approach for supporting system-level test scenarios generation from textual use cases. In: SAC \u201908: Proceedings of the 2008 ACM symposium on applied computing. ACM New York pp 724\u2013729","DOI":"10.1145\/1363686.1363857"},{"key":"e_1_2_1_2_49_2","unstructured":"Scattergood JB (1998) The semantics and implementation of machine-readable CSP. PhD thesis Oxford University Computing Laboratory"},{"key":"e_1_2_1_2_50_2","doi-asserted-by":"crossref","unstructured":"Schneider S (1999) Abstraction and testing. In: FM \u201999 World Congress on formal methods vol I. Springer Berlin pp 738\u2013757","DOI":"10.1007\/3-540-48119-2_41"},{"key":"e_1_2_1_2_51_2","doi-asserted-by":"crossref","unstructured":"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\u2013322","DOI":"10.1007\/978-3-540-88479-8_22"},{"key":"e_1_2_1_2_52_2","doi-asserted-by":"crossref","unstructured":"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 \u201909 Washington DC USA. IEEE Computer Society pp 127\u2013135","DOI":"10.1109\/TASE.2009.32"},{"key":"e_1_2_1_2_53_2","doi-asserted-by":"crossref","unstructured":"Sampaio A Nogueira S Mota A (2009) Compositional verification of input-output conformance via CSP refinement checking. In: ICFEM \u201909: Proceedings of the 11th international conference on formal engineering methods (invited paper). Springer Berlin pp 20\u201348","DOI":"10.1007\/978-3-642-10373-5_2"},{"key":"e_1_2_1_2_54_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2005.02.006"},{"key":"e_1_2_1_2_55_2","unstructured":"Tretmans J Belinfante A (1999) Automatic testing with formal methods. EuroSTAR\u201999: 7th European international conference on software testing analysis & review Nov 8\u201312 1999 pp 8\u201312"},{"key":"e_1_2_1_2_56_2","doi-asserted-by":"crossref","unstructured":"Torres D et\u00a0al. (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","DOI":"10.1109\/HIS.2006.264928"},{"issue":"3","key":"e_1_2_1_2_57_2","first-page":"103","article-title":"Test generation with inputs, outputs and repetitive quiescence","volume":"17","author":"Tretmans J","year":"1996","journal-title":"Softw Concepts Tools"},{"key":"e_1_2_1_2_58_2","doi-asserted-by":"crossref","unstructured":"Tretmans J (1999) Testing concurrent systems: a formal approach. In: Baeten JCM Mauw S (eds) CONCUR\u201999. LNCS vol 1664. Springer Berlin pp 46\u201365","DOI":"10.1007\/3-540-48320-9_6"},{"key":"e_1_2_1_2_59_2","unstructured":"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"},{"key":"e_1_2_1_2_60_2","doi-asserted-by":"crossref","unstructured":"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\u201376","DOI":"10.1007\/978-3-540-78917-8_2"},{"key":"e_1_2_1_2_61_2","unstructured":"Williams C Paradkar A (1999) Efficient regression testing of multi-panel systems. In: ISSRE \u201999: Proceedings of the 10th international symposium on software reliability engineering Washington DC USA. IEEE Computer Society p 158"},{"key":"e_1_2_1_2_62_2","unstructured":"Weiglhofer M Wotawa F (2008) \u201cOn the fly\u201d input output conformance verification. In: Proceedings of the IASTED international conference on software engineering Innsbruck Austria. ACTA Press pp 286\u2013291"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-012-0258-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-012-0258-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-012-0258-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,6]],"date-time":"2025-04-06T12:32:00Z","timestamp":1743942720000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-012-0258-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,5]]},"references-count":62,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2014,5]]}},"alternative-id":["10.1007\/s00165-012-0258-z"],"URL":"https:\/\/doi.org\/10.1007\/s00165-012-0258-z","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,5]]}}}