{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:21:47Z","timestamp":1751660507175},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540525592"},{"type":"electronic","value":"9783540470359"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1990]]},"DOI":"10.1007\/3-540-52559-9_71","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T21:36:56Z","timestamp":1330205816000},"page":"361-385","source":"Crossref","is-referenced-by-count":12,"title":["On decomposing and refining specifications of distributed systems"],"prefix":"10.1007","author":[{"given":"Bengt","family":"Jonsson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,4]]},"reference":[{"key":"13_CR1","doi-asserted-by":"crossref","unstructured":"M. Abadi and L. Lamport. The existence of refinement mappings. In Proc. 3rd IEEE Symp. on Logic in Computer Science, Edinburgh, 1988.","DOI":"10.1109\/LICS.1988.5115"},{"key":"13_CR2","unstructured":"B. Alpern and F.S. Schneider. Verifying temporal properties without using temporal logic. Technical Report TR 85-723, Cornell University, 1985."},{"key":"13_CR3","unstructured":"B. Alpern and F.S. Schneider. Proving boolean combinations of deterministic properties. In Proc. 2nd IEEE Symp. on Logic in Computer Science, 1987."},{"key":"13_CR4","unstructured":"R.J.R. Back and R. Kurki-Suonio. Distributed co-operation with action systems. Technical Report A. 56, \u00c5bo Akademi, Dept. of Computer Science and Mathematics, 1987."},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"R.J.R. Back and K. Sere. Stepwise refinement of action systems. Technical Report A. 78, \u00c5bo Akademi, Dept. of Computer Science and Mathematics, 1989.","DOI":"10.1007\/3-540-51305-1_7"},{"key":"13_CR6","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":"13_CR7","doi-asserted-by":"crossref","unstructured":"C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.","DOI":"10.1007\/978-3-642-82921-5_4"},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"B. Jonsson. A model and proof system for asynchronous networks. Proc. 4:th ACM Symp. on Principles of Distributed Computing, pages 49\u201358, Minaki, Canada, 1985.","DOI":"10.1145\/323596.323601"},{"key":"13_CR9","volume-title":"Compositional Verification of Distributed Systems","author":"B. Jonsson","year":"1987","unstructured":"B. Jonsson. Compositional Verification of Distributed Systems. PhD thesis, Dept. of Computer Systems, Uppsala University, Sweden, Uppsala, Sweden, 1987. Available as report DoCS 87\/09."},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"B. Jonsson. Modular verification of asynchronous networks. In Proc. 6th ACM Symp. on Principles of Distributed Computing, pages 152\u2013166, Vancouver, Canada, 1987.","DOI":"10.1145\/41840.41853"},{"issue":"2","key":"13_CR11","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1145\/69624.357207","volume":"5","author":"L. Lamport","year":"1983","unstructured":"L. Lamport. Specifying concurrent program modules. ACM TOPLAS, 5(2):190\u2013222, 1983.","journal-title":"ACM TOPLAS"},{"key":"13_CR12","unstructured":"S.S. Lam and A.U. Shankar. A relational notation for state transition systems. Technical Report TR-88-21, Dept. of Computer Sciences, University of Texas at Austin, 1988."},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"N. A. Lynch and M. R. Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proc. 6th ACM Symp. on Principles of Distributed Computing, pages 137\u2013151, 1987.","DOI":"10.1145\/41840.41852"},{"key":"13_CR14","unstructured":"M. Merritt. Completeness theorems for automata. In this volume."},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"R. Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes of Computer Science. Springer Verlag, 1980.","DOI":"10.1007\/3-540-10235-3"},{"key":"13_CR16","unstructured":"R. Milner. Communication and Concurrency. Prentice-Hall, 1989."},{"key":"13_CR17","unstructured":"J. Misra. Reasoning about networks of communicating processes. In INRIA Advanced Nato Study Institute on Logics and Models for Verification and Specification of Concurrent Systems, La Colle sur Loupe, France, 1984."},{"issue":"4","key":"13_CR18","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1016\/0167-6423(84)90003-0","volume":"4","author":"Z. Manna","year":"1984","unstructured":"Z. Manna and A. Pnueli. Adequate proof principles for invariance and liveness properties of concurrent programs. Science of Computer Programming, 4(4):257\u2013289, 1984.","journal-title":"Science of Computer Programming"},{"key":"13_CR19","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. Specification and verification of concurrent programs by \u2200-Automata. In Proc. 14th ACM Symp. on Principles of Programming Languages, pages 1\u201312, 1987.","DOI":"10.1145\/41625.41626"},{"key":"13_CR20","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. The anchored version of the temporal framework. In de Bakker, de Roever, and Rozenberg, editors, Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, volume 354 of Lecture Notes in Computer Science, pages 201\u2013284. Springer Verlag, 1989.","DOI":"10.1007\/BFb0013024"},{"key":"13_CR21","unstructured":"F. Orava. Verifying safety and deadlock properties of networks of asynchronously communicating processes. In Proc. 9th IFIP WG6.1 Symp. on Protocol Specification, Testing, and Verification, Twente, Holland, 1989."},{"key":"13_CR22","doi-asserted-by":"crossref","unstructured":"A. Pnueli. Applications of temporal logic to the specification and verification of reactive systems: A survey of corrent trends. In de Bakker, de Roever, and Rozenberg, editors, Current Trends in Concurrency, volume 224 of Lecture Notes in Computer Science, pages 510\u2013584. Springer Verlag, 1986.","DOI":"10.1007\/BFb0027047"},{"key":"13_CR23","unstructured":"A. P. Sistla. On verifying that a concurrent program satisfies a non-deterministic specification. Technical Report TR 88-378.01.1, Computer and Intelligent Systems Lab. GTE Laboratories, May 1988."},{"key":"13_CR24","unstructured":"E. W. Stark. Foundations of a Theory of Specification for Distributed Systems. PhD thesis, Massachusetts Inst. of Technology, 1984. Available as Report No. MIT\/LCS\/TR-342."},{"key":"13_CR25","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1016\/0304-3975(86)90007-1","volume":"56","author":"E. W. Stark","year":"1988","unstructured":"E. W. Stark. Proving entailment between conceptual state specifications. Theoretical Computer Science, 56:135\u2013154, 1988.","journal-title":"Theoretical Computer Science"},{"key":"13_CR26","unstructured":"M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proc. IEEE Symp. on Logic in Computer Science, pages 332\u2013344, June 1986."}],"container-title":["Lecture Notes in Computer Science","Stepwise Refinement of Distributed Systems Models, Formalisms, Correctness"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-52559-9_71.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,31]],"date-time":"2021-12-31T03:13:20Z","timestamp":1640920400000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-52559-9_71"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1990]]},"ISBN":["9783540525592","9783540470359"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/3-540-52559-9_71","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1990]]}}}