Abstract: Timed computing systems are systems in which desirable correctness or performance properties of the system depend on the timing of events, not just on the order of their occurrence. Many applications that involve timed systems have strong safety, reliability, and predictability requirements which makes it important to have methods for systematic design of systems and rigorous analysis of timing-dependent behavior.

The Timed Input/Output Automaton (TIOA) framework is a mathematical framework that supports description and analysis of timed systems. In this framework a system is represented as a timed I/O automaton, which is a kind of nondeterministic state machine. The state of a timed I/O automaton can change in two ways: instantaneously through discrete transitions or through continuous transformation over time, described by trajectories. The TIOA framework supports reasoning with multiple levels of abstraction using simulation relations. The framework also includes a composition operation that allows decomposition of modeling and verification tasks.

In this talk, I will introduce the TIOA framework, focusing on the basic definitions that are useful for describing timing-dependent behavior, and the verification methods that are most commonly used in practice. I will also give an overview of the TIOA Language, which is a high-level specification language based on timed I/O automata and the Tempo Toolset, which is a set of software tools that support simulation and verification of timed system designs.

This talk is based on joint work with Nancy Lynch (MIT), Frits Vaandrager (Radboud University Nijmegen), and Roberto Segala (University of Verona).

Dilsun Kaynar is a Postdoctoral Fellow at the Computer Science Department. Prior to joining Carnegie Mellon University, she was a Postdoctoral Research Associate at the MIT Computer Science and Artificial Intelligence Laboratory. She received the Ph.D. Degree from the University of Edinburgh, UK. Her research interests are in the areas of formal models for distributed computation, system design and program verification, security, and programming languages. Appointments: rosemary@cs.cmu.edu