The standard introductory reference for I/O automata is the CWI paper by Lynch and Tuttle. All the details appear in Tuttle's M.S. thesis. A summary of the thesis appears in a 1987 PODC paper. A nice description of the model appears in Chapter 8 of Lynch's book, Distributed Algorithms.
The book Distributed Algorithms contains many algorithms and their proofs, all described in terms of I/O automata. I/O automata are used to model both shared memory and message-passing algorithms. The book Atomic Transactions contains algorithms for database concurrency control and abort recovery, again in terms of I/O automata. Other uses of I/O automata are sprinkled throughout the literature on distributed algorithms.
Last modified: February 26, 2002