Advertisement

Mechanical Translation of I/O Automaton Specifications into First-Order Logic

  • Andrej Bogdanov
  • Stephen J. Garland
  • Nancy A. Lynch
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2529)

Abstract

We describe a tool that improves the process of verifying relations between descriptions of a distributed algorithm at different levels of abstraction using interactive proof assistants. The tool automatically translates algorithms, written in the IOA language, into first-order logic, expressed in the Larch Shared Language, in a style that facilitates reasoning with a theorem prover. The translation uses a unified strategy to handle the various forms of nondeterminism that appear in abstract system descriptions. Applications of the tool to verify safety properties of three data management algorithms, including a substantial example based on Lamport’s logical time algorithm, suggest that the tool can be used to validate complicated, practical designs.

Keywords

Model Checker Theorem Prover Proof Assistant Mechanical Translation Nondeterministic Choice 
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

  1. 1.
    Andrej Bogdanov. Formal verification of simulations between I/O automata. Master of engineering thesis, Massachusetts Institute of Technology, 2001. http://theory.lcs.mit.edu/∼adib/thesis.
  2. 2.
    Marco Devillers. Translating I/O automata to PVS. Preliminary report, Computing Science Institute, University of Nijmengen, 1999.Google Scholar
  3. 3.
    Stephen J. Garland and Nancy A. Lynch. Using I/O automata for developing distributed systems. In Gary T. Leavens and Murali Sitaraman, editors, Foundations of Component-Based Systems, pages 285–312. Cambridge University Press, 2000.Google Scholar
  4. 4.
    Stephen J. Garland, Nancy A. Lynch, and Mandana Vaziri. IOA: a language for specifying, programming, and validating distributed systems. MIT Laboratory for Computer Science, 1997 (revised January, 2001).Google Scholar
  5. 5.
    David Gries. The Science of Programming. Springer-Verlag, 1981.Google Scholar
  6. 6.
    Leslie A. Lamport. Time, clocks and the ordering of events in a distributed system. Communications of the ACM, 21(7):558–565, July 1978.zbMATHCrossRefGoogle Scholar
  7. 7.
    Chris Luhrs. Distributed spanning tree algorithms coded in IOA: Challenge problems for software analysis and synthesis methods. Technical Note, 2001.Google Scholar
  8. 8.
    Nancy A. Lynch. Distributed Algorithms. Morgan Kaufman Pubishers Inc., 1996.Google Scholar
  9. 9.
    Nancy A. Lynch and Mark Tuttle. Hierarchical correctness proofs for distributed algorithms. Technical Report MIT/LCS/TR-387, MIT Laboratory for Computer Science, 1987.Google Scholar
  10. 10.
    Nancy A. Lynch and Frits Vaandrager. Forward and backward simulations-part I: Untimed systems. Information and Computation, 121(2):214–233, September 1995.zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Andrej Bogdanov
    • 1
  • Stephen J. Garland
    • 2
  • Nancy A. Lynch
    • 2
  1. 1.UC BerkeleyEECS - Computer Science DivisionBerkeley
  2. 2.MIT Laboratory for Computer ScienceCambridge

Personalised recommendations