IOA Language and Toolset
IOA is a formal language for describing computational processes that
are modeled using
I/O automata .
It is especially suitable for modeling distributed algorithms and
systems, and can do so at different levels of abstraction.
IOA can also be used for specifying properties that such processes,
algorithms, and systems are intended to satisfy.
In particular, it can be used to describe invariants and simulation
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
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.
The following are the primary sources of information on the IOA
Language and Toolset.
- IOA Language
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
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
- Ed Solovey's
MEng thesis (2003) describes support for simulation of composite
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.
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 to the project in addition to those listed above.
Example IOA Programs
example IOA programs which have been used by group members to
test various tools under development.
Copies of the IOA Toolkit are available in three editions. Please
read the README file and copyright notice before
downloading. The current version of the Toolkit is 0.10. This is
preliminary release is dated 13 August 2003.
Release notes will be available shortly.
Installation instructions can be found in the README file. Please
email@example.com if you
have any questions on the 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.
The list of people who are currently involved in the IOA project or who have worked on it recently.
Contact Dilsun Kirli Kaynar (firstname.lastname@example.org) for further
information on the IOA project.
Last modified: 13 August 2003
Return to TDS