{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,5,9]],"date-time":"2022-05-09T23:29:12Z","timestamp":1652138952582},"reference-count":37,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2015,3,24]],"date-time":"2015-03-24T00:00:00Z","timestamp":1427155200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Innovations Syst Softw Eng"],"published-print":{"date-parts":[[2015,12]]},"DOI":"10.1007\/s11334-015-0245-7","type":"journal-article","created":{"date-parts":[[2015,3,23]],"date-time":"2015-03-23T06:37:08Z","timestamp":1427092628000},"page":"233-242","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Bridging the gap between test cases and requirements by abstract testing"],"prefix":"10.1007","volume":"11","author":[{"given":"Florian","family":"Merz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carsten","family":"Sinz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hendrik","family":"Post","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Gorges","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Kropf","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,3,24]]},"reference":[{"key":"245_CR1","unstructured":"Arnold D (2009) An open framework for the specification and execution of a testable requirements model. Ph.D. thesis, Ottawa-Carleton Institute for Computer Science, Carleton University"},{"key":"245_CR2","doi-asserted-by":"crossref","unstructured":"Arnold D, Corriveau JP, Shi W (2010) Modeling and validating requirements using executable contracts and scenarios. In: Proceedings of the 8th international conference on software engineering research, management and applications (SERA)","DOI":"10.1109\/SERA.2010.46"},{"key":"245_CR3","doi-asserted-by":"crossref","unstructured":"Biere A, Cimatti A, Clarke EM, Zhu Y (1999) Symbolic model checking without BDDs. In: Proceedings of the 5th international conference on tools and algorithms for construction and analysis of systems (TACAS). Springer, London, pp 193\u2013207","DOI":"10.1007\/3-540-49059-0_14"},{"key":"245_CR4","doi-asserted-by":"crossref","unstructured":"Bringmann E, Kr\u00e4mer A (2008) Model-based testing of automotive systems. In: ICST, pp 485\u2013493","DOI":"10.1109\/ICST.2008.45"},{"key":"245_CR5","unstructured":"Burnstein I (2003) Practical software testing: a process-oriented approach. Springer, Berlin"},{"key":"245_CR6","doi-asserted-by":"crossref","unstructured":"Chaki S, Clarke E, Groce A, Jha S, Veith H (2003) Modular verification of software components in C. In: Proceedings of the 25th international conference on software engineering (ICSE). IEEE Computer Society, pp 385\u2013395","DOI":"10.1109\/ICSE.2003.1201217"},{"issue":"7","key":"245_CR7","doi-asserted-by":"crossref","first-page":"651","DOI":"10.1109\/32.935856","volume":"27","author":"M Chechik","year":"2001","unstructured":"Chechik M, Gannon JD (2001) Automatic analysis of consistency between requirements and designs. IEEE Trans Softw Eng 27(7):651\u2013672","journal-title":"IEEE Trans Softw Eng"},{"key":"245_CR8","doi-asserted-by":"crossref","unstructured":"Clarke E, Kroening D, Lerda F (2004) A tool for checking ANSI-C programs. In: Jensen K, Podelski A (eds) Tools and algorithms for the construction and analysis of systems (TACAS). LNCS, vol 2988. Springer, Berlin, pp 168\u2013176","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"245_CR9","doi-asserted-by":"crossref","unstructured":"Cousot P (2007) Proving the absence of run-time errors in safety-critical avionics code. In: Proceedings of the 7th ACM and IEEE international conference on embedded software (EMSOFT). ACM, New York, pp 7\u20139","DOI":"10.1145\/1289927.1289932"},{"key":"245_CR10","doi-asserted-by":"crossref","unstructured":"Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the fourth ACM symposium on principles of programming languages (POPL), Los Angeles, California, January 1977, pp 238\u2013252","DOI":"10.1145\/512950.512973"},{"key":"245_CR11","doi-asserted-by":"crossref","unstructured":"Cousot P, Cousot R, Feret J, Mauborgne L, Min\u00e9 A, Monniaux D, Rival X (2005) The ASTRE\u00c9 analyzer. In: Proceedings of the programming languages and systems, 14th European symposium on programming (ESOP), Edinburgh, UK, April 4\u20138, pp 21\u201330","DOI":"10.1007\/978-3-540-31987-0_3"},{"issue":"3","key":"245_CR12","doi-asserted-by":"crossref","first-page":"296","DOI":"10.1145\/287000.287023","volume":"7","author":"J Crow","year":"1998","unstructured":"Crow J, Di Vito B (1998) Formalizing space shuttle software requirements: four case studies. ACM Trans Softw Eng Methodol 7(3):296\u2013332","journal-title":"ACM Trans Softw Eng Methodol"},{"key":"245_CR13","unstructured":"Das Verisoft Projekt. http:\/\/www.verisoft.de . Accessed 22 Sept 2014"},{"key":"245_CR14","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1109\/32.588520","volume":"23","author":"B Dutertre","year":"1997","unstructured":"Dutertre B, Stavridou V (1997) Formal requirements analysis of an avionics control system. IEEE Trans Softw Eng 23:267\u2013278","journal-title":"IEEE Trans Softw Eng"},{"issue":"6","key":"245_CR15","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1218776.1218787","volume":"31","author":"G Fraser","year":"2006","unstructured":"Fraser G, Wotawa F (2006) Property relevant software testing with model-checkers. SIGSOFT Softw Eng Notes 31(6):1\u201310","journal-title":"SIGSOFT Softw Eng Notes"},{"issue":"5","key":"245_CR16","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1109\/MS.2002.1032845","volume":"19","author":"D Graham","year":"2002","unstructured":"Graham D (2002) Requirements and testing: seven missing-link myths. Softw IEEE 19(5):15\u201317","journal-title":"Softw IEEE"},{"issue":"1","key":"245_CR17","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1109\/TSE.2007.70772","volume":"34","author":"CL Heitmeyer","year":"2008","unstructured":"Heitmeyer CL, Archer M, Leonard EI, McLean J (2008) Applying formal methods to a certifiably secure software system. IEEE Trans Softw Eng 34(1):82\u201398","journal-title":"IEEE Trans Softw Eng"},{"issue":"3","key":"245_CR18","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1145\/234426.234431","volume":"5","author":"CL Heitmeyer","year":"1996","unstructured":"Heitmeyer CL, Jeffords RD, Labaw BG (1996) Automated consistency checking of requirements specifications. ACM Trans Softw Eng Methodol 5(3):231\u2013261","journal-title":"ACM Trans Softw Eng Methodol"},{"key":"245_CR19","doi-asserted-by":"crossref","unstructured":"Henzinger T, Jhala R, Majumdar R, Sutre G (2003) Software verification with BLAST. In: Proceedings of the 10th international SPIN workshop. LNCS, vol 2648. Springer, Berlin, pp 235\u2013239","DOI":"10.1007\/3-540-44829-2_17"},{"key":"245_CR20","doi-asserted-by":"crossref","unstructured":"Henzinger TA, Jhala R, Majumdar R, Sutre G (2003) Software verification with blast. In: Proceedings of the 10th international workshop on model checking of software (SPIN). LNCS, vol 2648. Springer, Berlin, pp 235\u2013239","DOI":"10.1007\/3-540-44829-2_17"},{"key":"245_CR21","unstructured":"Hunt JJ, Jenn E, Leriche S, Schmitt P, Tonin I, Wonnemann C (2006) A case study of specification and verification using JML in an avionics application. In: Proceedings of the 4th workshop on java technologies for real-time and embedded systems (JTRES). ACM Press, New York, pp 107\u2013116"},{"key":"245_CR22","unstructured":"Jones C, Bonsignour O (2011) The economics of software quality. Prentice Hall, New Jersey (2011)"},{"key":"245_CR23","doi-asserted-by":"crossref","unstructured":"Kim M, Kim Y, Kim H (2008) Unit testing of flash memory device driver through a SAT-based model checker. In: Proceedings of the international conference on automated software engineering (ASE). IEEE Computer Society Press, Washington, DC, pp 198\u2013207","DOI":"10.1109\/ASE.2008.30"},{"key":"245_CR24","doi-asserted-by":"crossref","unstructured":"Merz F, Falke S, Sinz C (2012) LLBMC: bounded model checking of C and C++ programs using a compiler IR. In: Proceedings of the 4th international conference on verified software: theories, tools, experiments (VSTTE\u201912). Springer, Berlin, pp 146\u2013161","DOI":"10.1007\/978-3-642-27705-4_12"},{"key":"245_CR25","doi-asserted-by":"crossref","unstructured":"Merz F, Sinz C, Post H, Gorges T, Kropf T (2010) Abstract testing: connecting source code verification with requirements. In: Proceedings of the 7th international conference on the quality of information and communications technology, pp 89\u201396","DOI":"10.1109\/QUATIC.2010.14"},{"key":"245_CR26","unstructured":"Meyer B (2005) Eiffel as a framework for verification. In: First IFIP TC 2\/WG 2.3 conference on verified software: theories, tools, experiments (VSSTE\u201905), pp 301\u2013307"},{"issue":"4\u20135","key":"245_CR27","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1007\/s10009-004-0173-6","volume":"8","author":"SP Miller","year":"2006","unstructured":"Miller SP, Tribble AC, Whalen MW, Heimdahl MPE (2006) Proving the shalls: early validation of requirements through formal methods. J Softw Tools Technol Transf (STTT) 8(4\u20135):303\u2013319","journal-title":"J Softw Tools Technol Transf (STTT)"},{"key":"245_CR28","unstructured":"MISRA C Working Group (2004) MISRA-C:2004\u2014guidelines for the use of the C language in critical systems. The Motor Industry Software Reliability Association"},{"key":"245_CR29","unstructured":"PolySpace Technologies (2008) Polyspace Client\/Server for C\/C++, Version 4.1.1.6. http:\/\/www.mathworks.de\/products\/polyspace . Accessed 24 Sept 2014"},{"key":"245_CR30","unstructured":"Post H, K\u00fcchlin W (2007) Integration of static analysis for linux device driver verification. In: Davies J, Gibbons J (eds) Proceedings of the 6th international conference integrated formal methods (IFM). LNCS, vol 4591. Springer, Berlin, pp 518\u2013537"},{"key":"245_CR31","unstructured":"RTI-Health, Social, and Economics Research (2002) The economic impacts of inadequate infrastructure for software testing. Planning Report 02-3. National Institute of Standards and Technology"},{"key":"245_CR32","unstructured":"SLAM-Microsoft Research. http:\/\/research.microsoft.com\/slam . Accessed 22 Sept 2014"},{"key":"245_CR33","doi-asserted-by":"crossref","unstructured":"Staats M, Heimdahl MPE (2008) Partial translation verification for untrusted code-generators. In: 10th international conference on formal engineering methodsformal (ICFEM\u201908), Kitakyushu-City, Japan, pp 226\u2013237","DOI":"10.1007\/978-3-540-88194-0_15"},{"key":"245_CR34","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1145\/1095430.1081749","volume":"30","author":"N Tillmann","year":"2005","unstructured":"Tillmann N, Schulte W (2005) Parameterized unit tests. SIGSOFT Softw Eng Notes 30:253\u2013262","journal-title":"SIGSOFT Softw Eng Notes"},{"key":"245_CR35","doi-asserted-by":"crossref","unstructured":"Uusitalo EJ, Komssi M, Kauppinen M, Davis AM (2008) Linking requirements and testing in practice. In: Proceedings of the 2008 16th IEEE international requirements engineering conference RE\u201908. IEEE Computer Society, Washington, DC, pp 265\u2013270","DOI":"10.1109\/RE.2008.30"},{"issue":"2","key":"245_CR36","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1023\/A:1022920129859","volume":"10","author":"W Visser","year":"2003","unstructured":"Visser W, Havelund K, Brat GP, Park S, Lerda F (2003) Model checking programs. Autom Softw Eng 10(2):203\u2013232","journal-title":"Autom Softw Eng"},{"issue":"4\u20135","key":"245_CR37","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/s10009-005-0209-6","volume":"8","author":"A Wassyng","year":"2006","unstructured":"Wassyng A, Lawford M (2006) Software tools for safety-critical software development. STTT 8(4\u20135):337\u2013354","journal-title":"STTT"}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-015-0245-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11334-015-0245-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-015-0245-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,22]],"date-time":"2019-08-22T07:20:40Z","timestamp":1566458440000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11334-015-0245-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,3,24]]},"references-count":37,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2015,12]]}},"alternative-id":["245"],"URL":"https:\/\/doi.org\/10.1007\/s11334-015-0245-7","relation":{},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"value":"1614-5046","type":"print"},{"value":"1614-5054","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,3,24]]}}}