{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:25:53Z","timestamp":1725488753155},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540421245"},{"type":"electronic","value":"9783540451396"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45139-0_10","type":"book-chapter","created":{"date-parts":[[2007,8,10]],"date-time":"2007-08-10T10:39:56Z","timestamp":1186742396000},"page":"163-182","source":"Crossref","is-referenced-by-count":5,"title":["Behavioural analysis of the enterprise javaBeans\u2122 component architecture"],"prefix":"10.1007","author":[{"given":"Shin","family":"Nakajima","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tetsuo","family":"Tamai","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,5,2]]},"reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"Allen, R. and Garlan, D.: Formalizing Architectural Connection, Proc. ACM\/IEEE ICSE\u201994 (1994).","DOI":"10.1109\/ICSE.1994.296767"},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"Allen, R., Garlan, D., and Ivers, J.: Formal Modeling and Analysis of the HLA Component Integration Standard, Proc. ACM SIGSOFT FSE\u201998, pp.70\u201379 (1998).","DOI":"10.1145\/288195.288251"},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., and Corbett, J.C.: Patterns in Property Specifications for Finite-State Verification, Proc. ACM\/IEEE ICSE\u201999 (1999).","DOI":"10.1145\/302405.302672"},{"key":"10_CR4","unstructured":"Godefroid, P. and Holzmann, G.J.: On the Verification of Temporal Properties, in Proc. PSTV\u201993, pp.109\u2013124 (1993)."},{"key":"10_CR5","first-page":"279","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The Model Checker SPIN, IEEE trans. SE, vol.23, no.5, pp.279\u2013295 (1997).","journal-title":"The Model Checker SPIN"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J. and Smith, M.H.: Software Model Checking: Extracting Verification Models from Source Code, Proc. FORTE\/PSTV\u201999 (1999).","DOI":"10.1007\/978-0-387-35578-8_28"},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"Jackson, D. and Sullivan, K.: COM Revisited: Tool-Assisted Modelling and Analysis of Complex Software Structures, Proc. ACM SIGSOFT FSE\u201900 (2000).","DOI":"10.1145\/355045.355065"},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Janssen, W., Mateescu, R., Mauw, S., Frennema, P., and van der Stappen, P.: Model Checking for Managers, Proc. 6th SPIN Workshop (1999).","DOI":"10.1007\/3-540-48234-2_7"},{"issue":"10","key":"10_CR9","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1145\/352183.352199","volume":"43","author":"C. Kobryn","year":"2000","unstructured":"Kobryn, C.: Modeling Components and Frameworks with UML, Comm. ACM, vol.43 no.10, pp.31\u201338 (2000).","journal-title":"Comm. ACM"},{"key":"10_CR10","unstructured":"Leavens, G. and Sitaraman, M. (ed.): Foundations of Component-based Systems, Cambridge University Press 2000."},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"Magee, J., Kramer, J., and Giannakopoulou, D.: Analysing the Behaviour of Distributed Software Architectures: a Case Study, Proc. IEEE FTDCS\u201997 (1997).","DOI":"10.1109\/FTDCS.1997.644733"},{"key":"10_CR12","unstructured":"Magee, J., Kramer, J., and Giannakopoulou, D.: Software Architecture Directed Behavior Analysis, Proc. IEEE IWSSD\u201998, pp.144\u2013146 (1998)."},{"key":"10_CR13","doi-asserted-by":"crossref","unstructured":"Manna, Z. and Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification, Springer-Verlag 1991.","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"10_CR14","unstructured":"OMG: OMG Unified Modeling Language Specification v1.3 (2000)."},{"key":"10_CR15","unstructured":"Roscoe, A.W.: The Theory and Practice of Concurrency, Prentice Hall 1998."},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"Rushby, J.: Mechanized Formal Methods: Where Next?, Proc. FM\u201999, pp.48\u201351 (1999).","DOI":"10.1007\/3-540-48119-2_3"},{"key":"10_CR17","unstructured":"Shaw, M. and Garlan, D.: Software Architecture, Prentice Hall 1996."},{"key":"10_CR18","doi-asserted-by":"crossref","unstructured":"Sousa, J. and Garlan, D.: Formal Modeling of the Enterprise JavaBeans\u2122 Component Integration Framework, Proc. FM\u201999, pp.1281\u20131300 (1999).","DOI":"10.1007\/3-540-48118-4_18"},{"issue":"4","key":"10_CR19","first-page":"584","volume":"25","author":"K. Sullivan","year":"1999","unstructured":"Sullivan, K., Marchukov, M., and Socha, J.: Analysis of a Conflict Between Aggregation and Interface Negotiation in Microsoft\u2019s Component Object Model, IEEE trans. SE, vol.25, no.4, pp.584\u2013599 (1999).","journal-title":"Analysis of a Conflict Between Aggregation and Interface Negotiation in Microsoft\u2019s Component Object Model"},{"key":"10_CR20","unstructured":"Sun Microsystems, Inc.: Enterprise JavaBeans\u2122 Specification, v1.1 (1999)."},{"key":"10_CR21","unstructured":"Szyperski, C.: Components and the Way Ahead, in [10], pp.1\u201320 (2000)."}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45139-0_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,25]],"date-time":"2020-04-25T15:39:02Z","timestamp":1587829142000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45139-0_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540421245","9783540451396"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-45139-0_10","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}