{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,10]],"date-time":"2025-04-10T04:18:45Z","timestamp":1744258725423,"version":"3.40.4"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642338250"},{"type":"electronic","value":"9783642338267"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-33826-7_4","type":"book-chapter","created":{"date-parts":[[2012,9,25]],"date-time":"2012-09-25T22:46:25Z","timestamp":1348613185000},"page":"48-62","source":"Crossref","is-referenced-by-count":7,"title":["Checking Sanity of Software Requirements"],"prefix":"10.1007","author":[{"given":"Ji\u0159\u00ed","family":"Barnat","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Petr","family":"Bauch","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lubo\u0161","family":"Brim","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"Barnat, J., Brim, L., \u010ce\u0161ka, M., Ro\u010dkai, P.: DiVinE: Parallel Distributed Model Checker. In: Proc. of HiBi\/PDMC, pp. 4\u20137 (2010)","DOI":"10.1109\/PDMC-HiBi.2010.9"},{"key":"4_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/3-540-44585-4_23","volume-title":"Computer Aided Verification","author":"S. Blom","year":"2001","unstructured":"Blom, S., Fokkink, W.J., Groote, J.F., van Langevelde, I., Lisser, B., van de Pol, J.: \u03bcCRL: A Toolset for Analysing Algebraic Specifications. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 250\u2013254. Springer, Heidelberg (2001)"},{"key":"4_CR3","doi-asserted-by":"publisher","first-page":"498","DOI":"10.1109\/32.708566","volume":"24","author":"W. Chan","year":"1998","unstructured":"Chan, W., Anderson, R.J., Bea, P., Burns, S., Modugno, F., Notkin, D., Reese, J.D.: Model Checking Large Software Specifications. IEEE T. Software Eng.\u00a024, 498\u2013520 (1998)","journal-title":"IEEE T. Software Eng."},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/3-540-44585-4_7","volume-title":"Computer Aided Verification","author":"H. Chockler","year":"2001","unstructured":"Chockler, H., Kupferman, O., Kurshan, R.P., Vardi, M.Y.: A Practical Approach to Coverage in Model Checking. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 66\u201378. Springer, Heidelberg (2001)"},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"528","DOI":"10.1007\/3-540-45319-9_36","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H. Chockler","year":"2001","unstructured":"Chockler, H., Kupferman, O., Vardi, M.Y.: Coverage Metrics for Temporal Logic Model Checking. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 528\u2013542. Springer, Heidelberg (2001)"},{"key":"4_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"2002","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An OpenSource Tool for Symbolic Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 359\u2013364. Springer, Heidelberg (2002)"},{"key":"4_CR7","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BF00121128","volume":"1","author":"C. Courcoubetis","year":"1992","unstructured":"Courcoubetis, C., Vardi, M.Y., Wolper, P., Yannakakis, M.: Memory-Efficient Algorithms for the Verification of Temporal Properties. Form. Method Syst. Des.\u00a01, 275\u2013288 (1992)","journal-title":"Form. Method Syst. Des."},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Property Specification Patterns for Finite-State Verification. In: Proc. of FMSP, pp. 7\u201315 (1998)","DOI":"10.1145\/298595.298598"},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"Heimdahl, M.P.E., Leveson, N.G.: Completeness and Consistency Analysis of State-Based Requirements. In: Proc. of ICSE, pp. 3\u201314 (1995)","DOI":"10.1145\/225014.225015"},{"key":"4_CR10","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1145\/1378727.1378742","volume":"51","author":"M. Hinchey","year":"2008","unstructured":"Hinchey, M., Jackson, M., Cousot, P., Cook, B., Bowen, J.P., Margaria, T.: Software Engineering and Formal Methods. Commun. ACM\u00a051, 54\u201359 (2008)","journal-title":"Commun. ACM"},{"key":"4_CR11","unstructured":"Industrial Framework for Embedded Systems Tools, http:\/\/www.artemis-ifest.eu"},{"key":"4_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/11817949_3","volume-title":"CONCUR 2006 \u2013 Concurrency Theory","author":"O. Kupferman","year":"2006","unstructured":"Kupferman, O.: Sanity Checks in Formal Verification. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol.\u00a04137, pp. 37\u201351. Springer, Heidelberg (2006)"},{"key":"4_CR13","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. STTT\u00a04, 224\u2013233 (2003)","journal-title":"STTT"},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"Leveson, N.: Completeness in Formal Specification Language Design for Process-Control Systems. In: Proc. of FMSP, pp. 75\u201387 (2000)","DOI":"10.1145\/349360.351140"},{"key":"4_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/978-3-540-45236-2_6","volume-title":"FME 2003: Formal Methods","author":"S.P. Miller","year":"2003","unstructured":"Miller, S.P., Tribble, A.C., Heimdahl, M.P.E.: Proving the Shalls. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, pp. 75\u201393. Springer, Heidelberg (2003)"},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"Rajan, A., Whalen, M.W., Heimdahl, M.P.E.: Model Validation using Automatically Generated Requirements-Based Tests. In: Proc. of HASE, pp. 95\u2013104 (2007)","DOI":"10.1109\/HASE.2007.57"},{"key":"4_CR17","doi-asserted-by":"crossref","unstructured":"Roy, S., Das, S., Basu, P., Dasgupta, P., Chakrabarti, P.P.: SAT Based Solutions for Consistency Problems in Formal Property Specifications for Open Systems. In: Proc. of ICCAD, pp. 885\u2013888 (2005)","DOI":"10.1109\/ICCAD.2005.1560186"},{"key":"4_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-540-73370-6_11","volume-title":"Model Checking Software","author":"K.Y. Rozier","year":"2007","unstructured":"Rozier, K.Y., Vardi, M.Y.: LTL Satisfiability Checking. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol.\u00a04595, pp. 149\u2013167. Springer, Heidelberg (2007)"},{"issue":"4","key":"4_CR19","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1109\/54.936247","volume":"18","author":"S. Tasiran","year":"2001","unstructured":"Tasiran, S., Keutzer, K.: Coverage Metrics for Functional Validation of Hardware Designs. IEEE Des. Test. Comput.\u00a018(4), 36\u201345 (2001)","journal-title":"IEEE Des. Test. Comput."},{"key":"4_CR20","doi-asserted-by":"crossref","unstructured":"Whalen, M.W., Rajan, A., Heimdahl, M.P.E., Miller, S.P.: Coverage Metrics for Requirements-Based Testing. In: Proc. of ISSTA, pp. 25\u201336 (2006)","DOI":"10.1145\/1146238.1146242"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-33826-7_4.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T12:42:52Z","timestamp":1744202572000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-33826-7_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642338250","9783642338267"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-33826-7_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}