{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,11]],"date-time":"2025-07-11T10:27:43Z","timestamp":1752229663308,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540401179"},{"type":"electronic","value":"9783540448297"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-44829-2_11","type":"book-chapter","created":{"date-parts":[[2007,7,3]],"date-time":"2007-07-03T16:01:40Z","timestamp":1183478500000},"page":"166-180","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":68,"title":["Model Checking Publish-Subscribe Systems"],"prefix":"10.1007","author":[{"given":"David","family":"Garlan","sequence":"first","affiliation":[]},{"given":"Serge","family":"Khersonsky","sequence":"additional","affiliation":[]},{"given":"Jung Soo","family":"Kim","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,4,15]]},"reference":[{"issue":"5","key":"11_CR1","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1145\/167049.167055","volume":"18","author":"G. Abowd","year":"1993","unstructured":"Gregory Abowd, Robert Allen, and David Garlan. Using style to understand descriptions of software architecture. In Proceedings of SIGSOFT\u201993: Foundations of Software Engineering, Software Engineering Notes 18(5), pages 9\u201320. ACM Press, December 1993.","journal-title":"Software Engineering Notes"},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"Robert Allen and David Garlan. Formalizing architectural connection. In Proceedings of the 16th International Conference on Software Engineering, pages 71\u201380, Sorrento, Italy, May 1994.","DOI":"10.1109\/ICSE.1994.296767"},{"issue":"4","key":"11_CR3","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1145\/235321.235324","volume":"5","author":"D. J. Barrett","year":"1996","unstructured":"Daniel J. Barrett, Lori A. Clarke, Peri L. Tarr, and Alexander E. Wise. A framework for event-based software integration. ACM Transactions on Software Engineering and Methodology, 5(4):378\u2013421, October 1996.","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"A. Carzaniga, D. S. Rosenblum, and A. L. Wolf. Achieving expressiveness and scalability in an internet-scale event notification service. Proc. 19th ACM Symposium on Principles of Distributed Computing, July 2000.","DOI":"10.1145\/343477.343622"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"E. Clarke and J. Wing. Formal methods: State of the art and future directions. ACM Computing Surveys, 24(4), December 1996.","DOI":"10.1145\/242223.242257"},{"key":"11_CR6","doi-asserted-by":"crossref","unstructured":"James Corbett, Matthew Dwyer, and John Hatcliff. Bandera: Extracting finite-state models from java source code. Proceedings of the 22nd International Conference on Software Engineering, June 2000.","DOI":"10.1145\/337180.337234"},{"key":"11_CR7","unstructured":"J\u00fcrgen Dingel, David Garlan, Somesh Jha, and David Notkin. Reasoning about Implicit Invocation. In Proceedings of the Sixth International Symposium on the Foundations of Software Engineering (FSE-6), Lake Buena Vista, Florida, November 1998. ACM."},{"key":"11_CR8","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/s001650050011","volume":"10","author":"J. Dingel","year":"1998","unstructured":"J\u00fcrgen Dingel, David Garlan, Somesh Jha, and David Notkin. Towards a formal treatment of implicit invocation. Formal Aspects of Computing, 10:193\u2013213, 1998.","journal-title":"Formal Aspects of Computing"},{"key":"11_CR9","unstructured":"David Garlan and Serge Khersonsky. Model checking implicit invocation systems. In Proceedings of the 10th International Workshop on Software Specification and Design, San Diego, CA, November 2000."},{"key":"11_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/3-540-54834-3_5","volume-title":"VDM\u201991: Formal Software Development Methods","author":"D. Garlan","year":"1991","unstructured":"David Garlan and David Notkin. Formalizing design spaces: Implicit invocation mechanisms. In VDM\u201991: Formal Software Development Methods, pages 31\u201344, Noordwijkerhout, The Netherlands, October 1991. Springer-Verlag, LNCS 551."},{"key":"11_CR11","doi-asserted-by":"crossref","unstructured":"K. Havelund and T. Pressburger. Model checking java programs using Java Pathfinder. International Journal on Software Tools for Technology Transfer, STTT, 2(4), April 2000.","DOI":"10.1007\/s100090050043"},{"key":"11_CR12","unstructured":"Jeff Magee and Jeff Kramer. Concurrency: state models & JAVA programs. John Wiley & Son, April 1999."},{"key":"11_CR13","unstructured":"Ken McMillan. Cadence SMV. http:\/\/www-cad.eecs.berkeley.edu\/kenmcmil\/smv\/."},{"key":"11_CR14","unstructured":"Microsoft. Slam. http:\/\/research.microsoft.com\/slam."},{"key":"11_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"489","DOI":"10.1007\/3-540-57342-9_91","volume-title":"Proceedings of the JSSST International Symposium on Object Technologies for Advanced Software","author":"D. Notkin","year":"1993","unstructured":"David Notkin, David Garlan, William G. Griswold, and Kevin Sullivan. Adding implicit invocation to languages: Three approaches. In S. Nishio and A. Yonezawa, editors, Proceedings of the JSSST International Symposium on Object Technologies for Advanced Software, pages 489\u2013510. Springer-Verlag LNCS, No. 742, November 1993."},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"Kevin J. Sullivan and David Notkin. Reconciling environment integration and software evolution. In Proceedings of SIGSOFT\u2019 90: Fourth Symposium on Software Development Environments, Irvine, December 1990.","DOI":"10.1145\/99277.99281"},{"issue":"3","key":"11_CR17","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1145\/131736.131744","volume":"1","author":"K. J. Sullivan","year":"1992","unstructured":"Kevin J. Sullivan and David Notkin. Reconciling environment integration and software evolution. ACM Transactions on Software Engineering and Methodology, 1(3):229\u2013268, July 1992.","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"key":"11_CR18","unstructured":"Sun Microsystems. JavaBeans. http:\/\/java.sun.com\/products\/javabeans."},{"issue":"6","key":"11_CR19","doi-asserted-by":"publisher","first-page":"390","DOI":"10.1109\/32.508313","volume":"22","author":"R. N. Taylor","year":"1996","unstructured":"Richard N. Taylor, Nenad Medvidovic, Kenneth M. Anderson, Jr. E. James Whitehead, Jason E. Robbins, Kari A. Nies, Peyman Oreizy, and Deborah L. Dubrow. A component-and message-based architectural style for GUI software. IEEE Transactions on Software Engineering, 22(6):390\u2013406, June 1996.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"11_CR20","unstructured":"TIBCO The Power of Now. Tibco hawk. http:\/\/www.tibco.com\/solutions\/."}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44829-2_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,18]],"date-time":"2025-01-18T04:02:30Z","timestamp":1737172950000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/3-540-44829-2_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540401179","9783540448297"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-44829-2_11","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]},"assertion":[{"value":"15 April 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}