The IOA Language and Toolset: Support for Designing, Analyzing, and Building Distributed Systems

Stephen J. Garland and Nancy A. Lynch

Technical Report MIT-LCS-TR-762, MIT Laboratory for Computer Science, Cambridge, Massachusetts, August 1998

This paper presents a new language for distributed programming, the IOA language, together with a design for a suite of tools, the IOA toolset, that support the production of high-quality distributed software. The language and tools are based on the I/O automaton model, which has been used extensively to describe and verify distributed algorithms. The toolset supports a development process that begins with a high-level specification, refines that specification via successively more detailed designs, and ends by automatically generating efficient distributed programs. The toolset encourages system decomposition, which helps make distributed programs understandable and easy to modify. Most importantly, it provides a variety of validation methods (theorem proving, model checking, and simulation), which can be used to ensure that the generated programs are correct, subject to stated assumptions about externally-provided system services (e.g., communication services).

Back to Publications of Stephen J. Garland