Abstract
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.
Work partially supported by CNRS STIC project “CORTOS” and by IST Network of Excellence “ARTIST2”.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science 126, 183–235 (1994)
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)
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)
Amnell, T., Fersman, E., Pettersson, P., Yi, W., Sun, H.: Code synthesis for timed automata. Nordic J. of Computing 9(4), 269–300 (2002)
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)
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)
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)
de Alfaro, L., Henzinger, T.A.: Interface automata. In: Foundations of Software Engineering (FSE). ACM Press, New York (2001)
Halbwachs, N.: Synchronous Programming of Reactive Systems. Kluwer, Dordrecht (1992)
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)
Henzinger, T., Manna, Z., Pnueli, A.: What good are digital clocks? In: Kuich, W. (ed.) ICALP 1992. LNCS, vol. 623. Springer, Heidelberg (1992)
Kopetz, H.: Real-Time Systems Design Principles for Distributed Embedded Applications. Kluwer, Dordrecht (1997)
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)
Larsen, K., Petterson, P., Yi, W.: Uppaal in a nutshell. Software Tools for Technology Transfer 1(1/2) (October 1997)
Ouaknine, J., Worrell, J.: Revisiting digitization, robustness, and decidability for timed automata. In: LICS 2003. IEEE CS Press, Los Alamitos (2003)
Puri, A.: Dynamical properties of timed automata. Discrete Event Dynamic Systems 10(1-2), 87–113 (2000)
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)
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)
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)
Tripakis, S., Yovine, S.: Analysis of timed systems using time-abstracting bisimulations. Formal Methods in System Design 18(1), 25–68 (2001)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Altisen, K., Tripakis, S. (2005). Implementation of Timed Automata: An Issue of Semantics or Modeling?. In: Pettersson, P., Yi, W. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2005. Lecture Notes in Computer Science, vol 3829. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11603009_21
Download citation
DOI: https://doi.org/10.1007/11603009_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-30946-8
Online ISBN: 978-3-540-31616-9
eBook Packages: Computer ScienceComputer Science (R0)