Abstract
A version of the temporal logic I STL is used to demonstrate a two-stage approach to refinement of distributed programs. In each refinement, first convenient lower-level computations are shown to implement upper-level operations, and then in the second stage, all other computations are shown to be equivalent to one of the convenient ones. The equivalence maintains the ordering of all causally dependent events, but allows independent events to occur in different orders. The advantage of this separation is that different kinds of reasoning and induction can be used for the two aspects. The approach is demonstrated for a refinement that is part of the development of a cache consistency algorithm where synchrony is gradually loosened among the operations of different processes.
This research was supported by the Fund for the Promotion of Research in the Technion, 120-845.
Preview
Unable to display preview. Download preview PDF.
References
Y. Afek, G. Brown, and M. Merritt. Lazy caching. Transactions of Programming Languages, 15(1):182–206, 1993.
E.A. Emerson and J.Y. Halpern. Sometimes and not never revisited: on branching versus linear time temporal logic. Journal of the ACM, 33:151–178, 1986.
R. Gerth(editor). Verifying sequentially consistent memory. Technical report, Esprit React report, 1993.
W. Janssen and J. Zwiers. Specifying and proving communication closedness in protocols. In Proceedings 13th IFIP symp. on Protocol Specification, Testing and Verification, 1993.
S. Katz and D. Peled. Interleaving set temporal logic. Theoretical Computer Science, 75:263–287, 1990.
S. Katz and D. Peled. Defining conditional independence using collapses. Theoretical Computer Science, 101:337–359, 1992.
S. Katz and D. Peled. Verification of distributed programs using representative interleaving sequences. Distributed Computing, 6:107–120, 1992.
L. Lamport. The temporal logic of actions. ACM Transactions on Programming Languages and Systems. to appear.
M. Poel and J. Zwiers. Modular completeness for communication closed layers. In Proceedings CONCUR'93, 1993.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Katz, S. (1994). Global equivalence proofs for ISTL. In: Gabbay, D.M., Ohlbach, H.J. (eds) Temporal Logic. ICTL 1994. Lecture Notes in Computer Science, vol 827. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0013978
Download citation
DOI: https://doi.org/10.1007/BFb0013978
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58241-0
Online ISBN: 978-3-540-48585-8
eBook Packages: Springer Book Archive