{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T18:56:11Z","timestamp":1742928971793,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642217678"},{"type":"electronic","value":"9783642217685"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-21768-5_13","type":"book-chapter","created":{"date-parts":[[2011,6,27]],"date-time":"2011-06-27T09:18:53Z","timestamp":1309166333000},"page":"171-186","source":"Crossref","is-referenced-by-count":6,"title":["State Coverage Metrics for Specification-Based Testing with B\u00fcchi Automata"],"prefix":"10.1007","author":[{"given":"Li","family":"Tan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"13_CR1","volume-title":"Computer Networks","author":"A.S. Tanenbaum","year":"2010","unstructured":"Tanenbaum, A.S.: Computer Networks, 5th edn. Prentice Hall, Englewood Cliffs (2010)","edition":"5"},{"key":"13_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/978-3-540-79124-9_6","volume-title":"Tests and Proofs","author":"A. Calvagna","year":"2008","unstructured":"Calvagna, A., Gargantini, A.: A Logic-Based Approach to Combinatorial Testing with Constraints. In: Beckert, B., H\u00e4hnle, R. (eds.) TAP 2008. LNCS, vol.\u00a04966, pp. 66\u201383. Springer, Heidelberg (2008)"},{"key":"13_CR3","volume-title":"Model Checking","author":"E. Clarke","year":"1999","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"13_CR4","first-page":"72","volume-title":"TAIC-PART 2009","author":"G. Fraser","year":"2009","unstructured":"Fraser, G., Gargantini, A.: An Evaluation of Specification Based Test Generation Techniques Using Model Checkers. In: TAIC-PART 2009, pp. 72\u201381. IEEE Press, Los Alamitos (2009)"},{"key":"13_CR5","first-page":"3","volume-title":"PSTV 1995","author":"R. Gerth","year":"1995","unstructured":"Gerth, R., Peled, D., Vardi, M., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: PSTV 1995, pp. 3\u201318. Chapman and Hall, Boca Raton (1995)"},{"key":"13_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1007\/3-540-36135-9_20","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2002","author":"D. Giannakopoulou","year":"2002","unstructured":"Giannakopoulou, D., Lerda, F.: From States to Transitions: Improving Translation of LTL Formulae to B\u00fcchi Automata. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol.\u00a02529, pp. 308\u2013326. Springer, Heidelberg (2002)"},{"issue":"5","key":"13_CR7","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"J. Gerard","year":"1997","unstructured":"Gerard, J.: The Model Checker SPIN. IEEE Transactions on Software Engineering\u00a023(5), 279\u2013295 (1997)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"13_CR8","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, pp. 327\u2013341. Springer, Heidelberg (2002)"},{"issue":"4","key":"13_CR9","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1007\/s100090050045","volume":"2","author":"M. Kamel","year":"2000","unstructured":"Kamel, M., Leue, S.: Formalization and validation of the General Inter-ORB Protocol (GIOP) using PROMELA and SPIN. International Journal on Software Tools for Technology Transfer (STTT)\u00a02(4), 394\u2013409 (2000)","journal-title":"International Journal on Software Tools for Technology Transfer (STTT)"},{"issue":"2","key":"13_CR10","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1007\/s100090100062","volume":"4","author":"O. Kupferman","year":"2003","unstructured":"Kupferman, O., Vardi, M.Y.: Vacuity detection in temporal model checking. International Journal on Software Tools for Technology Transfer (STTT)\u00a04(2), 224\u2013233 (2003)","journal-title":"International Journal on Software Tools for Technology Transfer (STTT)"},{"key":"13_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/3-540-46017-9_14","volume-title":"Model Checking Software","author":"P. Maggi","year":"2002","unstructured":"Maggi, P., Sisto, R.: Using SPIN to Verify Security Properties of Cryptographic Protocols. In: Bo\u0161na\u010dki, D., Leue, S. (eds.) SPIN 2002. LNCS, vol.\u00a02318, pp. 187\u2013204. Springer, Heidelberg (2002)"},{"key":"13_CR12","volume-title":"Complementation is more difficult with automata on infinite words","author":"M. Michel","year":"1988","unstructured":"Michel, M.: Complementation is more difficult with automata on infinite words. CNET, Paris (1988)"},{"key":"13_CR13","first-page":"493","volume-title":"IRI 2004","author":"L. Tan","year":"2004","unstructured":"Tan, L., Sokolsky, O., Lee, I.: Specification-based Testing with Linear Temporal Logic. In: IRI 2004, pp. 493\u2013498. IEEE Society, Los Alamitos (2004)"},{"key":"13_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"466","DOI":"10.1007\/978-3-540-71209-1_35","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y.-K. Tsay","year":"2007","unstructured":"Tsay, Y.-K., Chen, Y.-F., Tsai, M.-H., Wu, K.-N., Chan, W.-C.: GOAL: A Graphical Tool for Manipulating B\u00fcchi Automata and Temporal Formulae. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 466\u2013471. Springer, Heidelberg (2007)"},{"key":"13_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/978-3-540-69738-1_10","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"M.Y. Vardi","year":"2007","unstructured":"Vardi, M.Y.: Automata-theoretic model checking revisited. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, pp. 137\u2013150. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","Tests and Proofs"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-21768-5_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T19:57:29Z","timestamp":1558295849000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-21768-5_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642217678","9783642217685"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-21768-5_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}