Logotype Mälardalen University

MRTC publications



Timed Automata as Task Models for Event-Driven Systems

Authors: Christer Norström, Anders Wall (former),
Source: In proceedings of RTCSA'99, IEEE Computer Society, Hong Kong
 

Abstract

In this paper, 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 arriving 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 and non-periodic. We show that the schedulability problem for the extended model can be transformed to 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 (e.g. safety and functionality) of the system. 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.
 

BibTeX entry

@inproceedings{Norström_0093:1999,
   author = {Christer Norstr{\"o}m and Anders Wall and },
   title = {Timed Automata as Task Models for Event-Driven Systems},
   booktitle = {In proceedings of RTCSA'99},
   month = {December},
   year = {1999},
   publisher = {IEEE Computer Society},
   url = {http://www.mrtc.mdh.se/index.php?choice=publications&id=0093},
}

  • Mälardalen University |
  • Box 883 |
  • 721 23 Västerås/Eskilstuna |
  • 021-101300, 016-153600 |
  • webmaster |
  • Latest update: 2010.02.23