{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T11:02:26Z","timestamp":1753182146800,"version":"3.32.0"},"reference-count":11,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[1995,9,1]],"date-time":"1995-09-01T00:00:00Z","timestamp":809913600000},"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":["Form. Asp. Comput."],"published-print":{"date-parts":[[1995,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Our own basic intuitions are presented when introducing the method developed by Abadi and Lamport in [AbL88a] for proving refinement between specifications of nondeterministic programs correct to people unacquainted with it. The example we use to illustrate this method is a nontrivial communication protocol that provides a mechanism analogous to message passing between migrating processes within a fixed finite network of nodes due to Kleinman, Moscowitz, Pnueli and Shapiro [KMP91]. Especially the cruel last step of a three step refinement proof of that protocol gives rise to a deeper understanding of, and some small enhancements to, Abadi and Lamport's 1988 method.<\/jats:p>","DOI":"10.1007\/bf01211632","type":"journal-article","created":{"date-parts":[[2005,2,25]],"date-time":"2005-02-25T13:02:46Z","timestamp":1109336566000},"page":"550-575","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Towards a practitioners' approach to Abadi and Lamport's method"],"prefix":"10.1145","volume":"7","author":[{"given":"Kai","family":"Engelhardt","sequence":"first","affiliation":[{"name":"Institut f\u00fcr Informatik, Christian-Albrechts-Universit\u00e4t zu Kiel, Preu\u00dferstr. 1\u20139, 24105, Kiel, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Willem -Paul","family":"de Roever","sequence":"additional","affiliation":[{"name":"Institut f\u00fcr Informatik, Christian-Albrechts-Universit\u00e4t zu Kiel, Preu\u00dferstr. 1\u20139, 24105, Kiel, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"volume-title":"Technical Report 29","year":"1988","author":"Abadi M.","key":"e_1_2_1_2_1_2"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Abadi M. and Lamport L.: The existence of refinement mappings. In Proceedings 3rd Annual Symposium on Logic in Computer Science pages 165\u2013175 Edinburgh 1988.","DOI":"10.1109\/LICS.1988.5115"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(85)90056-0"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Coenen J. Zwiers J. and de Roever W.-P.: Assertional data reification proofs: Survey and perspective. In J.M. Morris and R.C. Shaw editors Proceedings of the 4th Refinement Workshop Workshops in Computing pages 91\u2013114. Springer Verlag 1991.","DOI":"10.1007\/978-1-4471-3756-6_5"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Engelhardt K. and de Roever W.-R: Generalizing Abadi and Lamport's method to solve a problem posed by A. Pnueli. In J.C.R Woodcock and RG. Larsen editors FME '93: Industrial-Strength Formal Methods volume 670 of LNCS pages 294\u2013313. Springer-Verlag April 1993.","DOI":"10.1007\/BFb0024653"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(87)90224-9"},{"key":"e_1_2_1_2_7_2","unstructured":"Jonsson B.: Simulations between specifications of distributed systems. In Jos C. M. Baeten and Jan Frisco Groote editors Proceedings CONCUR '91 2nd International Conference on Concurrency Theory Amsterdam The Netherlands volume 527 of LNCS pages 346\u2013360. Springer August 1991."},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Kleinmann A. Moscowitz Y. Pnueli A. and Shapiro E.: Communication with directed logic variables. 48 pages unpublished October 1990.","DOI":"10.1145\/99583.99615"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Kleinmann A. Moscowitz Y. Pnueli A. and Shapiro E.: Communication with directed logic variables. In Conference Record of the Eighteenth Annual ACM Symposium on Principles of Programming Languages pages 221\u2013232. ACM January 1991.","DOI":"10.1145\/99583.99615"},{"key":"e_1_2_1_2_10_2","unstructured":"Lamport L.: TLA message 10. TLA mailinglist June 1990. Contact email: Iamport@src.dec.com."},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Manna Z. and Pnueli A.: The Temporal Logic of Reactive and Concurrent Systems volume Specification. Springer-Verlag 1992.","DOI":"10.1007\/978-1-4612-0931-7"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01211632.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01211632\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/BF01211632","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,23]],"date-time":"2024-12-23T22:22:40Z","timestamp":1734992560000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/BF01211632"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,9]]},"references-count":11,"journal-issue":{"issue":"5","published-print":{"date-parts":[[1995,9]]}},"alternative-id":["10.1007\/BF01211632"],"URL":"https:\/\/doi.org\/10.1007\/bf01211632","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[1995,9]]}}}