{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,13]],"date-time":"2025-01-13T18:40:06Z","timestamp":1736793606615,"version":"3.33.0"},"reference-count":50,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2007,2,9]],"date-time":"2007-02-09T00:00:00Z","timestamp":1170979200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2007,2,9]],"date-time":"2007-02-09T00:00:00Z","timestamp":1170979200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Autom Softw Eng"],"published-print":{"date-parts":[[2007,3]]},"DOI":"10.1007\/s10515-006-0004-y","type":"journal-article","created":{"date-parts":[[2007,2,8]],"date-time":"2007-02-08T20:34:40Z","timestamp":1170966880000},"page":"37-57","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["On the effect of test-suite reduction on automatically generated model-based tests"],"prefix":"10.1007","volume":"14","author":[{"given":"Mats P. E.","family":"Heimdahl","sequence":"first","affiliation":[]},{"given":"Devaraj","family":"George","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2007,2,9]]},"reference":[{"key":"4_CR1","unstructured":"NuS: The NuSMV Toolset. Available at http:\/\/nusmv.irst.itc.it\/ (2005)"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"Ammann, P.E., Black, P.E.: A specification-based coverage metric to evaluate test sets. In: Proceedings of the Fourth IEEE International Symposium on High-Assurance Systems Engineering. IEEE Computer Society (1999)","DOI":"10.6028\/NIST.IR.6403"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Ammann, P.E., Black, P.E., Majurski, W.: Using model checking to generate tests from specifications. In: Proceedings of the Second IEEE International Conference on Formal Engineering Methods (ICFEM\u201998), pp. 46\u201354. IEEE Computer Society (1998)","DOI":"10.6028\/NIST.IR.6166"},{"key":"4_CR4","unstructured":"Archer, M., Heitmeyer, C., Simsm S.: TAME: A PVS interface to simplify proofs for automata models. In: User Interfaces for Theorem Provers (1998)"},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Bensalem, S., Caspi, P., Parent-Vigouroux, C., Dumas, C.: A methodology for proving control systems with Lustre and PVS. In: Proceedings of the Seventh Working Conference on Dependable Computing for Critical Applications (DCCA 7), pp. 89\u2013107. IEEE Computer Society, San Jose, CA (1999)","DOI":"10.1109\/DCFTS.1999.814291"},{"key":"4_CR6","unstructured":"Blackburn, M.R., Busser, R.D., Fontaine, J.S.: Automatic generation of test vectors for SCR-style specifications. In: Proceedings of the 12th Annual Conference on Computer Assurance, COMPASS\u201997 (1997)"},{"key":"4_CR7","unstructured":"Callahan, J., Schneider, F., Easterbrook, S.: Specification-based testing using model checking. In: Proceedings of the SPIN Workshop (1996)"},{"issue":"7","key":"4_CR8","doi-asserted-by":"crossref","first-page":"498","DOI":"10.1109\/32.708566","volume":"24","author":"W. Chan","year":"1998","unstructured":"Chan, W., Anderson, R., Beame, P., Burns, S., Modugno, F., Notkin, D., Reese, J.: Model checking large software specifications. IEEE Trans. Softw. Eng. 24(7), 498\u2013520 (1998)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"4_CR9","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1049\/sej.1994.0025","volume":"9","author":"J. Chilenski","year":"1994a","unstructured":"Chilenski, J., Miller, S.: Applicability of modified condition\/decision coverage to software testing. Softw. Eng. J. 9, 193\u2013200 (1994a)","journal-title":"Softw. Eng. J."},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"Chilenski, J.J., Miller, S.P.: Applicability of modified condition\/decision coverage to software testing. Softw. Eng. J. 193\u2013200 (1994b)","DOI":"10.1049\/sej.1994.0025"},{"key":"4_CR11","unstructured":"Choi, Y., Heimdahl, M.: Model checking RSML-e requirements. In: Proceedings of the 7th IEEE\/IEICE International Symposium on High Assurance Systems Engineering, pp. 109\u2013118. Tokyo, Japan (2002)"},{"key":"4_CR12","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press (1999)"},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"Engels, A., Feijs, L.M.G., Mauw, S.: Test generation for intelligent networks using model checking. In: Proceedings of TACAS\u201997, LNCS 1217, pp. 384\u2013398. Springer (1997)","DOI":"10.1007\/BFb0035401"},{"key":"4_CR45","unstructured":"Esterel Technologies: SCADE suite product description. http:\/\/www.esterel-technologies.com\/v2\/scadeSuiteForSafetyCriticalSoftwareDevelopment\/index.html (2004)"},{"key":"4_CR14","unstructured":"FAA, C.A.S.T.: What is a \u201cdecision\u201d in application of modified condition\/decision coverage and decision coverage (DC)? Technical Report position paper (2002)"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"Frankl, P., Weiss, S.N.: An experimental comparison of the effectiveness of the all-uses and all-edges adequacy criteria. In: Proceedings of the symposium on Testing, analysis, and verification (1991)","DOI":"10.1145\/120807.120821"},{"key":"4_CR16","unstructured":"Garey, M., Johnson, D.: Computers and Intractability. Freeman, New York (1979)"},{"issue":"6","key":"4_CR17","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1145\/318774.318939","volume":"24","author":"A. Gargantini","year":"1999","unstructured":"Gargantini, A., Heitmeyer, C.: Using model checking to generate tests from requirements specifications. Softw. Eng. Notes 24(6), 146\u2013162 (1999)","journal-title":"Softw. Eng. Notes"},{"issue":"3","key":"4_CR18","doi-asserted-by":"crossref","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O. Grumberg","year":"1994","unstructured":"Grumberg, O., Long, D.E.: Model checking and modular verification. ACM Trans. Program. Lang. Syst. 16(3), 843\u2013871 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"3","key":"4_CR19","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D. Harel","year":"1987","unstructured":"Harel, D.: Statecharts: A visual formalism for complex systems. Sci. Comput. Program. 8(3), 231\u2013274 (1987)","journal-title":"Sci. Comput. Program."},{"issue":"4","key":"4_CR20","doi-asserted-by":"crossref","first-page":"403","DOI":"10.1109\/32.54292","volume":"16","author":"D. Harel","year":"1990","unstructured":"Harel, D., Lachover, H., Naamad, A., Pnueli, A., Politi, M., Sherman, R., Shtull-Trauring, A., Trakhtenbrot, M. STATEMATE: A working environment for the development of complex reactive systems. IEEE Trans. Softw. Eng. 16(4), 403\u2013414 (1990)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"4_CR21","unstructured":"Hayhurst, K., Veerhusen, D., Rierson, L.: A practical tutorial on modified condition\/decision coverage. Technical Report TM-2001-210876, NASA (2001)"},{"key":"4_CR22","unstructured":"Heimdahl, M.P., Devaraj, G.: Test-suite reduction for model based tests: Effects on test quality and implications for testing. In: Proceedings of the 19th IEEE International Conference on Automated Software Engineering (ASE). Linz, Austria (2004)"},{"key":"4_CR23","unstructured":"Heimdahl, M.P., Devaraj, G., Weber, R.J.: Specification test coverage adequacy criteria = specification test generation inadequacy criteria? In: Proceedings of the Eighth IEEE International Symposium on High Assurance Systems Engineering (HASE). Tampa, Florida (2004)"},{"key":"4_CR24","unstructured":"Heimdahl, M.P., Rayadurgam, S., Visser, W.: Specification centered testing. In: Second International Workshop on Analysis, Testing and Verification (2001)"},{"key":"4_CR25","doi-asserted-by":"crossref","unstructured":"Heimdahl, M.P., Rayadurgam, S., Visser, W., Devaraj, G., Gao, J.: Auto-generating test sequences using model checkers: A case study\u2019. In: 3rd International Worshop on Formal Approaches to Testing of Software (FATES 2003) (2003)","DOI":"10.1007\/978-3-540-24617-6_4"},{"issue":"6","key":"4_CR26","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1109\/32.508311","volume":"22","author":"M.P.E. Heimdahl","year":"1996","unstructured":"Heimdahl, M.P.E., Leveson, N.G.: Completeness and consistency in hierarchical state-base requirements. IEEE Trans. Softw. Eng. 22(6), 363\u2013377 (1996)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"4_CR27","doi-asserted-by":"crossref","unstructured":"Heitmeyer, C., Bull, A., Gasarch, C., Labaw, B.: SCR*: A toolset for specifying and analyzing requirements. In: Proceedings of the Tenth Annual Conference on Computer Assurance, COMPASS 95 (1995)","DOI":"10.21236\/ADA465318"},{"issue":"3","key":"4_CR28","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1145\/234426.234431","volume":"5","author":"C. Heitmeyer","year":"1996","unstructured":"Heitmeyer, C., Jeffords, R., Labaw, B.: Automated consistency checking of requirements specifications. ACM Trans. Softw. Eng. Methodol. 5(3), 231\u2013261 (1996)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"issue":"11","key":"4_CR29","doi-asserted-by":"crossref","first-page":"927","DOI":"10.1109\/32.730543","volume":"24","author":"C. Heitmeyer","year":"1998","unstructured":"Heitmeyer, C., Jr, J.K., Labaw, B., Archer, M., Bharadwaj, R.: Using abstraction and model checking to detect safety violations in requirements specifications. IEEE Trans. Softw. Eng. 24(11), 927\u2013948 (1998)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"4_CR30","unstructured":"Hong, H.S., Cha, S.D., Lee, I., Sokolsky, O., Ural, H.: Data flow testing as model checking. In: Proceedings of the International Conference on Software Engineering. Portland, Oregon (2003)"},{"key":"4_CR31","doi-asserted-by":"crossref","unstructured":"Hong, H.S., Lee, I., Sokolsky, O., Ural, H.: A temporal logic based theory of test coverage and generation. In: Proceedings of the International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS\u201902). Grenoble, France (2002)","DOI":"10.1007\/3-540-46002-0_23"},{"key":"4_CR32","doi-asserted-by":"crossref","unstructured":"Jasper, R., Brennan, M., Williamson, K., Currier, B., Zimmerman, D.: Test data generation and feasible path analysis. In: Proceedings of International Symposium on Software Testing and Analysis (1994), pp. 95\u2013107.","DOI":"10.1145\/186258.187150"},{"issue":"3","key":"4_CR33","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1109\/TSE.2003.1183927","volume":"29","author":"J.A. Jones","year":"2003","unstructured":"Jones, J.A., Harrold, M.J.: Test-suite reduction and prioritization for modified condition\/decision coverage. IEEE Trans. Softw. Eng. 29(3), 195\u2013209 (2003)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"4_CR34","unstructured":"Lee, E.A.: Overview of the Ptolemy Project. Technical Report Technical Memorandum UCB\/ERL M03\/25, University of California, Berkeley, CA, 94720, USA (2003)"},{"issue":"9","key":"4_CR35","doi-asserted-by":"crossref","first-page":"684","DOI":"10.1109\/32.317428","volume":"20","author":"N. Leveson","year":"1994","unstructured":"Leveson, N., Heimdahl, M., Hildreth, H., Reese, J.: Requirements specification for process-control systems. IEEE Trans. Softw. Eng. 20(9), 684\u2013706 (1994)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"4_CR36","unstructured":"Mathworks Inc.: Mathworks Inc. Simulink Product Web Site. via the world-wide-web: http:\/\/www.mathworks.com."},{"key":"4_CR37","unstructured":"Offutt, A.J., Xiong, Y., Liu, S.: Criteria for generating specification-based tests. In: Proceedings of the Fifth IEEE International Conference on Engineering of Complex Computer Systems (ICECCS\u201999) (1999)"},{"key":"4_CR38","unstructured":"Owre, S., Shankar, N., Rushby, J.: The PVS specification language. Computer Science Laboratory; SRI International, Menlo Park, CA 94025, beta relese edition (1993)"},{"key":"4_CR39","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: Applications of temporal logic to specification and verification of reactive systems: A survey of current trends. Lecture Notes in Computer Science Number 224, pp. 510\u2013584 (1986)","DOI":"10.1007\/BFb0027047"},{"key":"4_CR40","unstructured":"Rayadurgam, S.: Automatic test-case generation from formal models of software. Ph.D. thesis, University of Minnesota (2003)"},{"key":"4_CR41","doi-asserted-by":"crossref","unstructured":"Rayadurgam, S., Heimdahl, M.P.: Coverage based test-case generation using model checkers. In: Proceedings of the 8th Annual IEEE International Conference and Workshop on the Engineering of Computer Based Systems (ECBS 2001), pp. 83\u201391. IEEE Computer Society (2001a)","DOI":"10.1109\/ECBS.2001.922409"},{"key":"4_CR42","unstructured":"Rayadurgam, S., Heimdahl, M.P.: Test-sequence generation from formal requirement models. In: Proceedings of the 6th IEEE International Symposium on the High Assurance Systems Engineering (HASE 2001). Boca Raton, Florida (2001b)"},{"key":"4_CR43","doi-asserted-by":"crossref","unstructured":"Rothermel, G., Harrold, M., Ostrin, J., Hong, C.: An empirical study of the effects of minimization on the fault detection capabilities of test suites. In: Proceedings of the International Conference on Software Maintenance, pp. 34\u201343 (1998)","DOI":"10.1109\/ICSM.1998.738487"},{"key":"4_CR44","unstructured":"RTCA: Software Considerations In Airborne Systems and Equipment Certification. RTCA (1992)"},{"key":"4_CR46","unstructured":"Thompson, J.M., Heimdahl, M.P.: An integrated development environment prototyping safety critical systems. In: Tenth IEEE International Workshop on Rapid System Prototyping (RSP) 99, (1999), pp. 172\u2013177."},{"key":"4_CR47","doi-asserted-by":"crossref","unstructured":"Thompson, J.M., Heimdahl, M.P., Miller, S.P.: Specification based prototyping for embedded systems. In: Seventh ACM SIGSOFT Symposium on the Foundations on Software Engineering, pp. 163\u2013179 (1999)","DOI":"10.1007\/3-540-48166-4_11"},{"key":"4_CR48","unstructured":"Whalen, M.W., Heimdahl, M.P.: On the requirements of high-integrity code generation. In: 4th IEEE International Symposium on High Assurance Systems Engineering, Vol. LNCS yyy, (1999), pp. 217\u2013226."},{"key":"4_CR49","unstructured":"Wong, W., Horgan, J., Mathur, A., Pasquini, A.: Test set size minimization and fault detection effectiveness: a case study in a space application. In: Proceedings of the 21st Annual International Computer Software and Applications Conference, (1997), pp. 522\u2013528."},{"issue":"4","key":"4_CR50","doi-asserted-by":"crossref","first-page":"347","DOI":"10.1002\/(SICI)1097-024X(19980410)28:4<347::AID-SPE145>3.0.CO;2-L","volume":"28","author":"W. Wong","year":"1998","unstructured":"Wong, W., Horgan, J., London, S., Mathur, A.: Effect of test set minimization on fault detection effectiveness. Softw. Pract. Exp. 28(4), 347\u2013369 (1998)","journal-title":"Softw. Pract. Exp."}],"container-title":["Automated Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10515-006-0004-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10515-006-0004-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10515-006-0004-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10515-006-0004-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,13]],"date-time":"2025-01-13T18:04:34Z","timestamp":1736791474000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10515-006-0004-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,2,9]]},"references-count":50,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2007,3]]}},"alternative-id":["4"],"URL":"https:\/\/doi.org\/10.1007\/s10515-006-0004-y","relation":{},"ISSN":["0928-8910","1573-7535"],"issn-type":[{"type":"print","value":"0928-8910"},{"type":"electronic","value":"1573-7535"}],"subject":[],"published":{"date-parts":[[2007,2,9]]},"assertion":[{"value":"9 February 2007","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}