Technical Report Number
We present the Spectrum Simulation System, a new research tool for the design and study of distributed algorithms. Based on the formal Input/Output Automation model of Lynch and Tuttle, Spectrum allows one to express distributed algorithms as collections of I/O automata and simulate them directly in terms of the semantics of that model. This permits integration of algorithm specification, design, debugging, analysis, and proof of correctness within a single formal framework that is natural for describing distributed algorithms. Spectrum provides a language for expressing algorithms as I/O automata, a simulator for generating algorithm executions, and a graphics interface for constructing systems of automata and observing their executions. We show that the properties of the I/O automation model provide a solid foundation for algorithm development tools. For example, using I/O automation composition, Spectrum users may define composed types hierarchically, study simulations at varying levels of detail, and create specialized debugging and analysis devices. These devices, called spectators, are written in the Spectrum language just as any other system component, and can monitor algorithm executions for correctness and performance without interfering with the algorithm. The system is designed to support experimentation with algorithm. For example, the system separates algorithms from the system configurations in which they are to run, allowing users to vary them independently. Also the message system may be modeled explicitly as as automation, permitting users to study algorithms under different communications assumptions simply by substituting one automation for another.
Goldman, Kenneth J., "The Spectrum Simulation System: A Formal Approach to Distributed Algorithm Development Tools" Report Number: WUCS-91-42 (1991). All Computer Science and Engineering Research.