Abstract
By adding a new technique and a simple proof strategy to Abadi & Lamport's 1988 method [1] for proving refinement between specifications of distributed programs correct, the inherent limitation of their method, occurring when the abstract level of specification features so-called infinite invisible nondeterminism or internal discontinuity, can be sometimes overcome. This technique is applied to the cruel last step of a three step correctness proof for an algorithm for communication between migrating processes within a finite network due to Kleinman, Moscowitz, Pnueli & Shapiro [5].
Supported by ESPRIT BRA projects ’SPEC’ and ’REACT‘ (no. 6021)
Preview
Unable to display preview. Download preview PDF.
References
M. Abadi and L. Lamport. The existence of refinement mappings. In Proceedings 3rd Annual Symposium on Logic in Computer Science, pages 165–175, Edinburgh, 1988.
K. Engelhardt and W.-P. de Roever. Generalizing Abadi & Lamport's Method to Solve a Problem Posed by A. Pnueli. Technical report, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel, 1993.
B. Jonsson. Simulations between specifications of distributed systems. In J. C. M. Baeten and J. F. Groote, editors, Proceedings CONCUR '91, 2nd International Conference on Concurrency Theory, Amsterdam, The Netherlands, volume 527 of LNCS, pages 346–360. Springer, Aug. 1991.
A. Kleinmann, Y. Moscowitz, A. Pnueli, and E. Shapiro. Communication with directed logical variables. 48 pages, Oct. 1990.
A. Kleinmann, Y. Moscowitz, A. Pnueli, and E. Shapiro. Communication with directed logical variables. In Conference Record of the Eighteenth Annual ACM Symposium on Principles of Programming Languages, pages 221–232. ACM, Jan. 1991.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Engelhardt, K., de Roever, WP. (1993). Generalizing Abadi & Lamport's method to solve a problem posed by A. Pnueli. In: Woodcock, J.C.P., Larsen, P.G. (eds) FME '93: Industrial-Strength Formal Methods. FME 1993. Lecture Notes in Computer Science, vol 670. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0024653
Download citation
DOI: https://doi.org/10.1007/BFb0024653
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56662-5
Online ISBN: 978-3-540-47623-8
eBook Packages: Springer Book Archive