Timed automata as task models for event-driven systems

We extend the classic model of timed automata with a notion of real-time tasks. The main idea is to associate each discrete transition in a timed automaton with a task (an executable program). Intuitively, a discrete transition in an extended timed automaton denotes an event releasing a task and the guard on the transition specifies all the possible arrival times of the event (instead of the so-called minimal inter-arrival time). This yields a general model for hard real-time systems in which tasks may be periodic or non-periodic. We show that the schedulability problem for the extended model can be transformed into a reachability problem for standard timed automata, and thus it is decidable. This allows us to apply model-checking tools for timed automata to schedulability analysis for event-driven systems. In addition, based on the same model of a system, we may use the tools to verify other properties of the system (e.g. safety and functionality). This unifies schedulability analysis and formal verification in one framework. We present an example where the model-checker UPPAAL is applied to check the schedulability and safety properties of a control program for a turning lathe