{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,20]],"date-time":"2022-04-20T15:35:14Z","timestamp":1650468914173},"reference-count":31,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2013,4,10]],"date-time":"2013-04-10T00:00:00Z","timestamp":1365552000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Inf Syst Front"],"published-print":{"date-parts":[[2014,11]]},"DOI":"10.1007\/s10796-013-9424-y","type":"journal-article","created":{"date-parts":[[2013,4,9]],"date-time":"2013-04-09T01:30:20Z","timestamp":1365471020000},"page":"823-834","source":"Crossref","is-referenced-by-count":4,"title":["A unified framework for evaluating test criteria in model-checking-assisted test case generation"],"prefix":"10.1007","volume":"16","author":[{"given":"Bolong","family":"Zeng","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Li","family":"Tan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2013,4,10]]},"reference":[{"key":"9424_CR1","first-page":"46","volume-title":"Proceedings of the second IEEE international conference on formal engineering methods, ICFEM\u201998","author":"PE Ammann","year":"1998","unstructured":"Ammann, P.E., Black, P.E., Majurski, W. (1998). 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). Washington, DC: IEEE Computer Society."},{"key":"9424_CR2","volume-title":"Proceedings of the 9th international conference on computer aided verification, CAV \u201997","author":"I Beer","year":"1997","unstructured":"Beer, I., Ben-David, S., Eisner, C., Rodeh, Y. (1997). Efficient detection of vacuity in actl formulas. In: Proceedings of the 9th international conference on computer aided verification, CAV \u201997. London: Springer-Verlag."},{"key":"9424_CR3","doi-asserted-by":"crossref","first-page":"326","DOI":"10.1109\/ICSE.2004.1317455","volume-title":"Proceedings of the 26th international conference on software engineering, ICSE\u201904","author":"D Beyer","year":"2004","unstructured":"Beyer, D., Chlipala, A.J., Majumdar, R., Henzinger, T.A., Jhala, R. (2004). Generating tests from counterexamples. In Proceedings of the 26th international conference on software engineering, ICSE\u201904 (pp. 326\u2013335). Washington, DC: IEEE Computer Society."},{"key":"9424_CR4","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1109\/LICS.2002.1029814","volume-title":"Proceedings of 17th annual IEEE symposium on Logic in computer science","author":"E Clarke","year":"2002","unstructured":"Clarke, E., Jha, S., Lu, Y. (2002). Tree-like counterexamples in model checking. In Proceedings of 17th annual IEEE symposium on Logic in computer science (pp. 19\u201329). Washington, DC: IEEE Computer Society."},{"key":"9424_CR5","volume-title":"Logic of programs, workshop","author":"EM Clarke","year":"1982","unstructured":"Clarke, E.M., & Emerson, E.A. (1982). Design and synthesis of synchronization skeletons using branching-time temporal logic. In Logic of programs, workshop. London: Springer-Verlag."},{"key":"9424_CR6","volume-title":"Proceedings of the 32nd annual ACM\/IEEE design automation conference, DAC \u201995","author":"EM Clarke","year":"1995","unstructured":"Clarke, E.M., Grumberg, O., McMillan, K.L., Zhao, X. (1995). Efficient generation of counterexamples and witnesses in symbolic model checking. In Proceedings of the 32nd annual ACM\/IEEE design automation conference, DAC \u201995. New York: ACM."},{"key":"9424_CR7","volume-title":"Model checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D. (1999). Model checking. Cambridge: MIT Press."},{"key":"9424_CR8","volume-title":"Proceedings of the third international workshop on tools and algorithms for construction and analysis of systems, TACAS \u201997","author":"A Engels","year":"1997","unstructured":"Engels, A., Feijs, L.M.G., Mauw, S. (1997). Test generation for intelligent networks using model checking. In Proceedings of the third international workshop on tools and algorithms for construction and analysis of systems, TACAS \u201997. London: Springer-Verlag."},{"key":"9424_CR9","volume-title":"Proceedings of the 2009 international conference on software testing verification and validation ICST \u201909","author":"G Fraser","year":"2009","unstructured":"Fraser, G., & Gargantini, A. (2009). An evaluation of model checkers for specification based test case generation. In Proceedings of the 2009 international conference on software testing verification and validation ICST \u201909. Washington, DC: IEEE Computer Society."},{"key":"9424_CR10","volume-title":"Proceedings of the 7th European software engineering conference held jointly with the 7th ACM SIGSOFT international symposium on Foundations of software engineering, ESEC\/FSE-7","author":"A Gargantini","year":"1999","unstructured":"Gargantini, A., & Heitmeyer, C. (1999). Using model checking to generate tests from requirements specifications. In Proceedings of the 7th European software engineering conference held jointly with the 7th ACM SIGSOFT international symposium on Foundations of software engineering, ESEC\/FSE-7. London: Springer-Verlag."},{"key":"9424_CR11","volume-title":"Proceedings of the second international workshop on automated program analysis, testing and verification","author":"MP Heimdahl","year":"2001","unstructured":"Heimdahl, M.P., Rayadurgam, S., Visser, W. (2001). Specification centered testing. In Proceedings of the second international workshop on automated program analysis, testing and verification. Washington, DC: IEEE Computer Society."},{"issue":"5","key":"9424_CR13","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"GJ Holzmann","year":"1997","unstructured":"Holzmann, G.J. (1997). The model checker {SPIN}. IEEE Transactions on Software Engineering, 23(5), 279\u2013295.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"9424_CR14","volume-title":"Proceedings of the 25th international conference on software engineering ICSE \u201903","author":"HS Hong","year":"2003","unstructured":"Hong, H.S., Cha, S.D., Lee, I., Sokolsky, O., Ural, H. (2003). Data flow testing as model checking. In Proceedings of the 25th international conference on software engineering ICSE \u201903. Washington, DC: IEEE Computer Society."},{"key":"9424_CR15","volume-title":"Proceedings 848of the 8th international conference on tools and algorithms for the construction and analysis of systems, TACAS \u201902","author":"HS Hong","year":"2002","unstructured":"Hong, H.S., Lee, I., Sokolsky, O., Ural, H. (2002). A temporal logic based theory of test coverage and generation. In Proceedings of the 8th international conference on tools and algorithms for the construction and analysis of systems, TACAS \u201902. London: Springer-Verlag."},{"key":"9424_CR16","volume-title":"Software testing: a craftsman\u2019s approach","author":"PC Jorgensen","year":"1995","unstructured":"Jorgensen, P.C. (1995). Software testing: a craftsman\u2019s approach, 1st edn. Boca Raton: CRC Press.","edition":"1"},{"key":"9424_CR17","unstructured":"Kamel, M., & Leue, S. (1998). Validation of the general inter-orb protocol (giop) using the spin model-checker. In In software tools for technology transfer. Springer-Verlag."},{"key":"9424_CR18","doi-asserted-by":"crossref","unstructured":"Kupferman, O., & Vardi, M.Y. (1999). Vacuity detection in temporal model checking. Lecture Notes in Computer Science, 82, 82\u201396.","DOI":"10.1007\/3-540-48153-2_8"},{"key":"9424_CR19","doi-asserted-by":"crossref","unstructured":"Lamport, L. (1974). A new solution of dijkstra\u2019s concurrent programming problem. Communication ACM, 17, 453\u2013455.","DOI":"10.1145\/361082.361093"},{"key":"9424_CR20","volume-title":"Lecture notes in computer science","author":"F Lerda","year":"2001","unstructured":"Lerda, F., & Visser, W. (2001). Addressing dynamic issues of program model checking. In Lecture notes in computer science. Heidelberg: Springer-Verlag."},{"key":"9424_CR21","unstructured":"MathWorks (2007). Simulink design verifier. http:\/\/www.mathworks.com\/products\/sldesignverifier\/ . Accessed 30 Mar 2013."},{"key":"9424_CR22","doi-asserted-by":"crossref","unstructured":"Peterson, G.L. (1981). Myths about the mutual exclusion problem. Information Processing Letters, 12(3), 115\u2013116.","DOI":"10.1016\/0020-0190(81)90106-X"},{"key":"9424_CR23","volume-title":"Computer networks: A systems approach","author":"LL Peterson","year":"2003","unstructured":"Peterson, L.L., & Davie, B.S. (2003). Computer networks: A systems approach, 3rd edn. San Francisco: Morgan Kaufmann.","edition":"3"},{"key":"9424_CR24","doi-asserted-by":"crossref","unstructured":"Rapps, S., & Weyuker, E.J. (1985). Selecting software test data using data flow information. IEEE Transactions on Software Engineering, 11, 367\u2013375.","DOI":"10.1109\/TSE.1985.232226"},{"key":"9424_CR25","doi-asserted-by":"crossref","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. (2001). 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 (pp. 83\u201391), ECBS 2001. Washington, D.C: IEEE Computer Society."},{"key":"9424_CR26","doi-asserted-by":"crossref","unstructured":"Rushby, J. (2002). Using model checking to help discover mode confusions and other automation surprises. Reliability Engineering and System Safety, 75(2), 167\u2013177.","DOI":"10.1016\/S0951-8320(01)00092-8"},{"key":"9424_CR27","unstructured":"SC-167 Committee (1992). Software considerations in airborne systems and equipment certification. Tech. rep., Radio Technical Commission for Aeronautics."},{"key":"9424_CR28","volume-title":"Proceedings of the 5th international conference on tests and proofs, TAP\u201911","author":"L Tan","year":"2011","unstructured":"Tan, L. (2011). State coverage metrics for specification-based testing with b\u00fcchi automata. In Proceedings of the 5th international conference on tests and proofs, TAP\u201911. Heidelberg: Springer-Verlag."},{"key":"9424_CR29","volume-title":"In computer-aided verification","author":"L Tan","year":"2002","unstructured":"Tan, L., & Cleaveland, R. (2002). Evidence-based model checking. In In computer-aided verification. Heidelberg: Springer-Verlag."},{"key":"9424_CR30","unstructured":"Tan, L., Sokolsky, O., Lee, I. (2003). Property-coverage testing. Tech. rep., Department of Computer and Information Science, University of Pennsylvania."},{"key":"9424_CR31","first-page":"493","volume-title":"The proceedings of IEEE international conference on information reuse and integration, IRI04","author":"L Tan","year":"2004","unstructured":"Tan, L., Sokolsky, O., Lee, I. (2004). Specification-based Testing with Linear Temporal Logic. In The proceedings of IEEE internation conference on information reuse and integration (pp. 493\u2013498), IRI04. Las Vegas: IEEE society."},{"key":"9424_CR32","volume-title":"Proceedings of TACAS (2007), LNCS 4424","author":"Y-k Tsay","year":"2007","unstructured":"Tsay, Y.-k., Chen, Y.-f., Tsai, M.-h., Wu, K.-n., Chan, W.-c. (2007). Goal: A graphical tool for manipulating Buchi automata and temporal formulae. In Proceedings of TACAS (2007), LNCS 4424. Heidelberg: Springer."}],"container-title":["Information Systems Frontiers"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10796-013-9424-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10796-013-9424-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10796-013-9424-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T20:36:21Z","timestamp":1559248581000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10796-013-9424-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,4,10]]},"references-count":31,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2014,11]]}},"alternative-id":["9424"],"URL":"https:\/\/doi.org\/10.1007\/s10796-013-9424-y","relation":{},"ISSN":["1387-3326","1572-9419"],"issn-type":[{"value":"1387-3326","type":"print"},{"value":"1572-9419","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,4,10]]}}}