{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T06:56:03Z","timestamp":1747810563747},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540208945"},{"type":"electronic","value":"9783540246176"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24617-6_4","type":"book-chapter","created":{"date-parts":[[2010,9,5]],"date-time":"2010-09-05T11:26:17Z","timestamp":1283685977000},"page":"42-59","source":"Crossref","is-referenced-by-count":23,"title":["Auto-generating Test Sequences Using Model Checkers: A Case Study"],"prefix":"10.1007","author":[{"given":"Mats P. E.","family":"Heimdahl","sequence":"first","affiliation":[]},{"given":"Sanjai","family":"Rayadurgam","sequence":"additional","affiliation":[]},{"given":"Willem","family":"Visser","sequence":"additional","affiliation":[]},{"given":"George","family":"Devaraj","sequence":"additional","affiliation":[]},{"given":"Jimin","family":"Gao","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","volume-title":"Proceedings of the Fourth IEEE International Symposium on High-Assurance Systems Engineering","author":"P.E. Ammann","year":"1999","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, November 1999. IEEE Computer Society, Los Alamitos (1999)"},{"key":"4_CR2","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1109\/ICFEM.1998.730569","volume-title":"Proceedings of the Second IEEE International Conference on Formal Engineering Methods (ICFEM 1998)","author":"P.E. Ammann","year":"1998","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 1998), November 1998, pp. 46\u201354. IEEE Computer Society, Los Alamitos (1998)"},{"key":"4_CR3","unstructured":"Callahan, J., Schneider, F., Easterbrook, S.: Specification-based testing using model checking. In: Proceedings of the SPIN Workshop (August 1996)"},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"Chilenski, J.J., Miller, S.P.: Applicability of modified condition\/decision coverage to software testing. Software Engineering Journal, 193\u2013200 (September 1994)","DOI":"10.1049\/sej.1994.0025"},{"key":"4_CR5","unstructured":"Choi, Y., Heimdahl, M.: Model checking RSML\u2212\u2009erequirements. In: Proceedings of the 7th IEEE\/IEICE International Symposium on High Assurance Systems Engineering (October 2002)"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Choi, Y., Rayadurgam, S., Heimdahl, M.: Automatic abstraction for model checking software systems with interrelated numeric constraints. In: Proceedings of the 9th ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC\/FSE-9), September 2001, pp. 164\u2013174 (2001)","DOI":"10.1145\/503209.503232"},{"key":"4_CR7","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counter example-guided abstraction refinement. In: Proceedings of the 12th International Conference on Computer Aided Verification, July 2000, pp. 154\u2013169 (2000)","DOI":"10.1007\/10722167_15"},{"key":"4_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"384","DOI":"10.1007\/BFb0035401","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Engels","year":"1997","unstructured":"Engels, A., Feijs, L.M.G., Mauw, S.: Test generation for intelligent networks using model checking. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol.\u00a01217, pp. 384\u2013398. Springer, Heidelberg (1997)"},{"issue":"6","key":"4_CR10","doi-asserted-by":"publisher","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. Software Engineering Notes\u00a024(6), 146\u2013162 (1999)","journal-title":"Software Engineering Notes"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Groce, A., Visser, W.: Model checking java programs using structural heuristics. In: Proceedings of the International Symposium on Software Testign and Analysis 2002, Rome, Italy (July 2002)","DOI":"10.1145\/566172.566175"},{"issue":"3","key":"4_CR12","doi-asserted-by":"publisher","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. Science of Computer Programming\u00a08(3), 231\u2013274 (1987)","journal-title":"Science of Computer Programming"},{"key":"4_CR13","unstructured":"Heimdahl, M.P.E., Rayadurgam, S., Visser, W.: Specification centered testing. In: Proceedings of The First International Workshop on Automated Program Analysis, Testing and Verificaiton, ICSE 2000 (2000)"},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Majumdar, R.: Lazy abstraction. In: Proceedings of the 29th Symposium on Principles of Programming Languages (January 2002)","DOI":"10.1145\/503272.503279"},{"key":"4_CR15","unstructured":"Hong, H.S., Cha, S.D., Lee, I., Sokolsky, O., Ural, H.: Data flow testing as model checking. In: Proceedings of 2003 International Confernece on Software Engineering, Portland, Oregon (May 2003)"},{"key":"4_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/3-540-46002-0_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H.S. Hong","year":"2002","unstructured":"Hong, H.S., Lee, I., Sokolsky, O., Ural, H.: A temporal logic based theory of test coverage and generation. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, p. 327. Springer, Heidelberg (2002)"},{"key":"4_CR17","doi-asserted-by":"crossref","unstructured":"Khurshid, S., Pasareanu, C.S., Visser, W.: Generalized symbolic execution for model checking and testing. In: Proceedings of the Ninth International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Warsaw, Poland (April 2003)","DOI":"10.1007\/3-540-36577-X_40"},{"issue":"9","key":"4_CR18","doi-asserted-by":"publisher","first-page":"684","DOI":"10.1109\/32.317428","volume":"20","author":"N.G. Leveson","year":"1994","unstructured":"Leveson, N.G., Heimdahl, M.P.E., Hildreth, H., Reese, J.D.: Requirements Specification for Process-Control Systems. IEEE Transactions on Software Engineering\u00a020(9), 684\u2013706 (1994)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"4_CR19","unstructured":"NuSMV: A New Symbolic Model Checking, Available at \n                    \n                      http:\/\/nusmv.irst.itc.it\/"},{"key":"4_CR20","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1109\/ECBS.2001.922409","volume-title":"Proceedings of the 8th Annual IEEE International Conference and Workshop on the Engineering of Computer Based Systems (ECBS 2001)","author":"S. Rayadurgam","year":"2001","unstructured":"Rayadurgam, S., Heimdahl, M.P.E.: 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), April 2001, pp. 83\u201391. IEEE Computer Society, Los Alamitos (2001)"},{"key":"4_CR21","doi-asserted-by":"crossref","unstructured":"Rayadurgam, S., Heimdahl, M.P.E.: 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 (October 2001)","DOI":"10.1109\/HASE.2001.966804"},{"key":"4_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/3-540-48166-4_11","volume-title":"Software Engineering - ESEC\/FSE \u201999","author":"J.M. Thompson","year":"1999","unstructured":"Thompson, J.M., Heimdahl, M.P.E., Miller, S.P.: Specification based prototyping for embedded systems. In: Nierstrasz, O., Lemoine, M. (eds.) ESEC 1999 and ESEC-FSE 1999. LNCS, vol.\u00a01687, pp. 163\u2013179. Springer, Heidelberg (1999)"},{"issue":"7","key":"4_CR23","first-page":"731","volume":"6","author":"J.M. Thompson","year":"2000","unstructured":"Thompson, J.M., Whalen, M.W., Heimdahl, M.P.E.: Requirements capture and evaluation in Nimbus: The light-control case study. Journal of Universal Computer Science\u00a06(7), 731\u2013757 (2000)","journal-title":"Journal of Universal Computer Science"},{"key":"4_CR24","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proceedings of the 1st Symposium on Logic in Computer Science, Cambridge, June 1986, pp. 322\u2013331 (1986)"},{"key":"4_CR25","doi-asserted-by":"crossref","unstructured":"Visser, W., Havelund, K., Brat, G., Park, S.: Model checking programs. In: Proceedings of the 15th International Conference on Automated Software Engineering, Grenoble, France (September 2000)","DOI":"10.1109\/ASE.2000.873645"}],"container-title":["Lecture Notes in Computer Science","Formal Approaches to Software Testing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24617-6_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,20]],"date-time":"2019-03-20T00:03:14Z","timestamp":1553040194000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24617-6_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540208945","9783540246176"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24617-6_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}