Modeling Real-Time Systems using Rate Automata

  • Jennifer McManis
  • Pravin Varaiya
Conference paper
Part of the The IMA Volumes in Mathematics and its Applications book series (IMA, volume 73)


Recently, real-time system models have been proposed which fall into the general category of timed automata. A timed automaton consists of a discrete event component represented as a finite automaton, coupled with a temporal component represented as a finite collection of clocks marking time between event occurrences. For timed automata it is possible to reduce certain verification problems to those of checking language containment or language emptiness. We extend this model to allow the clocks to rim at rates other than one. The extension is well suited to the analysis of scheduling problems, find we demonstrate this by the modeling a simple scheduling policy. We give conditions for reduction of the rate automaton to a finite state automaton.


Schedule Policy Time Region Task Type Hybrid Automaton Finite State Automaton 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    R. Alur, C. Courcoubetis, AND D. Dill, Model-checking for real-time systems, in IEEE Proceedings of the Fifth Annual Symposium on Logic and Computer Science, 1990.Google Scholar
  2. [2]
    R. Alur, C. Courcoubetis, T. Henzinger, AND P. Ho, Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems (preprint ) 1993.Google Scholar
  3. [3]
    R. Alur AND D. Dill, Automata for modeling real-time systems, in Proceedings of the 17th Annual Colloquium on Automata, Languages, and Programming, 1990.Google Scholar
  4. [4]
    S. Baruah, A. Mok, AND L. Rosier, Preemptively scheduling hard-real-time sporadic tasks on one processor, Real-Time Systems Symposium, 1990.Google Scholar
  5. [5]
    M. Dertouzos, Control robotics; the procedural control of physical processes, in Proceedings of the IFIP Congress, 1974.Google Scholar
  6. [6]
    D. Dill, Timing assumptions and verification of finite-state concurrent systems, in Automatic Verification Methods for Finite State Systems, Lecture Notes in Computer Science, no. 407 Springer-Verlag 1989.Google Scholar
  7. [7]
    A. Fawaz, P. Varaiya, AND J. Walrand, Analysis of interrupt handling schemes in real-time systems, in Proceedings of the International Phoenix Conference on Computers and Communication, 1989, pp. 260–263.CrossRefGoogle Scholar
  8. [8]
    K. Jeffay, D. Stanat, AND C. Martel, On non-preemptive scheduling of periodic and sporadic tasks, Real-Time Systems Symposium, 1991.Google Scholar
  9. [9]
    Y. Kelly, A. Pnueli, J. Sifakis, AND S.Yovine, Integration graphs: a class of decidable hybrid systems, (preprint) 1993.Google Scholar
  10. [10]
    J. McManis, Control of Real-Time Discrete Events Dynamical Systems, ( PhD thesis) University of California, Berkeley 1993.Google Scholar
  11. [11]
    F. Modugno, M. Merritt, AND M. Tuttle, Time constrained automata, in CONCUR’91 Proceedings, Workshop on Theories of Concurrency: Unification and Extension, LNCS 527, Springer-Verlag, August 1991, pp. 408 – 423.Google Scholar
  12. [12]
    S. Narain, Proving temporal properties about hybrid systems, RAND Corporation, 1990.Google Scholar
  13. [13]
    X. Nicollin, A. Olivero, J. Sifakis, AND S. Yovine, An approach to the description and analysis of hybrid systems, in Proceedings of the Workshop on Theory of Hybrid Systems, Lyngby, Denmark, Lecture Notes in Computer Science, Springer-Verlag 1992.Google Scholar
  14. [14]
    X. Nicollin, J. Sifakis, AND S. Yovine, From atp to timed graphs and hybrid systems, in Real Time: Theory in Practice, (J. W. de Bakker, K. Huising, W.-P. de Roever, AND G. Rozenberg, editors) Lecture Notes in Computer Science, Springer-Verlag, 1992.Google Scholar
  15. [15]
    J. Ostroff, Temporal Logic for Real-Time Systems, Research Studies Press Ltd. 1989.Google Scholar
  16. [16]
    B. Sprunt, L. Sha, AND J. Lehoczky, A periodic task scheduling for hard-real-time systems, in The Journal of Real-Time Systems, 1989.Google Scholar

Copyright information

© Springer-Verlag New York, Inc 1995

Authors and Affiliations

  • Jennifer McManis
  • Pravin Varaiya

There are no affiliations available

Personalised recommendations