On Verification of Refinements of Timed Distributed Algorithms
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.
Unable to display preview. Download preview PDF.
- 2.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.Google Scholar
- 4.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.Google Scholar
- 5.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.Google Scholar
- 6.Y. Gurevich. Evolving algebra 1993: Lipari guide. In E. Börger, editor, Specification and Validation Methods, pages 9–93. Oxford University Press, 1995.Google Scholar
- 9.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.Google Scholar