Mechanical Translation of I/O Automaton Specifications into First-Order Logic
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.
KeywordsModel Checker Theorem Prover Proof Assistant Mechanical Translation Nondeterministic Choice
- 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.Marco Devillers. Translating I/O automata to PVS. Preliminary report, Computing Science Institute, University of Nijmengen, 1999.Google Scholar
- 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.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.David Gries. The Science of Programming. Springer-Verlag, 1981.Google Scholar
- 7.Chris Luhrs. Distributed spanning tree algorithms coded in IOA: Challenge problems for software analysis and synthesis methods. Technical Note, 2001.Google Scholar
- 8.Nancy A. Lynch. Distributed Algorithms. Morgan Kaufman Pubishers Inc., 1996.Google Scholar
- 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