Abstract
Within verification of distributed Abstract State Machines one often has to prove properties related to the state transition level induced by partially ordered runs. This paper shows how such a transition level in form of a transition graph may be constructed. In this way the verification can be carried out directly on the transition graph. The construction itself is given as a sequential non-deterministic ASM.
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.
References
Egon Börger, Yuri Gurevich, and Dean Rosenzweig. The bakery algorithm: Yet another specification and verification. In E. Börger, editor, Specification and Validation Methods, pages 231–243. Oxford University Press, 1995.
Robert Eschbach, Uwe Glässer, Reinhard Gotzhein, and Andreas Prinz. On the Formal Semantics of SDL-2000: A Compilation Approach Based on an Abstract SDL Machine. In Y. Gurevich, P.W. Kutter, M. Odersky, and L. Thiele, editors, Abstract State Machines-Theory and Applications, number 1912 in LNCS. Springer, 2000.
Robert Eschbach. A termination detection algorithm: Specification and verification. In Jeanette M. Wing, Jim Woodcock, and Jim Davies, editors, Proc. of FM’99-World Congress on Formal Methods in the Development of Computing Systems, number 1709 in LNCS, pages 1720–1737, 1999.
Yuri Gurevich and James K. Huggins. The semantics of the c programming language. In Selected papers fromCSL’92 (Computer Science Logic), LNCS, pages 274–308. Springer, 1993.
Yuri Gurevich and Dean Rosenzweig. Partially ordered runs: A case study. In Yuri Gurevich, Philipp W. Kutter, Martin Odersky, and Lothar Thiele, editors, Abstract State Machines: Theory and Applications, Proc. of International Workshop, ASM2000, Monte Verità , Switzerland, number 1912 in LNCS, pages 131–150. Springer, March 2000.
Yuri Gurevich. Evolving Algebras 1993: Lipari Guide. In E. Börger, editor, Specification and Validation Methods. Oxford Univ. Press, 1995.
Yuri Gurevich. May 1997 draft of the ASM guide. Technical Report CSE-TR-336-97, University of Michigan, 1997.
Yuri Gurevich. Sequential abstract state machines capture sequential algorithms. ACM Transactions on Computational Logic, 1(1):77–111, July 2000.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Eschbach, R. (2001). A Verification Approach for Distributed Abstract State Machines. In: Bjørner, D., Broy, M., Zamulin, A.V. (eds) Perspectives of System Informatics. PSI 2001. Lecture Notes in Computer Science, vol 2244. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45575-2_12
Download citation
DOI: https://doi.org/10.1007/3-540-45575-2_12
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43075-9
Online ISBN: 978-3-540-45575-2
eBook Packages: Springer Book Archive