{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T00:43:25Z","timestamp":1648514605953},"reference-count":65,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2014,7,1]],"date-time":"2014-07-01T00:00:00Z","timestamp":1404172800000},"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,7]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Many tools can check if a test set provides control coverage; they are, however, of little or no help when coverage is not achieved and the test set needs to be completed. In this paper, we describe how a formal characterisation of a coverage criterion can be used to generate test data; we present a procedure based on traditional programming techniques like normalisation, and weakest precondition calculation. It is a basis for automation using an algebraic theorem prover. In the worst situation, if automation fails to produce a specific test, we are left with a specification of the compliant test sets. Many approaches to model-based testing rely on formal models of a system under test. Our work, on the other hand, is not concerned with the use of abstract models for testing, but with coverage based on the text of programs.<\/jats:p>","DOI":"10.1007\/s00165-013-0279-2","type":"journal-article","created":{"date-parts":[[2013,5,28]],"date-time":"2013-05-28T05:45:02Z","timestamp":1369719902000},"page":"795-823","source":"Crossref","is-referenced-by-count":1,"title":["Test-data generation for control coverage by proof"],"prefix":"10.1145","volume":"26","author":[{"given":"Ana","family":"Cavalcanti","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of York, York, UK"}]},{"given":"Steve","family":"King","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of York, York, UK"}]},{"given":"Colin","family":"O\u2019Halloran","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Oxford, Oxford, UK"}]},{"given":"Jim","family":"Woodcock","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of York, York, UK"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-book: assigning progams to meanings","author":"Abrial J-R","year":"1996"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Adams MM Clayton PB (2005) Cost-effective formal verification for control systems. In: Lau K Banach R (eds) ICFEM 2005: formal methods and software engineering volume 3785 of Lecture Notes in Computer Science. Springer Berlin pp 465\u2013479","DOI":"10.1007\/11576280_32"},{"key":"e_1_2_1_2_3_2","unstructured":"Arthan R Caseley P O\u2019Halloran CM Smith A (2000) ClawZ: control laws in Z. In: 3rd international conference on formal engineering methods. IEEE Press pp 169\u2013176"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Agrawal H (1994) Dominators super blocks and program coverage. In: 21st ACM symposium on principles of programming languages pp 25\u201334","DOI":"10.1145\/174675.175935"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Ammann P Offutt J Huang H (2003) Coverage criteria for logical expressions. 14th international symposium on software reliability engineering pp 99\u2013107","DOI":"10.1109\/ISSRE.2003.1251034"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.345823"},{"key":"e_1_2_1_2_7_2","unstructured":"Burton S Clark J McDermid JA (2000) Testing proof and automation: an integrated approach. In: 1st international workshop on automated program analysis testing and verification (WAP-ATV 2000) pp 57\u201363"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Boshernitsan M Doong R Savoia A (2006) From Daikon to Agitator: lessons and challenges in building a commercial tool for developer testing. International symposium on software testing and analysis. ACM Press pp 169\u2013180","DOI":"10.1145\/1146238.1146258"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1049\/sej.1991.0040"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"publisher","DOI":"10.1016\/0164-1212(95)00089-5"},{"key":"e_1_2_1_2_11_2","unstructured":"Bullseye Testing Technology. C-Cover. http:\/\/www.bullseye.com"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Brucker AD Wolff B (2012) On theorem prover-based testing. Formal Aspects Comput","DOI":"10.1007\/s00165-012-0222-y"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Chang J-R Huang C-Y Li P-H (2012) An investigation of classification-based algorithms for modified condition\/decision coverage criteria. In: 6th international conference on software security and reliability. IEEE pp 127\u2013136","DOI":"10.1109\/SERE-C.2012.23"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1987.233196"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Cavalcanti ALC Harwood W Woodcock JCP (2006) Pointers and records in the unifying theories of programming. In: Dunne S Stoddart B (eds) Unifying theories of programming volume 4010 of Lecture Notes in Computer Science. Springer Berlin pp 200\u2013216","DOI":"10.1007\/11768173_12"},{"key":"e_1_2_1_2_16_2","unstructured":"Cavalcanti ALC King S O\u2019Halloran CM Woodcock JCP (2007) A scientific investigation of MC\/DC testing. Technical Report YCS-2007-411. University of York Department of Computer Science"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Chilenski JJ Miller SP (1994) Applicability of modified condition\/decision coverage to software testing. Softw Eng J 193\u2013200","DOI":"10.1049\/sej.1994.0025"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Clayton P Halloran CO\u2019 (2006) Using the compliance notation in industry. In: Cavalcanti ALC Sampaio ACA Woodcock JCP (eds) Refinement techniques in software engineering volume 3167 of Lecture Notes in Computer Science. Springer New York pp 269\u2013314","DOI":"10.1007\/11889229_7"},{"key":"e_1_2_1_2_19_2","unstructured":"Callahan J Schneider F Easterbrook S (1996) Specification-based testing using model checking. In: SPIN workshop"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/s001650050016"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Dick J Faivre A (1993) Automating the generation and sequencing of test cases from model-based specifications. In: Formal methods Europe volume 670 of Lecture Notes in Computer Science. Springer New York pp 268\u2013284","DOI":"10.1007\/BFb0024651"},{"key":"e_1_2_1_2_22_2","unstructured":"Dijkstra EW (1976) A discipline of programming. Prentice-Hall Englewood Cliffs"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Ernst MD Perkins JH Guo PJ McCamant S Pacheco C Tschantz MS Xiao C (2007) The Daikon system for dynamic detection of likely invariants. Sci Comput Program","DOI":"10.1016\/j.scico.2007.01.015"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/226155.226158"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/s001650050026"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Grabowski J Nielsen B (2004) Using model checking for reducing the cost of test generation. In: Grabowsk J Nielsen B (eds) Formal approaches to software testing volume 3395 of Lecture Notes in Computer Science. Springer Berlin pp 110\u2013124","DOI":"10.1007\/978-3-540-31848-4_8"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.4370030104"},{"key":"e_1_2_1_2_28_2","unstructured":"Hong HS Cha SD Lee I Sokolsky O Ural H (2003) Data flow testing as model checking. In: 25th international conference on software engineering pp 232\u2013242"},{"key":"e_1_2_1_2_29_2","unstructured":"Hoare CAR He J (1998) Unifying theories of programming. Prentice-Hall Englewood Cliffs"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Hong HS Lee I Sokolsky O Ural H (2002) A temporal logic based theory of test coverage and generation. In: International conference on tools and algorithms for construction and analysis of systems","DOI":"10.1007\/3-540-46002-0_23"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Helke S Neustupny T Santen T (1997) Automating test case generation from Z specifications with Isabelle. In: Bowen JP Hinchey MG Till D (eds) International conference of Z users volume 1212 of Lecture Notes in Computer Science. Springer New York pp 52\u201371","DOI":"10.1007\/BFb0027283"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Horwitz S (2002) Tool support for improving test coverage. In: Le M\u00e9tayer D (ed) European symposium on programming volume 2305 of Lecture Notes in Computer Science. Springer New York pp 162\u2013177","DOI":"10.1007\/3-540-45927-8_12"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0950-5849(00)00145-2"},{"key":"e_1_2_1_2_34_2","unstructured":"IPL. AdaTEST 95. http:\/\/www.ipl.com\/products\/tools\/pt600.php"},{"issue":"1","key":"e_1_2_1_2_35_2","first-page":"10","article-title":"ICL ProofPower","volume":"1","author":"Jones RB","year":"1992","journal-title":"BCS FACS FACTS Ser III"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.306"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"crossref","unstructured":"King JC (1975) A new approach to program testing. In: International conference on reliable software. ACM pp 228\u2013233","DOI":"10.1145\/390016.808444"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.57624"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.4370020405"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/322993.322996"},{"key":"e_1_2_1_2_41_2","unstructured":"Lira BO Cavalcanti ALC Sampaio ACA (2002) Automation of a normal form reduction strategy for object-oriented programming. In: Proceedings of the 5th Brazilian workshop on formal methods pp 193\u2013208"},{"key":"e_1_2_1_2_42_2","unstructured":"LDRA. LDRA TestBed. http:\/\/www.ldra.co.uk\/testbed.asp"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"crossref","unstructured":"Lee D Yannakakis M (1996) Principles and methods of testing finite state machines\u2014a survey. In: Proceedings of the IEEE vol 84 pp 1090\u20131126","DOI":"10.1109\/5.533956"},{"key":"e_1_2_1_2_44_2","unstructured":"Maharaj S (1999) Towards a method of test case extraction from correctness proofs. In: 14th international workshop on algebraic development techniques pp 45\u201346"},{"key":"e_1_2_1_2_45_2","unstructured":"Meisels I (2000) Software Manual for Windows Z\/EVES Version 2.1. ORA Canada TR-97-5505-04g"},{"key":"e_1_2_1_2_46_2","doi-asserted-by":"crossref","unstructured":"Michael CC McGraw G (1998) Automated software test data generation for complex programs. In: Automated software engineering pp 136\u2013146","DOI":"10.1109\/ASE.1998.732605"},{"key":"e_1_2_1_2_47_2","unstructured":"Morgan CC (1994) Programming from specifications 2nd edn. Prentice-Hall Englewood-Cliffs"},{"key":"e_1_2_1_2_48_2","doi-asserted-by":"crossref","unstructured":"Nipkow T Wenzel M Paulson LC (2002) Isabelle\/HOL: a proof assistant for higher-order logic. Springer Berlin","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_2_1_2_49_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2003.10.003"},{"key":"e_1_2_1_2_50_2","doi-asserted-by":"crossref","unstructured":"Owre S Rushby JM Shankar N (1992) PVS: a prototype verification system. In: Kapur D (ed) 11th international conference on automated deduction volume 607 of Lecture Notes in Artificial Intelligence. Springer New York pp 748\u2013752","DOI":"10.1007\/3-540-55602-8_217"},{"key":"e_1_2_1_2_51_2","doi-asserted-by":"crossref","unstructured":"Pandita R Xie T Tillmann N de Halleux J (2010) Guided test generation for coverage criteria. In 26th IEEE international conference on software maintenance. IEEE Computer Society pp 1\u201310","DOI":"10.1109\/ICSM.2010.5609565"},{"key":"e_1_2_1_2_52_2","unstructured":"Rational Software. PureCoverage. http:\/\/www.rational.com\/products\/pqc\/index.jsp"},{"key":"e_1_2_1_2_53_2","unstructured":"RTCA\/DO-178C\/ED-12C (2011) Software considerations in airborne systems and equipment certification"},{"key":"e_1_2_1_2_54_2","doi-asserted-by":"crossref","unstructured":"Rayadurgam S Heimdahl MPE (2003) Generating MC\/DC adequate test sequences through model checking. In: Software engineering workshop 28th annual NASA Goddard pp 91\u201396","DOI":"10.1109\/SEW.2003.1270730"},{"key":"e_1_2_1_2_55_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-009-0119-6"},{"key":"e_1_2_1_2_56_2","unstructured":"Singh H Conrad M Sadeghipour S (1997) Test case design based on Z and the classification-tree method. In: Hinchey MG Liu S (eds) 1st international conference on formal engineering methods (ICFEM 1997). IEEE Computer Society Press pp 81\u201390"},{"key":"e_1_2_1_2_57_2","unstructured":"Software Research Inc. TCAT. http:\/\/www.soft.com\/products\/web\/tcat.java.html"},{"key":"e_1_2_1_2_58_2","doi-asserted-by":"publisher","DOI":"10.1016\/0169-7552(94)00005-E"},{"key":"e_1_2_1_2_59_2","unstructured":"Tudor N Adams M Clayton P O\u2019Halloran CM (2004) Auto-coding\/auto-proving flight control software. In: IEEE digital avionics systems conference"},{"key":"e_1_2_1_2_60_2","doi-asserted-by":"publisher","DOI":"10.1109\/12.88472"},{"key":"e_1_2_1_2_61_2","volume-title":"Using Z\u2014specification, refinement, and proof","author":"Woodcock JCP","year":"1996"},{"key":"e_1_2_1_2_62_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.286420"},{"key":"e_1_2_1_2_63_2","doi-asserted-by":"crossref","unstructured":"Xia S Di Vito B Munoz C (2005) Automated test generation for engineering applications. In: Automated software engineering pp 283\u2013286","DOI":"10.1145\/1101908.1101951"},{"key":"e_1_2_1_2_64_2","doi-asserted-by":"crossref","unstructured":"Zeyda F Cavalcanti ALC (2012) Higher-order UTP in theories of object-orientation. In: 4th international symposium on unifying theories of programming Lecture Notes in Computer Science","DOI":"10.1007\/978-3-642-35705-3_10"},{"key":"e_1_2_1_2_65_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2010.02.010"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-013-0279-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-013-0279-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-013-0279-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T16:03:23Z","timestamp":1641485003000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-013-0279-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,7]]},"references-count":65,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2014,7]]}},"alternative-id":["10.1007\/s00165-013-0279-2"],"URL":"https:\/\/doi.org\/10.1007\/s00165-013-0279-2","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,7]]}}}