Specifying and proving properties of timed I/O automata using Tempo

Timed I/O automata (TIOA) is a mathematical framework for modeling and verification of distributed systems that involve discrete and continuous dynamics. TIOA can be used for example, to model a real-time software component controlling a physical process. The TIOA model is sufficiently general to subsume other models in use for timed systems. The Tempo Toolset, currently under development, is aimed at supporting system development based on TIOA specifications. The Tempo Toolset is an extension of the IOA toolkit, which provides a specification simulator, a code generator, and both model checking and theorem proving support for analyzing specifications. This paper focuses on the modeling of timed systems and their properties with TIOA and on the use of TAME4TIOA, the TAME (Timed Automata Modeling Environment) based theorem proving support provided in Tempo, for proving system properties, including timing properties. Several examples are provided by way of illustration.