{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T13:51:44Z","timestamp":1740145904773,"version":"3.37.3"},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2016,10,28]],"date-time":"2016-10-28T00:00:00Z","timestamp":1477612800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Braz Comput Soc"],"published-print":{"date-parts":[[2016,12]]},"DOI":"10.1186\/s13173-016-0048-1","type":"journal-article","created":{"date-parts":[[2016,10,28]],"date-time":"2016-10-28T05:31:41Z","timestamp":1477632701000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["An empirical study of test generation with BETA"],"prefix":"10.1186","volume":"22","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1571-0550","authenticated-orcid":false,"given":"Ernesto C. B.","family":"de Matos","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anamaria M.","family":"Moreira","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jo\u00e3o B.","family":"de Souza Neto","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,10,28]]},"reference":[{"key":"48_CR1","unstructured":"Legeard B, Peureux F, Utting M (2002) Automated Boundary Testing from Z and B. In: LarsHenrik E Lindsay PA (eds)FME 2002: Formal Methods\u2014Getting IT Right: International Symposium of Formal Methods Europe Copenhagen, Denmark, July 22\u201324, 2002 Proceedings, 21\u201340.. Springer Berlin Heidelberg, Berlin, Heidelberg. doi: http:\/\/dx.doi.org\/10.1007\/3540456147_2 ."},{"key":"48_CR2","first-page":"277","volume-title":"Proceedings of the 7th International Conference of B Users","author":"E Jaffuel","year":"2006","unstructured":"Jaffuel E, Legeard B (2006) LEIRIOS test generator: automated test generation from B models In: Proceedings of the 7th International Conference of B Users, 277\u2013280.. Springer, Berlin."},{"key":"48_CR3","first-page":"1","volume-title":"Int. Workshop on the B Method: from Research to Teaching","author":"F Dadeau","year":"2008","unstructured":"Dadeau F, Julliand J, Tissot R (2008) Leirios test generator: from research to teaching, through industry In: Int. Workshop on the B Method: from Research to Teaching, 1\u201316.. APCB, Nantes."},{"issue":"1","key":"48_CR4","first-page":"335","volume":"5","author":"PA Masson","year":"2010","unstructured":"Masson PA, Potet ML, Julliand J, Tissot R, Debois G, Legeard B, Chetali B, Bouquet F, Jaffuel E, Van Aertrick L, Andronick J, Haddad A (2010) An access control model based testing approach for smart card applications: Results of the POS\u00c9 project. J Inf Assur Secur 5(1): 335\u2013351.","journal-title":"J Inf Assur Secur"},{"key":"48_CR5","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/j.entcs.2004.12.009","volume":"111","author":"M Satpathy","year":"2005","unstructured":"Satpathy M, Leuschel M, Butler M (2005) ProTest: An automatic test environment for B Specifications. Electronic Notes Theoretical Comput Sci 111: 113\u2013136.","journal-title":"Electronic Notes Theoretical Comput Sci"},{"issue":"3","key":"48_CR6","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1145\/174146.154190","volume":"18","author":"P Stocks","year":"1993","unstructured":"Stocks P, Carrington D (1993) Test template framework: a specification-based testing case study. SIGSOFT Softw Eng Notes 18(3): 11\u201318.","journal-title":"SIGSOFT Softw Eng Notes"},{"key":"48_CR7","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-642-10373-5_9","volume-title":"Formal Methods and Software Engineering. LNCS","author":"M Cristi\u00e1","year":"2009","unstructured":"Cristi\u00e1 M, Monetti P (2009) Implementing and applying the Stocks-Carrington framework for model-based testing In: Formal Methods and Software Engineering. LNCS, 167\u2013185.. Springer, Berlin."},{"key":"48_CR8","unstructured":"Satpathy M, Butler M, Leuschel M, Ramesh S (2007) Automatic Testing from Formal Specifications. In: Gurevich Y Meyer B (eds)Tests and Proofs: First International Conference, TAP 2007, Zurich, Switzerland, February 12\u201313, 2007. Revised Papers, 95\u2013113.. Springer Berlin Heidelberg, Berlin, Heidelberg. doi: http:\/\/dx.doi.org\/10.1007\/9783540737704_6 ."},{"key":"48_CR9","doi-asserted-by":"crossref","unstructured":"Gupta A, Bhatia R (2010) Testing functional requirements using B model specifications. SIGSOFT Softw Eng Notes 35(2): 1\u20137. doi: http:\/\/dx.doi.org\/10.1145\/1734103.1734115 .","DOI":"10.1145\/1734103.1734115"},{"key":"48_CR10","doi-asserted-by":"crossref","unstructured":"Singh H, Conrad M, Sadeghipour S (1997) Test case design based on Z and the classification-tree method In: Formal Engineering Methods., 1997. Proceedings., First IEEE International Conference on, 81\u201390.. IEEE Computer Society. doi: http:\/\/dx.doi.org\/10.1109\/ICFEM.1997.630406 .","DOI":"10.1109\/ICFEM.1997.630406"},{"key":"48_CR11","unstructured":"Mendes E, Silveira DS, Lencastre M (2010) TESTIMONIUM: Um m\u00e9todo para gera\u00e7\u00e3o de casos de teste a partir de regras de neg\u00f3cio expressas em OCL In: Proceedings of the 4th Brazilian Workshop on Systematic and Automated Software Testing (SAST), Natal."},{"key":"48_CR12","unstructured":"Burton S, York H (2000) Automated testing from Z Specifications. Technical report, York. Report: University of York."},{"key":"48_CR13","unstructured":"Marinov D, Khurshid S (2001) TestEra: A novel framework for automated testing of Java programs In: Proceedings of the 16th IEEE International Conference on Automated Software Engineering, 22\u201331.. IEEE Computer Society, Washington. http:\/\/dl.acm.org\/citation.cfm?id=872023.872551 ."},{"key":"48_CR14","first-page":"1789","volume-title":"ECOOP 2002 - Object-Oriented Programming. LNCS","author":"Y Cheon","year":"2002","unstructured":"Cheon Y, Leavens G (2002) A simple and practical approach to unit testing: the JML and JUnit way In: ECOOP 2002 - Object-Oriented Programming. LNCS, 1789\u20131901.. Springer, Berlin."},{"key":"48_CR15","doi-asserted-by":"crossref","unstructured":"Amla N, Ammann P (1992) Using Z specifications in category partition testing In: Computer Assurance, 1992. COMPASS \u201992. \u2019Systems Integrity, Software Safety and Process Security: Building the System Right.\u2019, Proceedings of the Seventh Annual Conference on, 3\u201310, Gaithersburg. doi: http:\/\/dx.doi.org\/10.1109\/CMPASS.1992.235766 .","DOI":"10.1109\/CMPASS.1992.235766"},{"key":"48_CR16","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/BFb0024651","volume-title":"FME \u201993: Industrial-Strength Formal Methods. LNCS","author":"J Dick","year":"1993","unstructured":"Dick J, Faivre A (1993) Automating the generation and sequencing of test cases from model-based specifications In: FME \u201993: Industrial-Strength Formal Methods. LNCS, 268\u2013284.. Springer, Berlin."},{"issue":"2","key":"48_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1459352.1459354","volume":"41","author":"RM Hierons","year":"2009","unstructured":"Hierons RM, et al. (2009) Using formal specifications to support testing. ACM Comput Surv 41(2): 1\u201376.","journal-title":"ACM Comput Surv"},{"key":"48_CR18","first-page":"51","volume-title":"Z User Workshop. Workshops in Computing","author":"D Carrington","year":"1994","unstructured":"Carrington D, Stocks P (1994) A tale of two paradigms: formal methods and software testing In: Z User Workshop. Workshops in Computing, 51\u201368.. Springer, Cambridge."},{"key":"48_CR19","volume-title":"Formal Methods: Foundations and Applications. LNCS","author":"ECB Matos","year":"2012","unstructured":"Matos ECB, Moreira AM (2012) BETA: A B based testing approach In: Formal Methods: Foundations and Applications. LNCS.. Springer, Natal."},{"key":"48_CR20","unstructured":"Matos ECB, Moreira AM (2013) BETA: a tool for test case generation based on B specifications In: Proceedings of CBSoft Tools Session 2013, Bras\u00edlia."},{"key":"48_CR21","volume-title":"The B-book: assigning programs to meanings","author":"JR Abrial","year":"2005","unstructured":"Abrial JR (2005) The B-book: assigning programs to meanings. Cambridge University Press, New York."},{"key":"48_CR22","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511809163","volume-title":"Introduction to software testing","author":"P Ammann","year":"2008","unstructured":"Ammann P, Offutt J (2008) Introduction to software testing. Cambridge University Press, New York."},{"key":"48_CR23","unstructured":"Matos ECB, Moreira AM, Souza F, Coelho RdS (2010) Generating test cases from B specifications: an industrial case study In: Proceedings of 22nd IFIP International Conference on Testing Software and Systems, Natal."},{"key":"48_CR24","unstructured":"Matos ECB, Moreira AM, Souza Neto JB (2015) An empirical study of test generation with BETA In: Proceedings of the 9th Brazilian Workshop on Systematic and Automated Software Testing (SAST), Belo Horizonte."},{"key":"48_CR25","doi-asserted-by":"crossref","unstructured":"Andrews JH, Briand LC, Labiche Y (2005) Is mutation an appropriate tool for testing experiments? In: Proceedings of the 27th International Conference on Software Engineering, 402\u2013411.. ACM, New York. doi: http:\/\/dx.doi.org\/10.1145\/1062455.1062530 .","DOI":"10.1145\/1062455.1062530"},{"key":"48_CR26","volume-title":"M\u00e9t\u00e9or: A successful application of B in a large project. FM\u201999 \u2014 Formal Methods: World Congress on Formal Methods in the Development of Computing Systems","author":"P Behm","year":"1999","unstructured":"Behm P, Benoit P, Faivre A, Meynadier JM (1999) M\u00e9t\u00e9or: A successful application of B in a large project. FM\u201999 \u2014 Formal Methods: World Congress on Formal Methods in the Development of Computing Systems. Springer, Berlin."},{"key":"48_CR27","unstructured":"Lei Y, Tai KC (1998) InParameterOrder: a test generation strategy for pairwise testing In: The 3rd IEEE International Symposium on HighAssurance Systems Engineering, 254\u2013261.. IEEE Computer Society, Washington. http:\/\/dl.acm.org\/citation.cfm?id=645432.652389 ."},{"key":"48_CR28","doi-asserted-by":"publisher","first-page":"855","DOI":"10.1007\/978-3-540-45236-2_46","volume-title":"FME 2003: Formal Methods. LNCS","author":"M Leuschel","year":"2003","unstructured":"Leuschel M, Butler M (2003) ProB: A model checker for B In: FME 2003: Formal Methods. LNCS, 855\u2013874.. Springer, Berlin."},{"key":"48_CR29","unstructured":"Matos ECB (2016) BETA: a B based testing approach. PhD thesis, Federal University of Rio Grande do Norte, Natal."},{"key":"48_CR30","doi-asserted-by":"crossref","unstructured":"Marinescu R, Seceleanu C, Le Guen H, Pettersson P (2015) Chapter Three A Research Overview of ToolSupported Modelbased Testing of Requirementsbased Designs. In: Hurson AR (ed)Advances in Computers, 89\u2013140.. Elsevier, Amsterdam. doi: http:\/\/dx.doi.org\/10.1016\/bs.adcom.2015.03.003 . http:\/\/www.sciencedirect.com\/science\/article\/pii\/S0065245815000297 .","DOI":"10.1016\/bs.adcom.2015.03.003"},{"key":"48_CR31","doi-asserted-by":"crossref","unstructured":"Bernard E, Legeard B, Luck X, Peureux F (2004) Generation of test sequences from formal specifications: GSM 11-11 standard case study. Softw Pract Experience 34(10): 915\u2013948. doi: http:\/\/dx.doi.org\/10.1002\/spe.597 .","DOI":"10.1002\/spe.597"},{"key":"48_CR32","volume-title":"Introdu\u00e7\u00e3o Ao Teste de Software","author":"ME Delamaro","year":"2007","unstructured":"Delamaro ME, Maldonado JC, Jino M (2007) Introdu\u00e7\u00e3o Ao Teste de Software. Editora Campus \u2013 RJ, Rio de Janeiro, Brazil."},{"key":"48_CR33","unstructured":"Jia Y, Harman M (2008) MILU: A customizable, runtime-optimized higher order mutation testing tool for the full C language In: Practice and Research Techniques. TAIC PART \u201908. Testing: Academic Industrial Conference, 94\u201398.. IEEE Computer Society, Windsor. doi: http:\/\/dx.doi.org\/10.1109\/TAICPART.2008.18 ."},{"key":"48_CR34","volume-title":"Design of mutant operators for the C programming language","author":"H Agrawal","year":"1989","unstructured":"Agrawal H, DeMillo RA, Hathaway B, Hsu W, Hsu W, Krauser EW, Martin RJ, Mathur AP, Spafford E (1989) Design of mutant operators for the C programming language. Report SERC-TR-41-P, Purdue University, West Lafayette, Indiana."},{"key":"48_CR35","volume-title":"Programming in Lua","author":"R Ierusalimschy","year":"2013","unstructured":"Ierusalimschy R (2013) Programming in Lua. 3rd ed.. Lua. Org, Rio de Janeiro."},{"key":"48_CR36","unstructured":"Moreira AM, Ierusalimschy R (2013) Modeling the Lua API in B. Draft."},{"key":"48_CR37","unstructured":"Ierusalimschy R, Figueiredo LH, Celes W (2014) Lua 5.2 reference manual. http:\/\/www.lua.org\/manual\/5.2\/ . Accessed 28 Jan 2016."},{"key":"48_CR38","unstructured":"Moreira AM, Cleverton H, D\u00e9harbe D, de Matos ECB, Souza Neto JB, de Medeiros V (2015) Verifying code generation tools for the B-method using tests: a case study. In: Blanchette JC Kosmatov N (eds)Tests and Proofs: 9th International Conference, TAP 2015, Held as Part of STAF 2015, L\u2019Aquila, Italy, July 22\u201324, 2015. Proceedings, 76\u201391.. Springer International Publishing, Cham. doi: http:\/\/dx.doi.org\/10.1007\/9783319212159_5 ."},{"key":"48_CR39","unstructured":"D\u00e9harbe D, Medeiros Jr V (2013) Proposal: translation of B implementations to LLVM-IR. Brazilian Symposium on Formal Methods."},{"issue":"1","key":"48_CR40","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0743-1066(95)00147-6","volume":"28","author":"A Dovier","year":"1996","unstructured":"Dovier A, Omodeo EG, Pontelli E, Rossi G (1996) {log}: A language for programming in logic with finite sets. J Log Program 28(1): 1\u201344.","journal-title":"J Log Program"},{"key":"48_CR41","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/978-3-642-40561-7_16","volume-title":"Software Engineering and Formal Methods. LNCS","author":"M Cristi\u00e1","year":"2013","unstructured":"Cristi\u00e1 M, Rossi G, Frydman C (2013) {log} as a test case generator for the test template framework In: Software Engineering and Formal Methods. LNCS, 229\u2013243.. Springer, Berlin."},{"key":"48_CR42","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1016\/j.jss.2015.12.022","volume":"113","author":"VHS Durelli","year":"2016","unstructured":"Durelli VHS, Offutt J, Li N, Delamaro ME, Guo J, Shi Z, Ai X (2016) What to expect of predicates: An empirical analysis of predicates in real world programs. J Syst Softw 113: 324\u2013336.","journal-title":"J Syst Softw"},{"key":"48_CR43","unstructured":"Cristi\u00e1 M, Cuenca J, Frydman C (2014) Coverage criteria for logical specifications In: Proceedings of the 8th Brazilian Workshop on Systematic and Automated Software Testing (SAST), 11\u201320, Macei\u00f3."}],"container-title":["Journal of the Brazilian Computer Society"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1186\/s13173-016-0048-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1186\/s13173-016-0048-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1186\/s13173-016-0048-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,13]],"date-time":"2024-08-13T10:45:56Z","timestamp":1723545956000},"score":1,"resource":{"primary":{"URL":"https:\/\/journal-bcs.springeropen.com\/articles\/10.1186\/s13173-016-0048-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,10,28]]},"references-count":43,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2016,12]]}},"alternative-id":["48"],"URL":"https:\/\/doi.org\/10.1186\/s13173-016-0048-1","relation":{},"ISSN":["0104-6500","1678-4804"],"issn-type":[{"type":"print","value":"0104-6500"},{"type":"electronic","value":"1678-4804"}],"subject":[],"published":{"date-parts":[[2016,10,28]]},"article-number":"8"}}