From the Specification to the Scheduling of Time-Dependent Systems

  • Christophe Lohr
  • Jean-Pierre Courtiat
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2469)


This paper introduces and formalizes a new variant of Timed Automata, called Time Labeled Scheduling Automata. A Time Labeled Scheduling Automaton is a single clock implementation model expressing globally the time constraints that a system has to meet. An algorithm is presented to show how a Time Labeled Scheduling Automaton can be synthesized from a minimal reachability graph derived from a high-level specification expressing the composition of different time constraints. It is shown how the reachability graph may be corrected before synthesizing the Time Labeled Scheduling Automaton to remove all its potentially inconsistent behaviors. Current applications of the model are the scheduling of interactive multimedia documents and a simple illustration is given in this area.


Process Algebra RT-Lotos Timed Automata Minimal Reachability Graph Temporal Consistency Time Labeled Scheduling Automata 


  1. 1.
    K. Altisen, G. Gossler, and J. Sifakis. A methodology for the construction of scheduled systems. In FTRTFT 2000, volume 1926 of Lecture Notes in Computer Science, pages 106–120, Pune, India, September 2000.Google Scholar
  2. 2.
    R. Alur, C. Courcoubetis, and N. Halbwachs. Minimization of timed transition systems. In CONCUR’92, volume 630 of Lecture Notes in Computer Science. Springer Verlag, 1992.CrossRefGoogle Scholar
  3. 3.
    R. Alur and D. Dill. The theory of timed automata. In REX Workshop “Real-Time: Theory in Practice”, volume 600 of Lecture Notes in Computer Science. Springer Verlag, 1991.Google Scholar
  4. 4.
    R. Alur, L. Fix, and T.A. Heizinger. Event-clock automata: A determinizable class of timed automata. In 6 th Annual Conference on Computeraided Verification, Lecture Notes in Computer Science 818, pages 1–13. Springer Verlag, 1994.Google Scholar
  5. 5.
    E. Asarin, O. Maler, and A. Pnueli. Symbolic controller synthesis for discrete and timed systems. In Hybrid Systems, pages 1–20, 1994.Google Scholar
  6. 6.
    B. Berthomieu and M. Diaz. Modeling and verification of time-dependent systems using time Petri nets. In IEEE Transactions on Software Engineering, volume 17. nℴ3, 1991.Google Scholar
  7. 7.
    J.P. Courtiat and R.C. R. de Oliveira. A reachability analysis of RT-Lotos specifications. In 8 th International Conference on Formal Description Techniques, Montreal, Canada, October 1995. Chapman&Hall.Google Scholar
  8. 8.
    J.P Courtiat, C.A.S. Santos, C. Lohr, and B. Outtaj. Experience with RT-Lotos, a temporal extension of the Lotos formal description technique. Computer Communications, 23:1104–1123, 2000.CrossRefGoogle Scholar
  9. 9.
    H. Dierks. Synthesising controllers from real-time specifications. In Tenth International Symposium on System Synthesis, pages 126–133. IEEE Computer Society, September 1997.Google Scholar
  10. 10.
    I. Kang and I. Lee. An efficient state space generation for analysis of real-time systems. In International Symposium on Software Testing and Analysis, pages 4–13, 1996.Google Scholar
  11. 11.
    X. Nicollin and J. Sifakis. An overview and synthesis on timed process algebras. In REX Workshop “Real-Time: Theory in Practice”, volume 600 of Lecture Notes in Computer Science. Springer Verlag, 1991.Google Scholar
  12. 12.
    A. Pnueli, E. Asarin, O. Maler, and J. Sifakis. Controller synthesis for timed automata. In System Structure and Control. Elsevier Science, 1998.Google Scholar
  13. 13.
    P.N.M. Sampaio and J.P. Courtiat. A formal approach for the presentation of interactive multimedia documents. In ACM Multimedia’2000, pages 435–438, Los Angeles, USA, October 2000.Google Scholar
  14. 14.
    P.N.M. Sampaio and J.P. Courtiat. Scheduling and presenting interactive multimedia documents. In International Conference on Multimedia and Exposition’2001, pages 1227–1227, Tokyo, Japan, August 2001.Google Scholar
  15. 15.
    P.N.M Sampaio, C. Lohr, and J.P. Courtiat. An integrated environment for the presentation of consistent SMIL 2.0 documents. In ACM Symposium on Document Engineering, Atlanta, Georgia, USA, November 2001.Google Scholar
  16. 16.
    C.A.S. Santos, P.N.M. Sampaio, and J.P. Courtiat. Revisiting the concept of hypermedia document consistency. In ACM Multimedia’99, Orlando, USA, November 1999.Google Scholar
  17. 17.
    P. Sénac, M. Diaz, A. Leger, and P. de Saqui-Sannes. Modelling logical and temporal synchronization in hypermedia systems. In IEEE Journal on Selected Areas in Communications, volume 14(1), pages 84–103, January 1996.Google Scholar
  18. 18.
    M. Yannakakis and D. Lee. An efficient algorithm for minimizing real-time transition systems. In CAV’93, volume 697 of Lecture Notes in Computer Science. Springer Verlag, 1993.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Christophe Lohr
    • 1
  • Jean-Pierre Courtiat
    • 1
  1. 1.LAAS - CNRSToulouseFrance

Personalised recommendations