IOA Language and Toolset

Current research on IOA involves design and implementation of tools to support the development and analysis of IOA programs. These tools include analysis tools such as the simulator and interfaces to theorem-proving tools. They also include tools for generation of distributed code.

All the tools are based formally on I/O automata. Taken as a whole, the toolset is intended to help programmers to:

• Express designs at different levels of abstraction, starting with a high-level specification of the required behavior,
• Reason about properties of designs and about relationships between designs at different levels of abstraction,
• Produce documentation for the different stages of development,
• Produce code that is provably correct, subject to formally-stated assumptions about user-programmed data types and externally provided system services.

Documentation

IOA Language

• The paper Using I/O Automata for Developing Distributed Systems by Stephen Garland and Nancy Lynch gives an overview of the design of IOA and its toolset, together with an extended example of how they can be used.
• The IOA Reference Guide gives a full description of the formal syntax and semantics of IOA programs.

Simulation

• The Simulator Manual is the most recent document describing the design, implementation and use of the IOA Simulator.
• Simulating Nondeterministic Systems at Multiple Levels of Abstraction presents a case study that illustrates the use of the paired simulation capability of the IOA simulator in proving correct an algorithm for mutual exclusion.
• Antonio Ramirez' MEng thesis (2000) describes the design of the simulator, with the capability of simulating pairs of automata together, where one is claimed to implement the other.
• Some of the design ideas which appear in Antonio Ramirez's thesis first appeared in Anna Chefter's MEng thesis (1998) which describes a simulator for testing the behavior of IOA programs. This work does not address paired simulation.
• Laura Dean's MEng thesis (2001) describes enhancements to the simulator, including connections to the Daikon invariant discovery tool.
• Toh Ne Win, Michael Ernst and Gustavo Santos extended the connection between the IOA Toolkit and Daikon. Technical Report 841 presents their technique and some case studies.
• Ed Solovey's MEng thesis (2003) describes support for simulation of composite I/O automata.

Verification

• Using Simulated Execution in Verifying Distributed Algorithms describes a verification methodology for proving safety properties of distributed systems by using a combination of tools in our toolset (the IOA simulator, the dynamic program analysis tool Daikon and the theorem prover LP).
• Toh Ne Win's MEng thesis Theorem-Proving Distributed Algorithms with Dynamic Analysis gives a more detailed account of the methodology introduced in the paper listed above. It illustrates the methodology by means of three case studies and presents methods to generate proofs in Isabelle/HOL as well as the theorem prover LP.
• Andrej Bogdanov's MEng thesis describes his implementation of an IOA to LSL translator for use with the LP theorem prover.
• Stanislav Funiak's report describes the implementation of a tool to translate IOA to TLA+, the input language of the TLC model checker.

Distributed Code Generation

• Joshua A. Tauber's doctoral thesis describes the IOA-to-Java compiler for distributed algorithms. For those interested in the details of the implementation it is probably best read in conjunction with Michael Tsai's thesis.
• Michael Tsai's MEng thesis presents a framework of tools for compiling distributed algorithms written in the IOA language to Java code that runs on a network of workstations.
• Implementing Asynchronous Distributed Systems Using the IOA Toolkit (MIT CSAIL Technical Report MIT-LCS-TR-966) describes the experiments of Chryssis Georgiou, Panayiotis Mavrommatis, and Joshua A. Tauber on using the IOA checker, composer and code generator in implementing several distributed algorithms. These algorithms include the LCR algorithm for leader election in a ring network and the GHS algorithm for computing the minimum spanning tree in an arbitrary graph.

Related Papers

Example IOA Programs

Software

• The standard version. This contains all the published executable programs and some examples of applications written in IOA.
• The source version. This contains all of the above, along with source files and more examples. The Toolkit is written in Java.
• The extended tools version. This contains all of the above, plus extra compilation and verification tools commonly used with the IOA Toolkit, such as the Larch Prover and Java libraries.

People

Contact Dilsun Kirli Kaynar (dilsun@theory.lcs.mit.edu) for further information on the IOA project.

Useful Links for Developers of the Toolkit