{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,10]],"date-time":"2025-01-10T12:40:03Z","timestamp":1736512803336,"version":"3.32.0"},"publisher-location":"Berlin, Heidelberg","reference-count":40,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540356288"},{"type":"electronic","value":"9783540356295"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11783565_3","type":"book-chapter","created":{"date-parts":[[2006,6,21]],"date-time":"2006-06-21T12:08:03Z","timestamp":1150891683000},"page":"33-49","source":"Crossref","is-referenced-by-count":0,"title":["Behavioral Compatibility Without State Explosion: Design and Verification of a Component-Based Elevator Control System"],"prefix":"10.1007","author":[{"given":"Paul C.","family":"Attie","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David H.","family":"Lorenz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aleksandra","family":"Portnova","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hana","family":"Chockler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1","key":"3_CR1","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1145\/151646.151649","volume":"15","author":"M. Abadi","year":"1993","unstructured":"Abadi, M., Lamport, L.: Composing specifications. ACM Transactions on Programming Languages and Systems\u00a015(1), 73\u2013132 (1993)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"3_CR2","first-page":"109","volume-title":"Proceedings of the 9th Annual Symposium on Foundations of Software Engineering (FSE)","author":"L. Alfaro de","year":"2001","unstructured":"de Alfaro, L., Henzinger, T.A.: Interface automata. In: Proceedings of the 9th Annual Symposium on Foundations of Software Engineering (FSE), pp. 109\u2013120. ACM Press, New York (2001)"},{"key":"3_CR3","unstructured":"Attie, P.C., Chockler, H.: Automatic verification of fault-tolerant register emulations. In: Proceedings of the Infinity 2005 workshop (2005)"},{"issue":"1","key":"3_CR4","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1145\/271510.271519","volume":"20","author":"P.C. Attie","year":"1998","unstructured":"Attie, P.C., Emerson, E.A.: Synthesis of concurrent systems with many similar processes. ACM Transactions on Programming Languages and Systems\u00a020(1), 51\u2013115 (1998)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"3_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48320-9_11","volume-title":"CONCUR\u201999. Concurrency Theory","author":"P.C. Attie","year":"1999","unstructured":"Attie, P.C.: Synthesis of large concurrent programs via pairwise composition. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol.\u00a01664. Springer, Heidelberg (1999)"},{"key":"3_CR6","unstructured":"Attie, P.C.: Synthesis of large dynamic concurrent programs from dynamic specifications. Technical report, American University of Beirut (2005), available at: http:\/\/www.cs.aub.edu.lb\/pa07\/files\/pubs.html"},{"key":"3_CR7","unstructured":"Attie, P.C., Lorenz, D.H.: Correctness of model-based component composition without state explosion. In: ECOOP 2003 Workshop on Correctness of Model-based Software Composition (2003)"},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-62927-0","volume-title":"Software Engineering - ESEC-FSE \u201997","author":"S. Cheung","year":"1997","unstructured":"Cheung, S., Giannakopoulou, D., Kramer, J.: Verification of liveness properties in compositional reachability analysis. In: Jazayeri, M. (ed.) ESEC 1997 and ESEC-FSE 1997. LNCS, vol.\u00a01301. Springer, Heidelberg (1997)"},{"key":"3_CR9","volume-title":"Proceedings of the 18 th International Conference on Software Engineering, ICSE 1996","author":"S. Cheung","year":"1996","unstructured":"Cheung, S., Kramer, J.: Checking subsystem safety properties in compositional reachability analysis. In: Proceedings of the 18 th International Conference on Software Engineering, ICSE 1996, Berlin, Germany. IEEE Computer Society Press, Los Alamitos (1996)"},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"Clarke, E., Enders, R., Filkorn, T., Jha, S.: Exploiting symmetry in temporal logic model checking. Formal Methods in System Design\u00a09(2) (1996)","DOI":"10.1007\/BF00625969"},{"key":"3_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"450","DOI":"10.1007\/3-540-56922-7_37","volume-title":"Computer Aided Verification","author":"E.M. Clarke","year":"1993","unstructured":"Clarke, E.M., Filkorn, T., Jha, S.: Exploiting symmetry in temporal logic model checking. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697, pp. 450\u2013462. Springer, Heidelberg (1993)"},{"issue":"5","key":"3_CR12","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E. Clarke","year":"1994","unstructured":"Clarke, E., Grumberg, O., Long, D.: Model checking and abstraction. ACM Transactions on Programming Languages and Systems\u00a016(5), 1512\u20131542 (1994)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"3_CR13","volume-title":"Proceedings of the 4 th IEEE Symposium on Logic in Computer Science","author":"E.M. Clarke","year":"1989","unstructured":"Clarke, E.M., Long, D., McMillan, K.L.: Compositional model checking. In: Proceedings of the 4 th IEEE Symposium on Logic in Computer Science. IEEE, New York (1989)"},{"volume-title":"Proceedings of the 4 th ICSE Workshop on Component-Based Software Engineering: Component Certification and System Prediction","year":"2001","key":"3_CR14","unstructured":"Crnkovic, I., Schmidt, H., Stafford, J., Wallnau, K. (eds.): Proceedings of the 4 th ICSE Workshop on Component-Based Software Engineering: Component Certification and System Prediction, Toronto, Canada. IEEE Computer Society, Los Alamitos (2001)"},{"key":"3_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"463","DOI":"10.1007\/3-540-56922-7_38","volume-title":"Computer Aided Verification","author":"E.A. Emerson","year":"1993","unstructured":"Emerson, E.A., Sistla, A.P.: Symmetry and model checking. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697, pp. 463\u2013477. Springer, Heidelberg (1993)"},{"issue":"1\/2","key":"3_CR16","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/BF00625970","volume":"9","author":"E.A. Emerson","year":"1996","unstructured":"Emerson, E.A., Sistla, A.P.: Symmetry and model checking. Formal Methods in System Design: An International Journal\u00a09(1\/2), 105\u2013131 (1996)","journal-title":"Formal Methods in System Design: An International Journal"},{"key":"3_CR17","series-title":"Formal Models and Semantics","volume-title":"Handbook of Theoretical Computer Science","author":"E.A. Emerson","year":"1990","unstructured":"Emerson, E.A.: Temporal and modal logic. In: Leeuwen, J.V. (ed.) Handbook of Theoretical Computer Science. Formal Models and Semantics, vol.\u00a0B. MIT Press\/Elsevier, Cambridge (1990)"},{"issue":"3","key":"3_CR18","doi-asserted-by":"publisher","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O. Grumberg","year":"1994","unstructured":"Grumberg, O., Long, D.: Model checking and modular verification. ACM Transactions on Programming Languages and Systems\u00a016(3), 843\u2013871 (1994)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"volume-title":"Component-Based Software Engineering: Putting the Pieces Together","year":"2001","key":"3_CR19","unstructured":"Heineman, G.T., Councill, W.T. (eds.): Component-Based Software Engineering: Putting the Pieces Together. Addison-Wesley, Reading (2001)"},{"key":"3_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-64358-3","volume-title":"Computer Aided Verification","author":"T.A. Henzinger","year":"1998","unstructured":"Henzinger, T.A., Qadeer, S., Rajamani, S.K.: You assume, we guarantee: Methodology and case studies. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427. Springer, Heidelberg (1998)"},{"key":"3_CR21","volume-title":"The SPIN Model Checker","author":"G.J. Holzmann","year":"2003","unstructured":"Holzmann, G.J.: The SPIN Model Checker. Addison-Wesley, San Francisco (2003)"},{"key":"3_CR22","unstructured":"Proceedings of the 23 rd International Conference on Software Engineering, ICSE 2001, Toronto, Canada. IEEE Computer Society, Los Alamitos (2001)"},{"issue":"1","key":"3_CR23","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1006\/inco.2000.3000","volume":"163","author":"Y. Kesten","year":"2000","unstructured":"Kesten, Y., Pnueli, A.: Verification by augmented finitary abstraction. Information and Computation\u00a0163(1), 203\u2013243 (2000)","journal-title":"Information and Computation"},{"issue":"4","key":"3_CR24","doi-asserted-by":"publisher","first-page":"668","DOI":"10.1006\/jcss.2000.1744","volume":"62","author":"Y. Kesten","year":"2001","unstructured":"Kesten, Y., Pnueli, A., Vardi, M.Y.: Verification by augmented abstraction: The automata-theoretic view. Journal of Computer and System Sciences\u00a062(4), 668\u2013690 (2001)","journal-title":"Journal of Computer and System Sciences"},{"key":"3_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"402","DOI":"10.1007\/3-540-49213-5_15","volume-title":"Compositionality: The Significant Difference","author":"L. Lamport","year":"1998","unstructured":"Lamport, L.: Composition: A way to make proofs harder. In: de Roever, W.P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol.\u00a01536, pp. 402\u2013423. Springer, Heidelberg (1998)"},{"key":"3_CR26","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1145\/367845.367951","volume-title":"Proceedings of the 15 th Annual Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA 2000","author":"D.H. Lorenz","year":"2000","unstructured":"Lorenz, D.H., Petkovic, P.: ContextBox: A visual builder for context beans (extended abstract). In: Proceedings of the 15 th Annual Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA 2000, pp. 75\u201376. ACM SIGPLAN, Minnesota (2000)"},{"key":"3_CR27","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1109\/TOOLS.2000.868971","volume-title":"Proceedings of the 34 th International Conference on Technology of Object-Oriented Languages and Systems","author":"D.H. Lorenz","year":"2000","unstructured":"Lorenz, D.H., Petkovic, P.: Design-time assembly of runtime containment components. In: Li, Q., Firesmith, D., Riehle, R., Pour, G., Meyer, B. (eds.) Proceedings of the 34 th International Conference on Technology of Object-Oriented Languages and Systems, Santa Barbara, CA, pp. 195\u2013204. IEEE Computer Society, Los Alamitos (2000)"},{"key":"3_CR28","doi-asserted-by":"crossref","unstructured":"Lorenz, D.H., Vlissides, J.: Designing components versus objects: A transformational approach. In: [22], pp. 253\u2013262 (2001)","DOI":"10.1109\/ICSE.2001.919099"},{"key":"3_CR29","unstructured":"Lynch, N., Tuttle, M.: An introduction to input\/output automata. CWI-Quarterly 2(3), Centrum voor Wiskunde en Informatica, Amsterdam, The Netherlands, 219\u2013246 (1989)"},{"issue":"2","key":"3_CR30","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1006\/inco.1995.1134","volume":"121","author":"N. Lynch","year":"1995","unstructured":"Lynch, N., Vaandrager, F.: Forward and backward simulations \u2014 part I: Untimed systems. Information and Computation\u00a0121(2), 214\u2013233 (1995)","journal-title":"Information and Computation"},{"key":"3_CR31","volume-title":"Distributed Algorithms","author":"N.A. Lynch","year":"1996","unstructured":"Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann, San Francisco (1996)"},{"key":"3_CR32","doi-asserted-by":"crossref","unstructured":"M\u00e4kinen, E., Syst\u00e4, T.: MAS - an interactive synthesizer to support behavioral modeling in UML. In: [22], pp. 15\u201324 (2001)","DOI":"10.1109\/ICSE.2001.919077"},{"key":"3_CR33","first-page":"46","volume-title":"IEEE Symposium on Foundations of Computer Science","author":"A. Pnueli","year":"1977","unstructured":"Pnueli, A.: The temporal logic of programs. In: IEEE Symposium on Foundations of Computer Science, pp. 46\u201357. IEEE Press, Los Alamitos (1977)"},{"key":"3_CR34","volume-title":"Component Software, Beyond Object-Oriented Programming","author":"C. Szyperski","year":"1997","unstructured":"Szyperski, C.: Component Software, Beyond Object-Oriented Programming. Addison-Wesley, Reading (1997)"},{"key":"3_CR35","first-page":"322","volume-title":"Proceedings of the 8 th International Conference on the Engineering of Computer Based Systems, ECBS 2001","author":"W. Vanderperren","year":"2001","unstructured":"Vanderperren, W., Wydaeghe, B.: Towards a new component composition process. In: Proceedings of the 8 th International Conference on the Engineering of Computer Based Systems, ECBS 2001, pp. 322\u2013331. IEEE Computer Society, Los Alamitos (2001)"},{"key":"3_CR36","doi-asserted-by":"crossref","unstructured":"Vanderperren, W., Wydaeghe, B.: Separating concerns in a high-level component-based context. In: Easy Comp. Workshop at ETAPS 2002 (2002)","DOI":"10.1016\/S1571-0661(04)80439-0"},{"key":"3_CR37","unstructured":"Vanderperren, W.: A pattern based approach to separate tangled concerns in component based development. In: Proceedings of the 1 st AOSD Workshop on Aspects, Components, and Patterns for Infrastructure Software, ACP4IS 2002, Enschede, The Netherlands, pp. 71\u201375 (2002)"},{"key":"3_CR38","volume-title":"Software Engineering","author":"K.C. Wallnau","year":"2001","unstructured":"Wallnau, K.C., Hissam, S., Seacord, R.: Building Systems from Commercial Components. In: Software Engineering. Addison-Wesley, Reading (2001)"},{"key":"3_CR39","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1109\/TOOLS.2001.941666","volume-title":"Proceedings of the 39th International Conference on Technology of Object-Oriented Languages and Systems","author":"B. Wydaeghe","year":"2001","unstructured":"Wydaeghe, B., Vanderperren, W.: Visual component composition using composition patterns. In: Proceedings of the 39th International Conference on Technology of Object-Oriented Languages and Systems, Santa Barbara, CA, pp. 120\u2013129. IEEE Computer Society, Los Alamitos (2001)"},{"key":"3_CR40","unstructured":"Wydaeghe, B.: PACOSUITE: Component composition based on composition patterns and usage scenarios. PhD thesis (2001)"}],"container-title":["Lecture Notes in Computer Science","Component-Based Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11783565_3.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T14:05:17Z","timestamp":1736431517000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11783565_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540356288","9783540356295"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/11783565_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}