{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,19]],"date-time":"2026-08-19T17:42:41Z","timestamp":1787161361056,"version":"build-2736575974"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540489283","type":"print"},{"value":"9783540489290","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11925040_11","type":"book-chapter","created":{"date-parts":[[2006,11,1]],"date-time":"2006-11-01T00:15:01Z","timestamp":1162340101000},"page":"161-180","source":"Crossref","is-referenced-by-count":3,"title":["A Case Study in Domain-Customized Model Checking for Real-Time Component Software"],"prefix":"10.1007","author":[{"given":"Matthew","family":"Hoosier","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Matthew B.","family":"Dwyer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"family":"Robby","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"John","family":"Hatcliff","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"Ben-David, S., Heyman, T., Grumberg, O., Schuster, A.: Scalable distributed on-the-fly symbolic model checking. In: Proceedings of Formal Methods in Computer-Aided Design, pp. 390\u2013404 (2000)","DOI":"10.1007\/3-540-40922-X_24"},{"key":"11_CR2","unstructured":"Bosnacki, D., Dams, D., Holenderski, L.: Symmetric SPIN. International Journal on Software Tools for Technology Transfer (2002)"},{"key":"11_CR3","unstructured":"Brat, G., Havelund, K., Park, S., Visser, W.: Java PathFinder \u2013 a second generation of a Java model-checker. In: Proceedings of the Workshop on Advances in Verification (July 2000)"},{"issue":"2","key":"11_CR4","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1109\/32.908961","volume":"27","author":"W. Chan","year":"2001","unstructured":"Chan, W., Anderson, R.J., Beame, P., Jones, D.H., Notkin, D., Warner, W.E.: Optimizing symbolic model checking for statecharts. IEEE Transactions on Software Engineering\u00a027(2), 170\u2013190 (2001)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"11_CR5","volume-title":"Model Checking","author":"E. Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)"},{"key":"11_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/3-540-48234-2_20","volume-title":"Theoretical and Practical Aspects of SPIN Model Checking","author":"C. Demartini","year":"1999","unstructured":"Demartini, C., Iosif, R., Sisto, R.: dspin: A dynamic extension of SPIN. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol.\u00a01680, pp. 261\u2013276. Springer, Heidelberg (1999)"},{"key":"11_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/978-3-540-39656-7_6","volume-title":"Formal Methods for Components and Objects","author":"W. Deng","year":"2003","unstructured":"Deng, W., Dwyer, M.B., Hatcliff, J., Jung, G., Robby, S.G.: Model-Checking Middleware-Based Event-Driven Real-Time Embedded Software. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2002. LNCS, vol.\u00a02852, pp. 154\u2013181. Springer, Heidelberg (2003)"},{"key":"11_CR8","volume-title":"Proceedings of the 24th International Conference on Software Engineering","author":"X. Deng","year":"2002","unstructured":"Deng, X., Dwyer, M.B., Hatcliff, J., Mizuno, M.: Invariant-based specification, synthesis, and verification of synchronization in concurrent programs. In: Proceedings of the 24th International Conference on Software Engineering. IEEE Press, Los Alamitos (2002)"},{"key":"11_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-540-45212-6_12","volume-title":"Embedded Software","author":"M.B. Dwyer","year":"2003","unstructured":"Dwyer, M.B., Robby, D.X., Hatcliff, J.: Space reductions for model checking quasi-cyclic systems. In: Alur, R., Lee, I. (eds.) EMSOFT 2003. LNCS, vol.\u00a02855, pp. 173\u2013189. Springer, Heidelberg (2003)"},{"key":"11_CR10","volume-title":"Design Patterns","author":"E. Gamma","year":"1995","unstructured":"Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns. Addison-Wesley Pub. Co., Reading (1995)"},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/3-540-45139-0_14","volume-title":"Model Checking Software","author":"H. Garavel","year":"2001","unstructured":"Garavel, H., Mateescu, R., Smarandache, I.: Parallel state space construction for model-checking. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol.\u00a02057, p. 217. Springer, Heidelberg (2001)"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Model-checking for programming languages using VeriSoft. In: Proceedings of the 24th ACM Symposium on Principles of Programming Languages (POPL 1997), pp. 174\u2013186 (January 1997)","DOI":"10.1145\/263699.263717"},{"key":"11_CR13","volume-title":"Proceedings of the 25th International Conference on Software Engineering","author":"J. Hatcliff","year":"2003","unstructured":"Hatcliff, J., Deng, W., Dwyer, M., Jung, G., Ranganath, V.P.: Cadena: An integrated development, analysis, and verification environment for component-based systems. In: Proceedings of the 25th International Conference on Software Engineering. IEEE Press, Los Alamitos (2003)"},{"key":"11_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/10722167_6","volume-title":"Computer Aided Verification","author":"T. Heyman","year":"2000","unstructured":"Heyman, T., Geist, D., Grumberg, O., Schuster, A.: Achieving scalability in parallel reachability analysis of very large circuits. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 20\u201335. Springer, Heidelberg (2000)"},{"issue":"5","key":"11_CR15","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Transactions on Software Engineering\u00a023(5), 279\u2013294 (1997)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"11_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/3-540-46017-9_5","volume-title":"Model Checking Software","author":"R. Iosif","year":"2002","unstructured":"Iosif, R.: Symmetry Reduction Criteria for Software Model Checking. In: Bo\u0161na\u010dki, D., Leue, S. (eds.) SPIN 2002. LNCS, vol.\u00a02318, pp. 22\u201341. Springer, Heidelberg (2002)"},{"key":"11_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-540-24732-6_10","volume-title":"Model Checking Software","author":"M. Jones","year":"2004","unstructured":"Jones, M., Mercer, E.G.: Explicit State Model Checking with Hopper. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol.\u00a02989, pp. 146\u2013150. Springer, Heidelberg (2004)"},{"key":"11_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/3-540-45139-0_6","volume-title":"Model Checking Software","author":"F. Lerda","year":"2001","unstructured":"Lerda, F., Visser, W.: Addressing Dynamic Issues of Program Model Checking. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol.\u00a02057, pp. 80\u2013102. Springer, Heidelberg (2001)"},{"key":"11_CR19","doi-asserted-by":"crossref","unstructured":"Robby, M.B., Dwyer, B., Hatcliff, J.: Bogor: An extensible and highly-modular model checking framework. In: Proceedings of the 9th European Software Engineering Conference held jointly with the 11th ACM SIGSOFT Symposium on the Foundations of Software Engineering (2003)","DOI":"10.1145\/940071.940107"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11925040_11.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T14:59:44Z","timestamp":1605625184000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11925040_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540489283","9783540489290"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/11925040_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}