Theorem-proving distributed algorithms with dynamic analysis

Theorem provers are notoriously hard to use because of the amount of human interaction they require, but they are important tools that can verify infinite state distributed systems. We present a method to make theorem-proving safety properties of distributed algorithms more productive by reducing human intervention. We model the algorithms as I/O automata, render the automata executable, and analyze the test executions with dynamic invariant detection. The human work in using a theorem prover is reduced because our technique provides two forms of assistance: lemmas generated by the dynamic invariant detection for use in the prover; and prover scripts, or tactics, generated from our experience with the I/O automaton model and the knowledge embedded in the test suite used for execution. We test our technique on three case studies: the Peterson 2-process mutual exclusion algorithm, a strong caching implementation of shared memory, and Lamport's Paxos algorithm for distributed consensus. In the development and implementation of our method, we also improved the tools for formal verification of 1/0 automata and for dynamic invariant detection. We describe a new model for specifying I/O automata in the Isabelle theorem prover's logic, and prove the soundness of a technique for verifying invariants in this model in the Isabelle prover. We develop methods for generating proofs of I/0 automata for two theorem provers, the Larch Prover and Isabelle/HOL. We show methods for executing I/O automata for testing, by allowing the execution of some automata defined with universal and existential quantifiers that were previously non-executable. Lastly, we present improvements to dynamic invariant detection in order to make it more scalable - in particular, we show how to achieve efficient incremental dynamic invariant detection, where the detection tool is only allowed to make one pass over its input executions.

Department dc:contributor.department

Massachusetts Institute of Technology. Dept. of Electrical Engineering and Computer Science.

Grantor dc:publisher

Massachusetts Institute of Technology

Year dc:date.issued

2003

Author dc:creator

• Ne Win, Toh, 1979-

Advisor dc:contributor.advisor

• Michael D. Ernst and Stephen J. Garland.

• Electrical Engineering and Computer Science.

Statement dc:rights

• M.I.T. theses are protected by copyright. They may be viewed from this source for any purpose, but reproduction or distribution in any format is prohibited without written permission. See provided URL for inquiries about permission.

Licence dc:rights.uri

• http://dspace.mit.edu/handle/1721.1/7582

Language dc:language.iso

eng

Handle dc:identifier.uri

http://hdl.handle.net/1721.1/29702

OAI identifier oai:identifier

oai:dspace.mit.edu:1721.1/29702