Advertisement

On Verification of Refinements of Timed Distributed Algorithms

  • J. Cohen
  • A. Slissenko
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1912)

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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    M. Abadi and L. Lamport. The existence of refinement mappings. Technical Report29, DEC Systems Research Center, Palo Alto, California, August, 14 1988.MATHGoogle Scholar
  2. 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
  3. 3.
    M. Broy. Compositional refinement of interactive systems. J. of the Assoc. Comput. Mach, 44(6):850–891, 1997.MathSciNetCrossRefMATHGoogle Scholar
  4. 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. 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. 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
  7. 7.
    L. Lamport. A new solution of Dijkstra’s concurrent programming problem. Communications of ACM, 17(8):453–455, 1974.MathSciNetCrossRefMATHGoogle Scholar
  8. 8.
    J. Ostroff. Composition and refinement of discrete real-time systems. ACM Trans. on Software Engineering and Methodology, 8(1):1–48, 1999.CrossRefGoogle Scholar
  9. 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

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • J. Cohen
    • 1
  • A. Slissenko
    • 1
    • 2
  1. 1.Dept. of InformaticsUniversityParis-12CréteilFrance
  2. 2.St. Petersburg Institute for Informatics and Automation of Russian Academy of SciencesSt. PetersburgItaly

Personalised recommendations