1. Introduction
This paper describes the Timed Input/Output Automata (TIOA) framework, a general mathematical framework for modeling and analyzing real-time systems. Designers of real-time systems can use this framework to describe complex systems and decompose them into manageable pieces. In particular, they can use TIOA to describe their systems at multiple levels of abstraction, and to decompose their systems into more primitive, interacting components. Designers can use TIOA to prove safety, liveness, and performance properties of real-time systems. Since TIOA is purely mathematical, such proofs are generally done by hand. However, TIOA is a natural basis for computer support tools, which will be developed in the future. The TIOA framework is general enough to express previous results from other frameworks, such as [24], [23], [5], [22], [21], [29].