{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,11]],"date-time":"2025-07-11T10:49:38Z","timestamp":1752230978523},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540203032"},{"type":"electronic","value":"9783540396567"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-39656-7_6","type":"book-chapter","created":{"date-parts":[[2010,6,29]],"date-time":"2010-06-29T18:35:52Z","timestamp":1277836552000},"page":"154-181","source":"Crossref","is-referenced-by-count":12,"title":["Model-Checking Middleware-Based Event-Driven Real-Time Embedded Software"],"prefix":"10.1007","author":[{"given":"Xianghua","family":"Deng","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matthew B.","family":"Dwyer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John","family":"Hatcliff","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Georg","family":"Jung","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"family":"Robby","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gurdip","family":"Singh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"6_CR1","doi-asserted-by":"crossref","unstructured":"Allen, R., Garlan, D.: A formal basis for architectural connection. ACM Transactions on Software Engineering and Methodology (July 1997)","DOI":"10.1145\/258077.258078"},{"key":"6_CR2","unstructured":"Bosnacki, D., Dams, D., Holenderski, L.: Symmetric spin. International Journal on Software Tools for Technology Transfer. Springer-Verlag (2002)"},{"key":"6_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)"},{"key":"6_CR4","volume-title":"Model Checking","author":"E. Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)"},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., P\u0103s\u0103reanu, C.S., Robby, Zheng, H.: Bandera: Extracting finite-state models from Java source code. In: Proceedings of the 22nd International Conference on Software Engineering (June 2000)","DOI":"10.1145\/337180.337234"},{"key":"6_CR6","unstructured":"de Niz, D., Rajkumar, R.: Geodesic - a reusable component framework for embedded real-time systems. Technical report, Carnegie Mellon University (2002)"},{"key":"6_CR7","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, p. 261. Springer, Heidelberg (1999)"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"Deng, W., Dwyer, M., Hatcliff, J., Jung, G., Robby, Singh, G.: Model-checking middleware-based event-driven real-time embedded software (extended version) (April 2003) (forthcoming)","DOI":"10.1007\/978-3-540-39656-7_6"},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"Doerr, B., Sharp, D.: Freeing product line architectures from execution dependencies. In: Proceedings of the Software Technology Conference (May 1999)","DOI":"10.1007\/978-1-4615-4339-8_17"},{"key":"6_CR10","unstructured":"Eclipse Consortium. Eclipse website (2001), http:\/\/www.eclipse.org"},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"Garlan, D., Khersonsky, S.: Model checking implicit-invocation systems. In: Proceedings of the 10th International Workshop on Software Specification and Design (November 2000)","DOI":"10.1109\/IWSSD.2000.891123"},{"key":"6_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/978-3-540-39656-7_19","volume-title":"Formal Methods for Components and Objects","author":"G. Goessler","year":"2003","unstructured":"Goessler, G., Sifakis, J.: Composition for component-based modeling. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2002. LNCS, vol.\u00a02852, pp. 443\u2013466. Springer, Heidelberg (2003)"},{"key":"6_CR13","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1145\/263698.263734","volume-title":"Proceedings of the 1997 ACM SIGPLAN conference on Object-oriented programming systems, languages and applications","author":"T.H. Harrison","year":"1997","unstructured":"Harrison, T.H., Levine, D.L., Schmidt, D.C.: The design and performance of a real-time corba event service. In: Proceedings of the 1997 ACM SIGPLAN conference on Object-oriented programming systems, languages and applications, pp. 184\u2013200. ACM Press, New York (1997)"},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"Hatcliff, J., Deng, W., Dwyer, M., Jung, G., Prasad, V.: Cadena: An integrated development, analysis, and verification environment for component-based systems. In: Proceedings of the 25th International Conference on Software Engineering (2003) (to appear)","DOI":"10.1109\/ICSE.2003.1201197"},{"key":"6_CR15","doi-asserted-by":"crossref","unstructured":"Havelund, K., Pressburger, T.: Model checking Java programs using Java PathFinder. International Journal on Software Tools for Technology Transfer (1999)","DOI":"10.1007\/s100090050043"},{"issue":"5","key":"6_CR16","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":"6_CR17","unstructured":"Holzmann, G.J.: State compression in SPIN: Recursive indexing and compression training runs. In: Proceedings of Third International SPIN Workshop (April 1997)"},{"key":"6_CR18","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)"},{"issue":"6","key":"6_CR19","doi-asserted-by":"publisher","first-page":"637","DOI":"10.1007\/s001659970003","volume":"11","author":"D. Latella","year":"1999","unstructured":"Latella, D., Majzik, I., Massink, M.: Automatic verification of a behavioural subset of UML statechart diagrams using the SPIN model-checker. Formal Aspects of Computing\u00a011(6), 637\u2013664 (1999)","journal-title":"Formal Aspects of Computing"},{"key":"6_CR20","unstructured":"Lee, E.A.: Overview of the ptolemy project. Technical Report UCB\/ERL M01\/11, University of California, Berkeley (March 2001)"},{"key":"6_CR21","doi-asserted-by":"crossref","unstructured":"Lilius, J., Paltor, I.P.: vUML: A tool for verifying UML models. In: Proceedings of the 14th IEEE International Conference on Automated Software Engineering (1999)","DOI":"10.1109\/ASE.1999.802301"},{"key":"6_CR22","doi-asserted-by":"crossref","unstructured":"Robby, Dwyer, M.B., Hatcliff, J.: Bogor: An extensible and highly-modular model checking framework. In: Proceedings of the 2003 ACM Symposium on Foundations of Software Engineering, FSE 2003 (2003)","DOI":"10.1145\/949952.940107"},{"key":"6_CR23","doi-asserted-by":"crossref","unstructured":"Robby, Dwyer, M.B., Hatcliff, J.: Bogor Website (2003), http:\/\/www.cis.ksu.edu\/bandera\/bogor","DOI":"10.1145\/949952.940107"},{"key":"6_CR24","unstructured":"Sipma, H.: Event correlation: A formal approach. Technical Report Draft, Stanford University (July 2002)"},{"key":"6_CR25","unstructured":"Vestal, S.: Metah user\u2019s manual (1998), http:\/\/www.htc.honeywell.com\/metah"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Components and Objects"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-39656-7_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T14:56:58Z","timestamp":1559228218000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-39656-7_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540203032","9783540396567"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-39656-7_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}