{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:02:52Z","timestamp":1725663772016},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540525592"},{"type":"electronic","value":"9783540470359"}],"license":[{"start":{"date-parts":[[1990,1,1]],"date-time":"1990-01-01T00:00:00Z","timestamp":631152000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1990]]},"DOI":"10.1007\/3-540-52559-9_87","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T21:37:31Z","timestamp":1330205851000},"page":"777-807","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Foundations of compositional program refinement"],"prefix":"10.1007","author":[{"given":"Rob","family":"Gerth","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,4]]},"reference":[{"key":"29_CR1","doi-asserted-by":"crossref","unstructured":"M. Abadi, L. Lamport (1988), \u201cThe Existence of Refinement Mappings\u201d, Proc. 3d IEEE Conf. on Logic in Computer Science (LICS), pp. 165\u2013175.","DOI":"10.1109\/LICS.1988.5115"},{"key":"29_CR2","doi-asserted-by":"crossref","unstructured":"M. Abadi, L. Lamport (1990), \u201cComposing Specifications\u201d, this volume.","DOI":"10.1007\/3-540-52559-9_59"},{"key":"29_CR3","unstructured":"B. Alpern, F.B. Schneider (1986), \u201cRecognizing Safety and Liveness\u201d, Technical Report TR86-727, Dept. of Computer Science, Cornell University."},{"key":"29_CR4","first-page":"389","volume":"197","author":"G. Berry","year":"1985","unstructured":"G. Berry, L. Cosserat (1985), The Synchronous Programming Language ESTEREL and its Mathematical Semantics, LNCS 197, pp. 389\u2013449, Springer Verlag.","journal-title":"LNCS"},{"issue":"7","key":"29_CR5","doi-asserted-by":"publisher","first-page":"560","DOI":"10.1145\/828.833","volume":"31","author":"S. Brookes","year":"1984","unstructured":"S. Brookes, C.A.R. Hoare, A. Roscoe (1984), A Theory of Communicating Sequential Processes, Journal of the ACM, Vol. 31, No. 7, pp. 560\u2013599.","journal-title":"Journal of the ACM"},{"key":"29_CR6","first-page":"109","volume":"60","author":"J. Bergstra","year":"1984","unstructured":"J. Bergstra, J.W. Klop (1984), Process Algebra for Synchronous Communication, Information and Computation, Vol. 60, pp. 109\u2013137.","journal-title":"Information and Computation"},{"key":"29_CR7","unstructured":"J. Bergstra, J.W. Klop, E.-R. Olderog (1986), \u201cFailure semantics with fair abstraction\u201d, Report CS-R8609, Center for Mathematics and Computer Science (CWI), Amsterdam."},{"key":"29_CR8","doi-asserted-by":"crossref","unstructured":"K.M. Chandy, J. Misra (1988), Parallel Program Design, Addison-Wesley.","DOI":"10.1007\/978-1-4613-9668-0_6"},{"key":"29_CR9","first-page":"47","volume":"137","author":"P. Darondeau","year":"1982","unstructured":"Ph. Darondeau (1982), \u201cAn Enlarged Definition and Complete Axiomatization of Observational Congruence of Finite Processes\u201d, LNCS 137, pp. 47\u201362, Springer Verlag.","journal-title":"LNCS"},{"key":"29_CR10","unstructured":"E.W. Dijkstra (1976), A Discipline of Programming, Prentice-Hall."},{"key":"29_CR11","unstructured":"S. Eilenberg (1974), Automata, Languages and Machines, Volume A, Academic Press."},{"key":"29_CR12","doi-asserted-by":"crossref","unstructured":"A. Fekete, N. Lynch, L. Shrira (1987), \u201cA Modular Proof of Correctness for a Network Synchronizer\u201d, Proc. 2nd International Workshop on Distributed Algorithms, LNCS 312, Springer Verlag.","DOI":"10.1007\/BFb0019807"},{"key":"29_CR13","first-page":"95","volume":"267","author":"R. Gerth","year":"1987","unstructured":"R. Gerth, A. Boucher (1987), \u201cA Timed Failures Model for Extended Communicating Processes\u201d, Proc. 14th ICALP, LNCS 267, pp. 95\u2013115, Springer Verlag.","journal-title":"LNCS"},{"key":"29_CR14","doi-asserted-by":"crossref","unstructured":"R. Gerth, A. Pnueli (1989), \u201cRooting UNITY\u201d, Proc. 5th IEEE International Workshop on Software Specification and Design, pp. 11\u201319.","DOI":"10.1145\/75199.75202"},{"key":"29_CR15","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1090\/psapm\/019\/0235771","volume":"19","author":"R. Floyd","year":"1967","unstructured":"R. Floyd (1967), \u201cAssigning Meaning to Programs\u201d, Proc. Sympos. in Appl. Math. 19, pp. 19\u201332, American Mathematical Society.","journal-title":"Proc. Sympos. in Appl. Math."},{"key":"29_CR16","doi-asserted-by":"crossref","unstructured":"D. Harel (1987), Statecharts: a visual approach to complex systems, Science of Computer Programming, Vol. 8, No. 3.","DOI":"10.1016\/0167-6423(87)90035-9"},{"key":"29_CR17","unstructured":"M. Hennesy (1988), Algebraic Theory of Processes, The MIT press."},{"key":"29_CR18","doi-asserted-by":"crossref","unstructured":"C.A.R. Hoare (1985), Communicating Sequential Processes, Prentice-Hall.","DOI":"10.1007\/978-3-642-82921-5_4"},{"key":"29_CR19","unstructured":"F. Jahanian, A. Mok (1988), Modecharts: a specification language for real-time systems, IEEE Transactions on Software Engineering, to appear."},{"key":"29_CR20","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1145\/69624.357207","volume":"5","author":"L. Lamport","year":"1983","unstructured":"L. Lamport (1983), Specifying concurrent program modules, ACM Transactions on Programming Languages and Systems, Vol. 5, No. 2, pp. 190\u2013222.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"29_CR21","unstructured":"L. Lamport (1986), \u201cSpecification Simplified\u201d, Technical Report, DEC Systems Research Center, Alamaden."},{"key":"29_CR22","doi-asserted-by":"crossref","unstructured":"N. Lynch (1990), \u201cMultivalued Possibilities Mappings\u201d, this volume.","DOI":"10.21236\/ADA226110"},{"issue":"4","key":"29_CR23","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1109\/TSE.1984.5010246","volume":"10","author":"S.S. Lam","year":"1984","unstructured":"S.S. Lam, A.U. Shankar (1984), Protocol verification via projection, IEEE Transactions on Software Engineering, Vol. 10, No. 4, pp. 325\u2013342.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"29_CR24","doi-asserted-by":"crossref","unstructured":"N. Lynch, M. Tuttle (1987), \u201cHierarchical correctness proofs for distributed algorithms\u201d, Proc. 6th ACM Sympos. Principles of Distributed Computing (PODC), pp. 137\u2013151, ACM.","DOI":"10.1145\/41840.41852"},{"key":"29_CR25","doi-asserted-by":"crossref","unstructured":"M. Merrit (1990), \u201cCompleteness Theorems for Automata\u201d, this volume.","DOI":"10.1007\/3-540-52559-9_78"},{"key":"29_CR26","unstructured":"R. Milner (1971), \u201cAn algebraic definition of simulation between programs\u201d, Proc. 2nd Joint Confer. on Artificial Intelligence, BCS, pp. 481\u2013489."},{"key":"29_CR27","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-10235-3","volume-title":"A Calculus of Communicating Systems","author":"R. Milner","year":"1980","unstructured":"R. Milner (1980), A Calculus of Communicating Systems, LNCS 94, Springer-Verlag, New York."},{"key":"29_CR28","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/0304-3975(83)90114-7","volume":"25","author":"R. Milner","year":"1983","unstructured":"R. Milner (1983), Calculi for Synchrony and Asynchrony, Theoretical Computer Science, Vol. 25, pp. 267\u2013310.","journal-title":"Theoretical Computer Science"},{"key":"29_CR29","unstructured":"R. Milner (1989), Communication and Concurrency, Prentice Hall."},{"key":"29_CR30","doi-asserted-by":"crossref","unstructured":"Z. Manna, A. Pnueli (1981), \u201cVerification of Concurrent Programs: The Temporal Framework\u201d, The Correctness Problem in Computer Science (R. S. Boyer, J. S. Moore, eds.), pp. 215\u2013274, Academic Press.","DOI":"10.21236\/ADA106750"},{"key":"29_CR31","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, A. Pnueli (1984), Adequate Proof Principles for Invariance and Liveness Properties of Concurrent Programs, Science of Computer Programming, Vol. 4, pp. 257\u2013289.","journal-title":"Science of Computer Programming"},{"key":"29_CR32","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/BF00264365","volume":"24","author":"R. Nicola De","year":"1987","unstructured":"R. De Nicola (1987), Extensional Equivalences for Transition Systems, Acta Informatica, Vol. 24, pp. 211\u2013237.","journal-title":"Acta Informatica"},{"key":"29_CR33","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1016\/0304-3975(84)90113-0","volume":"34","author":"R. Nicola De","year":"1984","unstructured":"R. De Nicola, M. Hennessy (1984), Testing Equivalences for Processes, Theoretical Computer Science, Vol. 34, pp. 83\u2013133.","journal-title":"Theoretical Computer Science"},{"key":"29_CR34","unstructured":"F. Stomp, W.P. de Roever (1987), \u201cA correctness proof of a distributed minimum-weight spanning tree algorithm\u201d, Proc. 7th IEEE International Conference on Distributed Computer Systems (ICDCS), pp. 440\u2013448."},{"key":"29_CR35","unstructured":"F. Stomp (1989), Design and Verification of Distributed Network Algorithms: Foundations and Applications, Ph.D. thesis, Eindhoven University of Technology."},{"key":"29_CR36","doi-asserted-by":"crossref","unstructured":"J. Welch, L. Lamport, N. Lynch (1988), \u201cA lattice-structured proof of a minimum spanning tree algorithm\u201d, Proc. ACM Symposium on Principles of Distributed Computing (PODC).","DOI":"10.21236\/ADA198312"}],"container-title":["Lecture Notes in Computer Science","Stepwise Refinement of Distributed Systems Models, Formalisms, Correctness"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-52559-9_87","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,31]],"date-time":"2021-12-31T03:13:51Z","timestamp":1640920431000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-52559-9_87"}},"subtitle":["Safety properties"],"short-title":[],"issued":{"date-parts":[[1990]]},"ISBN":["9783540525592","9783540470359"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/3-540-52559-9_87","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1990]]},"assertion":[{"value":"4 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}