We propose a new hybrid I/O automaton model that is capable of describing both continuous and discrete behavior. The model, which extends the timed I/O automaton model of Lynch et al and the phase transition system models of Manna et al, allows communication among components using both shared variables and shared actions. The main contributions of this paper are: (1) the definition of hybrid I/O automata and of an implementation relation based on hybrid traces, (2) the definition of a simulation between hybrid I/O automata and a proof that existence of a simulation implies the implementation relation, (3) a definition of composition of hybrid I/O automata and a proof that it respects the implementation relation, and (4) a definition of receptiveness for hybrid I/O automata and a proof that, assuming certain compatibility conditions, receptiveness is preserved by composition.

Software/Program Verification (acm D.2.4), Models of Computation (acm F.1.1), Specifying and Verifying and Reasoning about Programs (acm F.3.1)
Models of computation (Turing machines, etc.) (msc 68Q05), Specification and verification (program logics, model checking, etc.) (msc 68Q60), General (msc 93Axx), Control problems involving computers (process control, etc.) (msc 93C83)
CWI
Department of Computer Science [CS]

Lynch, N.A, Segala, R, Vaandrager, F.W, & Weinberg, H.B. (1995). Hybrid I/O automata. Department of Computer Science [CS]. CWI.