{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:50:54Z","timestamp":1725490254333},"publisher-location":"Berlin, Heidelberg","reference-count":39,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540665878"},{"type":"electronic","value":"9783540481195"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48119-2_32","type":"book-chapter","created":{"date-parts":[[2007,8,28]],"date-time":"2007-08-28T21:23:00Z","timestamp":1188336180000},"page":"570-589","source":"Crossref","is-referenced-by-count":6,"title":["Towards a Compositional Approach to the Design and Verification of Distributed Systems"],"prefix":"10.1007","author":[{"given":"Michel","family":"Charpentier","sequence":"first","affiliation":[]},{"given":"K. Mani","family":"Chandy","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[1999,9,17]]},"reference":[{"issue":"1","key":"32_CR1","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1145\/151646.151649","volume":"15","author":"M. Abadi","year":"1993","unstructured":"M. Abadi and L. Lamport. Composing specifications. ACM Transactions on Programming Languages and Systems, 15(1):73\u2013132, Jan. 1993.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"3","key":"32_CR2","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1145\/203095.201069","volume":"17","author":"M. Abadi","year":"1995","unstructured":"M. Abadi and L. Lamport. Conjoining specifications. ACM Transactions on Programming Languages and Systems, 17(3):507\u2013534, May 1995.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"32_CR3","series-title":"Lect Notes Comput Sci","first-page":"42","volume-title":"REX Workshop on Stepwise Refinement of Distributed Systems","author":"R. Back","year":"1989","unstructured":"R. Back. Refinement calculus, Part I: Sequential nondeterministic programs. In REX Workshop on Stepwise Refinement of Distributed Systems, volume 430 of Lecture Notes in Computer Science, pages 42\u201366. Springer-Verlag, 1989."},{"key":"32_CR4","series-title":"Lect Notes Comput Sci","first-page":"67","volume-title":"REX Workshop on Stepwise Refinement of Distributed Systems","author":"R. Back","year":"1989","unstructured":"R. Back. Refinement calculus, Part II: Parallel and reactive programs. In REX Workshop on Stepwise Refinement of Distributed Systems, volume 430 of Lecture Notes in Computer Science, pages 67\u201393. Springer-Verlag, 1989."},{"key":"32_CR5","doi-asserted-by":"crossref","unstructured":"K. M. Chandy and J. Misra. Parallel Program Design: A Foundation. Addison-Wesley, 1988.","DOI":"10.1007\/978-1-4613-9668-0_6"},{"key":"32_CR6","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1016\/0167-6423(94)00033-B","volume":"24","author":"K. M. Chandy","year":"1995","unstructured":"K. M. Chandy and B. A. Sanders. Predicate transformers for reasoning about concurrent computation. Science of Computer Programming, 24:129\u2013148, 1995.","journal-title":"Science of Computer Programming"},{"key":"32_CR7","series-title":"Technical Report","volume-title":"Reasoning about program composition","author":"K. M. Chandy","year":"1996","unstructured":"K. M. Chandy and B. A. Sanders. Reasoning about program composition. Technical Report 96-035, University of Florida, Department of Computer and Information Science and Engineering, 1996."},{"key":"32_CR8","unstructured":"D. Chappell. Understanding ActiveX and OLE. Microsoft Press, 1996."},{"key":"32_CR9","series-title":"PhD thesis","volume-title":"Assistance \u00e0 la R\u00e9partition de Syst\u00e8mes R\u00e9actifs","author":"M. Charpentier","year":"1997","unstructured":"M. Charpentier. Assistance \u00e0 la R\u00e9partition de Syst\u00e8mes R\u00e9actifs. PhD thesis, Institut National Polytechnique de Toulouse, France, Nov. 1997."},{"key":"32_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"1215","DOI":"10.1007\/BFb0098004","volume-title":"International workshop on Formal Methods for Parallel Programming: Theory and Applications (FMPPTA\u201999)","author":"M. Charpentier","year":"1999","unstructured":"M. Charpentier and K. M. Chandy. Examples of program composition illustrating the use of universal properties. In J. Rolim, editor, International workshop on Formal Methods for Parallel Programming: Theory and Applications (FMPPTA\u201999), volume 1586 of Lecture Notes in Computer Science, pages 1215\u20131227. Springer-Verlag, Apr. 1999."},{"key":"32_CR11","doi-asserted-by":"crossref","unstructured":"M. Charpentier and K. M. Chandy. Towards a compositional approach to the design and verification of distributed systems. Technical Report CS-TR-99-02, California Institute of Technology, Jan. 1999. 29 pages.","DOI":"10.21236\/ADA451478"},{"key":"32_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1007\/3-540-61769-8_7","volume-title":"Tenth International Workshop on Distributed Algorithms (WDAG\u201996)","author":"M. Charpentier","year":"1996","unstructured":"M. Charpentier, M. Filali, P. Mauran, G. Padiou, and P. Qu\u00e9innec. Abstracting communication to reason about distributed algorithms. In \u00d6. Babao\u011flu and K. Marzullo, editors, Tenth International Workshop on Distributed Algorithms (WDAG\u201996), volume 1151 of Lecture Notes in Computer Science, pages 89\u2013104. Springer-Verlag, October 1996."},{"key":"32_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"820","DOI":"10.1007\/3-540-64359-1_745","volume-title":"International workshop on Formal Methods for Parallel Programming: Theory and Applications (FMPPTA\u201998)","author":"M. Charpentier","year":"1998","unstructured":"M. Charpentier, M. Filali, P. Mauran, G. Padiou, and P. Qu\u00e9innec. Tailoring Unity to distributed program design. In J. Rolim, editor, International workshop on Formal Methods for Parallel Programming: Theory and Applications (FMPPTA\u201998), volume 1388 of Lecture Notes in Computer Science, pages 820\u2013832. Springer-Verlag, April 1998."},{"key":"32_CR14","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1016\/0167-6423(94)00017-4","volume":"23","author":"P. Collette","year":"1994","unstructured":"P. Collette. Composition of assumption-commitment specifications in a Unity style. Science of Computer Programming, 23:107\u2013125, 1994.","journal-title":"Science of Computer Programming"},{"key":"32_CR15","series-title":"Doctoral thesis","volume-title":"Design of Compositional Proof Systems Based on Assumption-Commitment Specifications. Application to Unity","author":"P. Collette","year":"1994","unstructured":"P. Collette. Design of Compositional Proof Systems Based on Assumption-Commitment Specifications. Application to Unity. Doctoral thesis, Facult\u00e9 des Sciences Appliqu\u00e9es, Universit\u00e9 Catholique de Louvain, June 1994."},{"key":"32_CR16","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1016\/0304-3975(91)90029-2","volume":"87","author":"P. Gardiner","year":"1991","unstructured":"P. Gardiner and C. Morgan. Data refinement of predicate transformers. Theoretical Computer Science, 87:143\u2013162, 1991.","journal-title":"Theoretical Computer Science"},{"key":"32_CR17","unstructured":"D. Garlan. Higher-order connectors. In Proceedings of Workshop on Compositional Software Architectures, Monterey, California, Jan. 1998."},{"key":"32_CR18","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1145\/97945.97967","volume":"25\/10","author":"R. Helm","year":"1990","unstructured":"R. Helm, I. M. Holland, and D. Gangopadhyay. Contracts: Specifying behavioral compositions in object-oriented systems. In European Conference on Object-Oriented Programming\/ACM Conference on Object-Oriented Programming Systems, Languages, and Applications, volume 25\/10, pages 169\u2013180, 1990.","journal-title":"European Conference on Object-Oriented Programming\/ACM Conference on Object-Oriented Programming Systems, Languages, and Applications"},{"issue":"4","key":"32_CR19","doi-asserted-by":"publisher","first-page":"596","DOI":"10.1145\/69575.69577","volume":"5","author":"C. Jones","year":"1983","unstructured":"C. Jones. Tentative steps toward a development method for interfering programs. ACM Transactions on Programming Languages and Systems, 5(4):596\u2013619, 1983.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"32_CR20","unstructured":"J. R. Kiniry. CDL: A component description language. In Proceedings of the COOTS\u2019 99 Advanced Topics Workshop on Validating the Composition\/Execution of Component-Based Systems, 1999."},{"issue":"1","key":"32_CR21","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/BF02276640","volume":"6","author":"S. Lam","year":"1992","unstructured":"S. Lam and A. Shankar. Specifying modules to satisfy interfaces-a state transition approach. Distributed Computing, 6(1):39\u201363, July 1992.","journal-title":"Distributed Computing"},{"issue":"1","key":"32_CR22","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1109\/32.263755","volume":"20","author":"S. Lam","year":"1994","unstructured":"S. Lam and A. Shankar. A theory of interfaces and modules 1: Composition theorem. IEEE Transactions on Software Engineering, 20(1):55\u201371, Jan. 1994.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"32_CR23","unstructured":"R. Manohar and P. Sivilotti. Composing processes using modified rely-guarantee specifications. Technical Report CS-TR-96-22, California Institute of Technology, 1996."},{"key":"32_CR24","unstructured":"B. Meyer. Object-Oriented Software Construction. Prentice-Hall, Inc., 2nd edition, 1988."},{"key":"32_CR25","doi-asserted-by":"crossref","unstructured":"B. Meyer. Applying design by contract. IEEE Computer, Oct. 1992.","DOI":"10.1109\/2.161279"},{"key":"32_CR26","doi-asserted-by":"crossref","unstructured":"R. Milner, M. Tofte, R. Harper, and D. MacQueen. The Definition of Standard ML (Revised). The MIT Press, 1997.","DOI":"10.7551\/mitpress\/2319.001.0001"},{"issue":"2","key":"32_CR27","first-page":"273","volume":"3","author":"J. Misra","year":"1995","unstructured":"J. Misra. A logic for concurrent programming: Progress. Journal of Computer and Software Engineering, 3(2):273\u2013300, 1995.","journal-title":"Journal of Computer and Software Engineering"},{"issue":"2","key":"32_CR28","first-page":"239","volume":"3","author":"J. Misra","year":"1995","unstructured":"J. Misra. A logic for concurrent programming: Safety. Journal of Computer and Software Engineering, 3(2):239\u2013272, 1995.","journal-title":"Journal of Computer and Software Engineering"},{"issue":"9","key":"32_CR29","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1145\/130994.131005","volume":"35","author":"O. Nierstrasz","year":"1992","unstructured":"O. Nierstrasz, S. Gibbs, and D. Tsichritzis. Component-oriented software development. Communications of the ACM, 35(9):160\u2013165, Sept. 1992.","journal-title":"Communications of the ACM"},{"key":"32_CR30","doi-asserted-by":"crossref","unstructured":"O. Nierstrasz and T. Meijler. Requirements for a composition language. In ECOOP\u201994 Workshop on Models and Languages for Coordination of Parallelism and Distribution, pages 147\u2013161. Springer-Verlag, 1995.","DOI":"10.1007\/3-540-59450-7_9"},{"key":"32_CR31","unstructured":"O. Nierstrasz and D. Tsichritzis, editors. Object-Oriented Software Composition. Prentice-Hall, Inc., 1995."},{"key":"32_CR32","unstructured":"Object Management Group (OMG). The Common Object Request Broker: Architecture and Specification (CORBA), revision 2.0. Object Management Group (OMG), 2.0 edition."},{"key":"32_CR33","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A Generic Theorem Prover","author":"L. C. Paulson","year":"1994","unstructured":"L. C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of Lecture Notes in Computer Science. Springer-Verlag, 1994."},{"issue":"2","key":"32_CR34","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/BF01898402","volume":"3","author":"B. A. Sanders","year":"1991","unstructured":"B. A. Sanders. Eliminating the substitution axiom from Unity logic. Formal Aspects of Computing, 3(2):189\u2013205, April-June 1991.","journal-title":"Formal Aspects of Computing"},{"issue":"2","key":"32_CR35","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/s002360050115","volume":"35","author":"B. A. Sanders","year":"1998","unstructured":"B. A. Sanders. Data refinement of mixed specification: A generalization of Unity. Acta Informatica, 35(2):91\u2013129, 1998.","journal-title":"Acta Informatica"},{"key":"32_CR36","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49213-5_21","volume-title":"Compositionality: The Significant Difference. International Symposium, COMPOS\u201997","author":"N. Shankar","year":"1998","unstructured":"N. Shankar. Lazy compositional verification. In Compositionality: The Significant Difference. International Symposium, COMPOS\u201997, volume 1536 of Lecture Notes in Computer Science. Springer-Verlag, 1998."},{"key":"32_CR37","unstructured":"P. A. G. Sivilotti. A Method for the Specification, Composition, and Testing of Distributed Object Systems. PhD thesis, California Institute of Technology, 256\u201380 Caltech, Pasadena, California 91125, Dec. 1997."},{"key":"32_CR38","unstructured":"Sun Microsystems, Inc. JavaBeans API specification, version 1.01. Technical report, Sun Microsystems, Inc., July 1997."},{"key":"32_CR39","unstructured":"C. Szyperski. Component Software: Beyond Object-Oriented Programming. Addison-Wesley Publishing Company, 1997."}],"container-title":["Lecture Notes in Computer Science","FM\u201999 \u2014 Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48119-2_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,2]],"date-time":"2019-05-02T13:27:28Z","timestamp":1556803648000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48119-2_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540665878","9783540481195"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/3-540-48119-2_32","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}