Implementation of Timed Automata: An Issue of Semantics or Modeling?

  • Karine Altisen
  • Stavros Tripakis
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3829)


We examine to what extent implementation of timed automata can be achieved using the standard semantics and appropriate modeling, instead of introducing new semantics. We propose an implementation methodology which allows to transform a timed automaton into a program and to check whether the execution of this program on a given platform satisfies a desired property. This is done by modeling the program and the execution platform, respectively, as an untimed automaton and a collection of timed automata. We also study the problem of property preservation, in particular when moving to a “better” execution platform. We show that some subtleties arise regarding the definition of “better”, in particular for digital clocks. The fundamental issue is that faster clocks result in better “sampling” and therefore can introduce more behaviors.


Execution Model Discrete Transition Input Event Outgoing Transition Time 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.
    Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science 126, 183–235 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    Alur, R., Henzinger, T., Kupferman, O., Vardi, M.: Alternating refinement relations. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 163–178. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  3. 3.
    Alur, R., Ivancic, F., Kim, J., Lee, I., Sokolsky, O.: Generating embedded software from hierarchical hybrid models. In: Languages, Compilers, and Tools for Embedded Systems (LCTES 2003). ACM, New York (2003)Google Scholar
  4. 4.
    Amnell, T., Fersman, E., Pettersson, P., Yi, W., Sun, H.: Code synthesis for timed automata. Nordic J. of Computing 9(4), 269–300 (2002)zbMATHMathSciNetGoogle Scholar
  5. 5.
    Caspi, P., Curic, A., Maignan, A., Sofronis, C., Tripakis, S.: Translating discrete-time Simulink to Lustre. In: Alur, R., Lee, I. (eds.) EMSOFT 2003. LNCS, vol. 2855, pp. 84–99. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  6. 6.
    Caspi, P., Curic, A., Maignan, A., Sofronis, C., Tripakis, S., Niebert, P.: From Simulink to SCADE/Lustre to TTA: a layered approach for distributed embedded applications. In: Languages, Compilers, and Tools for Embedded Systems (LCTES 2003). ACM, New York (2003)Google Scholar
  7. 7.
    Daws, C., Olivero, A., Tripakis, S., Yovine, S.: The tool Kronos. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995. LNCS, vol. 1066, pp. 208–219. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  8. 8.
    de Alfaro, L., Henzinger, T.A.: Interface automata. In: Foundations of Software Engineering (FSE). ACM Press, New York (2001)Google Scholar
  9. 9.
    Halbwachs, N.: Synchronous Programming of Reactive Systems. Kluwer, Dordrecht (1992)Google Scholar
  10. 10.
    Henzinger, T., Horowitz, B., Kirsch, C.: Giotto: A time-triggered language for embedded programming. In: Henzinger, T.A., Kirsch, C.M. (eds.) EMSOFT 2001. LNCS, vol. 2211, p. 166. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  11. 11.
    Henzinger, T., Manna, Z., Pnueli, A.: What good are digital clocks? In: Kuich, W. (ed.) ICALP 1992. LNCS, vol. 623. Springer, Heidelberg (1992)Google Scholar
  12. 12.
    Kopetz, H.: Real-Time Systems Design Principles for Distributed Embedded Applications. Kluwer, Dordrecht (1997)zbMATHGoogle Scholar
  13. 13.
    Krčál, P., Mokrushin, L., Thiagarajan, P.S., Yi, W.: Timed vs. Time-triggered automata. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 340–354. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  14. 14.
    Larsen, K., Petterson, P., Yi, W.: Uppaal in a nutshell. Software Tools for Technology Transfer 1(1/2) (October 1997)Google Scholar
  15. 15.
    Ouaknine, J., Worrell, J.: Revisiting digitization, robustness, and decidability for timed automata. In: LICS 2003. IEEE CS Press, Los Alamitos (2003)Google Scholar
  16. 16.
    Puri, A.: Dynamical properties of timed automata. Discrete Event Dynamic Systems 10(1-2), 87–113 (2000)zbMATHCrossRefMathSciNetGoogle Scholar
  17. 17.
    Scaife, N., Caspi, P.: Integrating model-based design and preemptive scheduling in mixed time- and event-triggered systems. In: Euromicro conference on Real-Time Systems (ECRTS 2004) (2004)Google Scholar
  18. 18.
    Scaife, N., Sofronis, C., Caspi, P., Tripakis, S., Maraninchi, F.: Defining and translating a “safe” subset of Simulink/Stateflow into Lustre. In: 4th ACM International Conference on Embedded Software (EMSOFT 2004) (2004)Google Scholar
  19. 19.
    Tripakis, S., Sofronis, C., Scaife, N., Caspi, P.: Semantics-preserving and memory-efficient implementation of inter-task communication under static-priority or EDF schedulers. In: 5th ACM Intl. Conf. on Embedded Software (EMSOFT 2005) (2005)Google Scholar
  20. 20.
    Tripakis, S., Yovine, S.: Analysis of timed systems using time-abstracting bisimulations. Formal Methods in System Design 18(1), 25–68 (2001)zbMATHCrossRefGoogle Scholar
  21. 21.
    De Wulf, M., Doyen, L., Raskin, J.-F.: Almost ASAP semantics: From timed models to timed implementations. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 296–310. Springer, Heidelberg (2004)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Karine Altisen
    • 1
  • Stavros Tripakis
    • 1
  1. 1.Verimag Centre EquationGièresFrance

Personalised recommendations