J. Antonio Ramírez-Robredo. Paired Simulation of I/O Automata. Master of Engineering Thesis, Massachusetts Institute of Technology, Cambridge, MA, September 2000.

Abstract

An important principle that permeates theoretical work in distributed systems is that of successive refinement. This principle encourages the algorithm designer to start with a high-level description of the system, and to successively refine it down to lower-level implementations. For this purpose, it is common to relate two automata using a forward simulation relation, which is a mathematical relation between the states of the automata. Given the importance of this technique, it is desirable to have software tools to work with simulation relations.

In this thesis, I describe my design of a new simulator for the IOA language with the capability of simulating pairs of automata together, which are claimed to be related by a given simulation relation. This simulator is able to verify if the proposed simulation relation holds in a particular execution of the low-level automaton, given a step correspondence between the automata. The work to accomplish this goal included designing language extensions to IOA for specifying the step correspondence (in addition to the simulation relation) between the automata, as well as a new approach for resolving single-automaton nondeterminism.

I have provided documentation on the software implementation of the simulator and necessary support modules so that future work on the IOA toolkit (be it work on the simulator or on other tools) can be done using this software environment as a foundation.