Abstract
We present a method that allows to guarantee liveness by construction of a class of timed systems. The method is based on the use of a set of structural properties which can be checked locally at low cost. We provide sufficient conditions for liveness preservation by parallel composition and priority choice operators. The latter allow to restrict a system’s behavior according to a given priority order on its actions.
We present several examples illustrating the use of the results, in particular for the construction of live controllers.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
K. Altisen, G. Gößler, A. Pnueli, J. Sifakis, S. Tripakis, and S. Yovine. A Framework for Scheduler Synthesis. In IEEE RTSS’99 proceedings, 1999. 109
R. Alur and D.L. Dill. A theoryof timed automata. TCS, 126, pp. 183–235, 1994.
E. Asarin, O. Maler, and A. Pnueli. Symbolic Controller Synthesis for Discrete and Timed Systems. Hybrid Systems II, LNCS 999, Springer-Verlag, 1995. 109
P. C. Attie. Synthesis of Large Concurrent Programs via Pairwise Composition. In CONCUR’99.
J. C. M. Baeten, J. A. Bergstra, and J. W. Klop. Syntax and defining equations for an interrupt mechanism in process algebra. Fundamenta Informaticae IX (2), pp. 127–168, 1986. 125
S. Bornot and J. Sifakis. On the composition of hybrid systems. In International Workshop “Hybrid Systems: Computation and Control”, LNCS, pp. 49–63. Springer-Verlag, April 1998. 110, 112, 117, 118, 125
S. Bornot and J. Sifakis. An Algebraic Framework for Urgency. In Calculational System Design, NATO Science Series, Computer and Systems Science 173, Marktoberdorf, July 1998. 110, 112, 115, 117, 118, 125
S. Bornot, J. Sifakis, and S. Tripakis. Modeling urgency in timed systems. In COMPOS’97, Malente, Germany. LNCS 1536, Springer-Verlag, 1998. 110, 125
L. P. Carloni, K. L. McMillan, and A. L. Sangiovanni-Vincentelli. Latency Insensitive Protocols. In CAV’99, Trento, Italy. LNCS 1633, Springer-Verlag, 1999. 125
R. Cleaveland, G. Lüttgen, V. Natarajan, and S. Sims. Priorities for Modeling and Verifying Distributed Systems. In TACAS’96, LNCS 1055, pp. 278–297. 125
T. A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. Proc. 7th Symp. on Logics in Computer Science (LICS’92) and Information and Computation 111(2):193–244, 1994.
C. A. R. Hoare. Communicating Sequential Processes. Prentice Hall, 1985. 120
M. V. Iordache, J. O. Moody, and P. J. Antsaklis. A Method for Deadlock Prevention in Discrete Event Systems Using Petri Nets. Technical Report, University of Notre Dame, July 1999. 125
H. Kwak, I. Lee, A. Philippou, J. Choi, and O. Sokolsky. Symbolic schedulability analysis of real-time systems. In IEEE RTSS’98, Madrid, Spain, December 1998. 125
R. Milner. Communication and Concurrency. Prentice Hall, 1989. 120
S. Tripakis. Verifying Progress in Timed Systems. In ARTS’99, Bamberg, Germany, 1999 (to appear in LNCS series). 114, 125
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bornot, S., Gößler, G., Sifakis, J. (2000). On the Construction of Live Timed Systems. In: Graf, S., Schwartzbach, M. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2000. Lecture Notes in Computer Science, vol 1785. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46419-0_9
Download citation
DOI: https://doi.org/10.1007/3-540-46419-0_9
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67282-1
Online ISBN: 978-3-540-46419-8
eBook Packages: Springer Book Archive