Distributed and parallel computer systems are becoming increasingly common and complicated. New applications such as computer-supported cooperative work systems are appearing on these platforms, and parallel scientific and engineering computations have long used parallelism for high performance. Many of these systems have important correctness, performance, and fault-tolerance requirements. However, they often use intertwined and complicated protocols that make them difficult to build and reason about. This project studies structured approaches to managing this complexity, which view the system at different levels of abstraction and as parallel compositions of interacting components. The particular approach used to do this is the I/O automaton model, which has previously been used to describe and verify distributed algorithms and distributed system designs. The model has a simple notion of external behavior based on linear traces of external actions of the components, and allows the components (automata) to be composed and related using simulation relations. The new research here will develop parts of the IOA programming language and toolset to support distributed and parallel programming using I/O automata. Extensions for timed and hybrid I/O automata will also be attempted. The new tools and techniques will allow a variety of systems to be modeled and analyzed at a high level of abstraction.
