The IOA Language and Toolset:
    Support for Mathematics-Based Distributed Programming

                 Nancy Lynch
                    MIT

This talk presents a new language for distributed programming, the IOA
language, together with a design for a suite of tools, the IOA toolset, to
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 is
intended to produce efficient, running distributed programs whose
correctness has been fully proved, subject to stated assumptions about
externally-provided system services (e.g., communication services).  The
toolset encourages system decomposition, which helps to make distributed
programs understandable and easy to modify.

The designer of a distributed system or algorithm is supposed to develop and
validate his/her design entirely within the IOA framework.  The final
result---an IOA program---is translated automatically into code in an
existing programming language such as C++ or Java.  (This translation uses
hand-coded implementations of operations on the data types.)  Before the
final translation step, the design is subject to a range of validation
methods, including complete proof using an interactive theorem-proving
program, and partial validation using a model-checker and a simulator.  Our
tools assist the programmer in decomposing the design into separable
interacting components, based on I/O automaton composition, and in refining
it using levels of abstraction, based on trace inclusion and forward and
backward simulation relations.

Joint work with Stephen Garland