Abstract
We propose a methodology for the specification and verification of distributed algorithms using Gurevich’s concept of Abstract State Machines. The methodology relies on a distinction between a higherlevel specification and a lower-level specification of an algorithm. The algorithm is characterized by an informal problem description. A justification assures the appropriateness of the higher-level specification for the problem description. A mathematical verification assures that the lower-level specification implements the higher-level one and is based on a refinement-relation. This methodology is demonstrated by a well-known distributed termination detection algorithm originally invented by Dijkstra, Feijen, and van Gasteren.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Martìn Abadi and Leslie Lamport. The existence of refinement mappings. Theoretical Computer Science, 82(2):253–284, May 1991.
Egon Börger, Yuri Gurevich, and Dean Rosenzweig. The bakery algorithm: Yet another specification and verification. In E. Bx00F6;rger, editor, Specification and Validation Methods, pages 231–243. Oxford University Press, 1995.
Egon Börger. High level system design and analysis using abstract state machines. In Hutter, Stephan, Traverso, and Ullman, editors, Current Trends in Applied Formal Methods (FM-Trends 98), LNCS. Springer, 1999. to appear.
Edsger W. Dijkstra, W.H.J. Feijen, and A.J.M. van Gasteren. Derivation of a termination detection algorithm for distributed computations. Information Processing Letters, 16(5):217–219, 1983.
Edsger W. Dijkstra. Shmuel Safra’s version of termination detection. In M. Broy and R. Steinbrüggen, editors, Proceedings of the NATO Advanced Study Institute on Calculational System Design, Marktoberdorf, Germany, 28 July-9 August 1998, pages 297–301, 1999.
Edsger W. Dijkstra and C.S. Scholten. Termination detection for diffusing computations. Information Processing Letters, 11(1):1–4, 1980.
Yuri Gurevich. Evolving algebras 1993: Lipari guide. In E. Börger, editor, Specification and Validation Methods, pages 9–36. Oxford University Press, 1995.
Yuri Gurevich. May 1997 draft of the ASM guide. Technical Report CSETR-336-97, University of Michigan, 1997.
Yuri Gurevich. The sequential ASM thesis. Bulletin of the European Association for Theoretical Computer Science, 67:93–124, February 1999. Columns: Logic in Computer Science.
Martin Kronenburg and Christian Peper. The FOREST Approach: World Wide Web page at http://rn.informatik.uni-kl.de/~forest/.
Leslie Lamport. On interprocess communication. Distributed Computing, 1:77–101, 1986.
Leslie Lamport. The temporal logic of actions. ACM Transactions on Programming Languages and Systems, 16(3):872–923, May 1994.
Christian Peper, Reinhard Gotzhein, and Martin Kronenburg. A generic approach to the formal specification of requirements. In 1st IEEE International Conference on Formal Engineering Methods 1997 (ICFEM’97), Hiroshima, Japan. IEEE Computer Society, 1997.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Eschbach, R. (1999). A termination detection algorithm: specification and verification. In: Wing, J.M., Woodcock, J., Davies, J. (eds) FM’99 — Formal Methods. FM 1999. Lecture Notes in Computer Science, vol 1709. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48118-4_41
Download citation
DOI: https://doi.org/10.1007/3-540-48118-4_41
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66588-5
Online ISBN: 978-3-540-48118-8
eBook Packages: Springer Book Archive