Abstract
This work is an attempt to apply Gurevich Abstract State Machines methodology to the verification of refinements of real-time distributed asynchronous algorithms. We define refinements following the semantical framework of observability, however, with respect to chosen pieces of the program. The time we consider is continuous as our motivation is related to systems of control that are usually specified within continuous time framework; the same framework is valid for discrete time. We remark that refinement of timed programs is not a simple replacement of a part of a program by making it more detailed. As an example to illustrate this we take Lamport’s Bakery Algorithm with real-time constraints. However, one of the key questions related to the verification of refinements is the preservation of verification proofs for the non refined initial algorithm as much as possible when verifying the refinement. This is the case for the notion of refinement we define. We introduce a notion of asynchronous timed distributed algorithm, define its semantics and discuss in what logic can be expressed its functioning. Then we introduce notions of refinement, and consider a refinement of interprocess communication of real-time Lamport’s Bakery algorithm using parallel message exchange. Such a refinement, contrary to our intuition, demands some non evident transformation of the initial algorithm to make it correct.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
M. Abadi and L. Lamport. The existence of refinement mappings. Technical Report29, DEC Systems Research Center, Palo Alto, California, August, 14 1988.
E. Börger, Y. Gurevich, and D. Rozenzweig. The bakery algorithm: Yet another specification and verification. In E. Börger, editor, Specification and Validation Methods, pages 231–243. Oxford University Press, 1995.
M. Broy. Compositional refinement of interactive systems. J. of the Assoc. Comput. Mach, 44(6):850–891, 1997.
D. Beauquier and A. Slissenko. A first order logic for specification of timed algorithms: Basic properties and a decidable class. 37 pages, 1999. To appear in J. of Pure and Applied Logic.
G. Goos, A. Heberle, W. Loewe, and W. Zimmermann. On modular definitions and implementations of programming languages. In Proc. of the Intern. Workshop on Abstract State Machines (ASM’2000), March 20-24, 2000, Switzerland, Monte Veritá, Ticino, pages 174–208. ETH, Zürich, 2000.
Y. Gurevich. Evolving algebra 1993: Lipari guide. In E. Börger, editor, Specification and Validation Methods, pages 9–93. Oxford University Press, 1995.
L. Lamport. A new solution of Dijkstra’s concurrent programming problem. Communications of ACM, 17(8):453–455, 1974.
J. Ostroff. Composition and refinement of discrete real-time systems. ACM Trans. on Software Engineering and Methodology, 8(1):1–48, 1999.
M. Wirsing. Algebraic specification. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science. Vol. B: Formal Models and Sematics, pages 677–788. Elsevier Science Publishers B.V., 1990.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cohen, J., Slissenko, A. (2000). On Verification of Refinements of Timed Distributed Algorithms. In: Gurevich, Y., Kutter, P.W., Odersky, M., Thiele, L. (eds) Abstract State Machines - Theory and Applications. ASM 2000. Lecture Notes in Computer Science, vol 1912. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44518-8_4
Download citation
DOI: https://doi.org/10.1007/3-540-44518-8_4
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67959-2
Online ISBN: 978-3-540-44518-0
eBook Packages: Springer Book Archive