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 relations.

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:




Documentation

The following are the primary sources of information on the IOA Language and Toolset.
IOA Language
Simulation
Verification
Distributed Code Generation



Related Papers

More papers related to the project in addition to those listed above.



Example IOA Programs

Pointers to example IOA programs which have been used by group members to test various tools under development.



Software

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 contact ioa@theory.lcs.mit.edu if you have any questions on the software.



People

The list of people who are currently involved in the IOA project or who have worked on it recently.

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



Useful Links for Developers of the Toolkit




Last modified: 13 August 2003
Return to TDS