Abstract
Timed systems can be modeled as automata (or, generally, discrete transition structures) extended with real-valued variables (clocks) measuring the time elapsed since their initialization. The following features are also common in the above models.
-
States are associated with time progress conditions specifying how time can advance. Time can progress at a state by t only if all the intermediate states reached satisfy the associated time progress condition.
-
At transitions, clock values can be tested and modified. This is usually done by associating with transitions guards (conditions on clocks) and assignments. If a guard is true from an automaton state and a given clock valuation, the corresponding transition can be executed by modifying clocks as specified by the corresponding assignment.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
N.C. Audsley, A. Bums, M.F. Richardson, and A.J. Wellings. Deadlinemonotonic scheduling. In Proc. 8th IEEE Workshop on Real-time Operating Systems and Software, 1991.
R. Alur, C. Courcoubetis, and D.L. Dill. Model checking in dense real time. Information and Computation, 104(1):2–34, 1993.
J.F. Allen. Maintaining knowledge about temporal intervals. Communications of the ACM, 26(11):832–843, November 1983.
S. Bornot and J. Sifakis. On the composition of hybrid systems (complete version). In International NATO Summer School on “Verification of Digital and Hybrid Systems”, Antalya, Turkey, 1997.
S. Bornot and J. Sifakis. Relating time progress and deadlines in hybrid systems. In International Workshop, HART’97, pages 286–300, Grenoble, France, March 1997. Lecture Notes in Computer Science 1201, Spinger-Verlag.
T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. Information and Computation, 111(2):193–244, 1994.
M. Jourdan, N. Layaïda, L. Sabry-Ismail, and C. Roisin. Authoring and presentation environment for interactive multimedia documents. In Proc. of the 4th Conf. on Multimedia Modelling, Singapore, November 1997. World Scientific Publishing.
P. Merlin. A study of the recoverability of computer systems. Master’s thesis, University of California, Irvine, 1974.
P. Sénac, M. Diaz, and P. de Saqui-Sannes. Toward a formal specification of multimedia scenarios. Annals of telecomunications, 49(5-6):297–314, 1994.
J. Sifakis. Use of petri nets for performance evaluation. In H. Beilner and E. Gelenebe, editors, Measuring, modelling and evaluating computer systems, pages 75–93. North-Holland, 1977.
J. Sifakis and S. Yovine. Compositional specification of timed systems. In 13th Annual Symposium on Theoretical Aspects of Computer Science, STACS’96, pages 347–359, Grenoble, France, February 1996. Lecture Notes in Computer Science 1046, Spinger-Verlag.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bornot, S., Sifakis, J., Tripakis, S. (1998). Modeling Urgency in Timed Systems. In: de Roever, WP., Langmaack, H., Pnueli, A. (eds) Compositionality: The Significant Difference. COMPOS 1997. Lecture Notes in Computer Science, vol 1536. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49213-5_5
Download citation
DOI: https://doi.org/10.1007/3-540-49213-5_5
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65493-3
Online ISBN: 978-3-540-49213-9
eBook Packages: Springer Book Archive