{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:17:25Z","timestamp":1763468245843,"version":"3.41.0"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319175232"},{"type":"electronic","value":"9783319175249"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-17524-9_20","type":"book-chapter","created":{"date-parts":[[2015,4,7]],"date-time":"2015-04-07T06:15:31Z","timestamp":1428387331000},"page":"279-294","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Are We There Yet? Determining the Adequacy of Formalized Requirements and Test Suites"],"prefix":"10.1007","author":[{"given":"Anitha","family":"Murugesan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael W.","family":"Whalen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Neha","family":"Rungta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Oksana","family":"Tkachuk","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Suzette","family":"Person","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mats P. E.","family":"Heimdahl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dongjiang","family":"You","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,4,8]]},"reference":[{"key":"20_CR1","unstructured":"IBM Rational Rhapsody (2014). http:\/\/www.ibm.com\/developerworks\/rational\/products\/rhapsody\/"},{"key":"20_CR2","unstructured":"IBM Rational Statemate (2014). http:\/\/www-03.ibm.com\/software\/products\/en\/ratistat"},{"key":"20_CR3","doi-asserted-by":"crossref","unstructured":"Ammann, P., Delamaro, M.E., Offutt, J.: Establishing theoretical minimal sets of mutants. In: Proceedings of the 2014 IEEE International Conference on Software Testing, Verification, and Validation, IEEE Computer Society Washington, DC, USA (2014)","DOI":"10.1109\/ICST.2014.13"},{"key":"20_CR4","unstructured":"Baudin, P., Filli\u00e2tre, J.-C., Claude, M., Benjamin, M., Moy, Y., Virgile, P., \u00cele-de France, I.S.: ANSI\/ISO C specification language, ACSL (2008)"},{"key":"20_CR5","doi-asserted-by":"crossref","unstructured":"Beer, I., Ben-David, S., Eisner, C., Rodeh, Y.: Efficient detection of vacuity in ACTL formulas. In: Formal Methods in System Design, pp. 141\u2013162 (2001)","DOI":"10.1023\/A:1008779610539"},{"key":"20_CR6","doi-asserted-by":"crossref","unstructured":"Clause, J., Li, W., Orso, A.: Dytan: a generic dynamic taint analysis framework. In: Proceedings of the 2007 Int\u2019l Symposium on Software Testing and Analysis, pp. 196\u2013206 (2007)","DOI":"10.1145\/1273463.1273490"},{"key":"20_CR7","doi-asserted-by":"crossref","unstructured":"Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-c. In: Software Engineering and Formal Methods, pp. 233\u2013247. Springer (2012)","DOI":"10.1007\/978-3-642-33826-7_16"},{"issue":"4","key":"20_CR8","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1109\/C-M.1978.218136","volume":"11","author":"RA DeMillo","year":"1978","unstructured":"DeMillo, R.A., Lipton, R.J., Sayward, F.G.: Hints on test data selection: Help for the practicing programmer. Computer 11(4), 34\u201341 (1978)","journal-title":"Computer"},{"key":"20_CR9","doi-asserted-by":"crossref","unstructured":"Devadas, S., Ghosh, A., Keutzer, K.: An observability-based code coverage metric for functional simulation. In: Proceedings of the 1996 IEEE\/ACM Int\u2019l Conf. on Computer-Aided Design, pp. 418\u2013425 (1996)","DOI":"10.1109\/ICCAD.1996.569832"},{"key":"20_CR10","unstructured":"Esterel-Technologies. SCADE Suite product description. http:\/\/www.esterel-technologies.com\/v2\/scadeSuiteForSafetyCriticalSoftwareDe"},{"issue":"8","key":"20_CR11","doi-asserted-by":"publisher","first-page":"1003","DOI":"10.1109\/43.936381","volume":"20","author":"F Fallah","year":"2001","unstructured":"Fallah, F., Devadas, S., Keutzer, K.: OCCOM-efficient computation of observability-based code coverage metrics for functional verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 20(8), 1003\u20131015 (2001)","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"20_CR12","doi-asserted-by":"crossref","unstructured":"Fraser, G., Staats, M., McMinn, P., Arcuri, A., Padberg, F.: Does automated white-box test generation really help software testers? In: ISSTA 2013 Proceedings of the 2013 International Symposium on Software Testing and Analysis, pp. 291\u2013301. ACM, New York, NY, USA (2013)","DOI":"10.1145\/2483760.2483774"},{"key":"20_CR13","unstructured":"Gacek, A.: JKind - a Java implementation of the KIND model checker. https:\/\/github.com\/agacek"},{"key":"20_CR14","doi-asserted-by":"crossref","unstructured":"Gay, G., Staats, M., Whalen, M.W., Heimdahl, M.P.E.: Moving the goalposts: coverage satisfaction is not enough. In: Proceedings of the 7th International Workshop on Search-Based Software Testing, ACM, New York, NY, USA (2014)","DOI":"10.1145\/2593833.2593837"},{"issue":"3","key":"20_CR15","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1016\/0020-0190(88)90054-3","volume":"29","author":"B Korel","year":"1988","unstructured":"Korel, B., Laski, J.: Dynamic program slicing. Information Processing Letters 29(3), 155\u2013163 (1988)","journal-title":"Information Processing Letters"},{"key":"20_CR16","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.Y.: Vacuity detection in temporal model checking. Journal on Software Tools for Technology Transfer 4(2), February 2003","DOI":"10.1007\/s100090100062"},{"key":"20_CR17","unstructured":"GNUGPL License. Gcov: Gnu coverage tool. https:\/\/gcc.gnu.org"},{"key":"20_CR18","doi-asserted-by":"crossref","unstructured":"Masri, W., Podgurski, A., Leon, D.: Detecting and debugging insecure information flows. In: Proceedings of the 15th Int\u2019l Symposium on Software Reliability Engineering, pp. 198\u2013209 (2004)","DOI":"10.1109\/ISSRE.2004.17"},{"key":"20_CR19","unstructured":"MathWorks Inc., Simulink. http:\/\/www.mathworks.com\/products\/simulink"},{"key":"20_CR20","unstructured":"MathWorks Inc., Simulink Coder. http:\/\/www.mathworks.com\/products\/simulink-coder\/"},{"key":"20_CR21","unstructured":"MathWorks Inc., Simulink Design Verifier. http:\/\/www.mathworks.com\/products\/sldesignverifier"},{"key":"20_CR22","doi-asserted-by":"crossref","unstructured":"Murugesan, A., Whalen, M.W., Rayadurgam, S., Heimdahl, M.P.E.: Compositional verification of a medical device system. In: ACM Int\u2019l Conf. on High Integrity Language Technology (HILT) 2013. ACM, November 2013","DOI":"10.1145\/2527269.2527272"},{"key":"20_CR23","doi-asserted-by":"crossref","unstructured":"Offutt, A.J., Untch, R.H.: Mutation testing for the new century. chapter Mutation 2000: Uniting the Orthogonal, pp. 34\u201344. Kluwer Academic Publishers, Norwell, MA, USA (2001)","DOI":"10.1007\/978-1-4757-5939-6_7"},{"key":"20_CR24","doi-asserted-by":"crossref","unstructured":"Pecheur, C., Raimondi, F., Brat, G.: A formal analysis of requirements-based testing. In: Proceedings of the Eighteenth International Symposium on Software Testing and Analysis, pp. 47\u201356. ACM (2009)","DOI":"10.1145\/1572272.1572279"},{"key":"20_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"485","DOI":"10.1007\/3-540-45657-0_39","volume-title":"Computer Aided Verification","author":"M Purandare","year":"2002","unstructured":"Purandare, M., Somenzi, F.: Vacuum cleaning CTL formulae. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 485. Springer, Heidelberg (2002)"},{"key":"20_CR26","unstructured":"Reactive systems inc. http:\/\/www.reactive-systems.com\/index.msp"},{"key":"20_CR27","unstructured":"RTCA\/DO-178C. Software considerations in airborne systems and equipment certification"},{"key":"20_CR28","doi-asserted-by":"crossref","unstructured":"Rungta, N., Tkachuk, O., Person, S., Biatek, J., Whalen, M.W., Castle, J., Gundy-Burlet, K.: Helping system engineers bridge the peaks. In: TwinPeaks 2014 Proceedings of the 4th International Workshop on Twin Peaks of Requirements and Architecture, pp. 9\u201313. ACM, New York, NY, USA, (2014)","DOI":"10.1145\/2593861.2593863"},{"key":"20_CR29","doi-asserted-by":"crossref","unstructured":"Schuler, D., Zeller, A.: Assessing oracle quality with checked coverage. In: ICST 2011 Proceedings of the 2011 Fourth IEEE International Conference on Software Testing, Verification and Validation, pp. 90\u201399. IEEE Computer Society, Washington, DC, USA (2011)","DOI":"10.1109\/ICST.2011.32"},{"issue":"7","key":"20_CR30","first-page":"531","volume":"23","author":"D Schuler","year":"2013","unstructured":"Schuler, D., Zeller, A.: Checked coverage: an indicator for oracle quality. Software: Testing, Verification and Reliability 23(7), 531\u2013551 (2013)","journal-title":"Software: Testing, Verification and Reliability"},{"key":"20_CR31","doi-asserted-by":"crossref","unstructured":"Staats, M., Gay, G., Whalen, M.W., Heimdahl, M.P.E.: On the danger of coverage directed test case generation. In: 15th Int\u2019l Conf. on Fundamental Approaches to Software Engineering (FASE), April 2012","DOI":"10.1007\/978-3-642-28872-2_28"},{"issue":"4","key":"20_CR32","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1109\/TSE.1984.5010248","volume":"10","author":"M Weiser","year":"1984","unstructured":"Weiser, M.: Program slicing. IEEE Transactions on Software Engineering 10(4), 352\u2013357 (1984)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"20_CR33","doi-asserted-by":"crossref","unstructured":"Whalen, M., Gay, G., You, D., Heimdahl, M.P.E., Staats, M.: Observable modified condition\/decision coverage. In: Proceedings of the 2013 Int\u2019l Conf. on Software Engineering. ACM, May 2013","DOI":"10.1109\/ICSE.2013.6606556"},{"key":"20_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/978-3-540-79707-4_7","volume-title":"Formal Methods for Industrial Critical Systems","author":"MW Whalen","year":"2007","unstructured":"Whalen, M.W., Cofer, D.D., Miller, S.P., Krogh, B.H., Storm, W.: Integration of Formal Analysis into a Model-Based Software Development Process. In: Leue, S., Merino, P. (eds.) Formal Methods for Industrial Critical Systems. LNCS, vol. 4916, pp. 68\u201384. Springer, Heidelberg (2007)"},{"key":"20_CR35","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-1539-9_13","volume-title":"Model Checking Information Flow","author":"MW Whalen","year":"2010","unstructured":"Whalen, M.W., Greve, D.A., Wagner, L.G.: Model Checking Information Flow. Springer-Verlag, Berlin Germany (2010)"},{"key":"20_CR36","doi-asserted-by":"crossref","unstructured":"Whalen, M.W., Rajan, A., Heimdahl, M.P.E.: Coverage metrics for requirements-based testing. In: Proceedings of Int\u2019l Symposium on Software Testing and Analysis, pp. 25\u201336. ACM, July 2006","DOI":"10.1145\/1146238.1146242"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-17524-9_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T23:26:20Z","timestamp":1747869980000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-17524-9_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319175232","9783319175249"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-17524-9_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"8 April 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}