Abstract
In this paper, we exend timed automata with asynchronous processes i.e. tasks triggered by events as a model for real-time systems. The model is expressive enough to describe concurrency and synchronization, and real time tasks which may be periodic, sporadic, preemptive or non-preemptive. We generalize the classic notion of schedulability to timed automata. An automaton is schedulable if there exists a scheduling strategy such that all possible sequences of events accepted by the automaton are schedulable in the sense that all associated tasks can be computed within their deadlines. We believe that the model may serve as a bridge between scheduling theory and automata-theoretic approaches to system modeling and analysis. Our main result is that the schedulability checking problem is decidable. To our knowledge, this is the first general decidability result on dense-time models for real time scheduling without assuming that preemptions occur only at integer time points. The proof is based on a decidable class of updatable automata: timed automata with subtraction in which clocks may be updated by subtractions within a bounded zone. The crucial observation is that the schedulability checking problem can be encoded as a reachability problem for such automata. Based on the proof, we have developed a symbolic technique and a prototype tool for schedulability analysis.
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
Y. Abdeddaïm and O. Maler. Job-shop scheduling using timed automata. In Proceedings of 13th Conference on Computer Aided Verification, July 18–23, 2001 Paris, France, 2001.
K. Altisen, G. Göβler, A. Pnueli, J. Sifakis, S. Tripakis, and S. Yovine. A framework for scheduler synthesis. In Proceedings of the 20th IEEE Real-Time Systems Symposium, Phoenix, AZ, USA, 1–3 December, 1999, pages 154–163. IEEE Computer Society Press, 1999.
K. Altisen, G. Göβler, and J. Sifakis. A methodology for the construction of scheduled systems. In Proceedings of FTRTFT 2000, Pune, India, September 2000, LNCS 1926, pp.106–120, 2000.
R. Alur, C. Courcoubetis, N. Halbwachs, T. A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. The algorithmic analysis of hybrid systems. Theoretical Computer Science, 138(1):3–34, 1995.
R. Alur and D. L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183–235, 1994.
T. Amnell, E. Fersman, L. Mokrushin, P. Pettersson, and W. Yi. TIMES-a tool for modelling and implementation of embedded systems. In Proceedings of TACAS02. Springer-Verlag, 2002.
P. Bouyer, C. Dufourd, E. Fleury, and A. Petit. Are timed automata updatable? In Proceedings of the 12th International Conference on Computer-Aided Verification, Chicago, IL, USA, July 15–19, 2000, 2000. Springer-Verlag.
G. C. Buttazzo. Hard Real-Time Computing Systems. Predictable Scheduling Algorithms and Applications. Kulwer Academic Publishers, 1997.
F. Cassez and F. Laroussinie. Model-checking for hybrid systems by quotienting and constraints solving. In Proceedings of the 12th International Conference on Computer-Aided Verification, pages 373–388, Standford, California, USA, 2000. Springer-Verlag.
J. Corbett. Modeling and analysis of real-time ada tasking programs. In Proceedings of 15th IEEE Real-Time Systems Symposium, San Juan, Puerto Rico, USA, pages 132–141. IEEE Computer Society Press, 1994.
C. Ericsson, A. Wall, and W. Yi. Timed automata as task models for eventdriven systems. In Proceedings of the 6th International Conference on Real-Time Computing Systems and Applications (RTCSA’99). IEEE Computer Society Press, 1999.
A. Fehnker. Scheduling a steel plant with timed automata. In Proceedings of the 6th International Conference on Real-Time Computing Systems and Applications (RTCSA’99). IEEE Computer Society Press, 1999.
E. Fersman, P. Pettersson, and W. Yi. Timed automata with asynchronous processes: Schedulability and decidability. Technical report, Department of Information Technology, Uppsala University, Sweden, 2002.
T. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. Information and Computation, 111(2):193–244, 1994.
T. Hune, K. G. Larsen, and P. Pettersson. Guided Synthesis of Control Programs using Uppaal. Nordic Journal of Computing, 8(1):43–64, 2001.
K. G. Larsen, P. P., and W. Yi. Compositional and symbolic model-checking of real-time systems. In Proceedings of 16th IEEE Real-Time Systems Symposium, December 5–7, 1995-Pisa, Italy, pages 76–89. IEEE Computer Society Press, 1995.
K. G. Larsen, P. Pettersson, and W. Yi. Uppaal in a Nutshell. Journal on Software Tools for Technology Transfer, 1(1–2):134–152, October 1997.
J. McManis and P. Varaiya. Suspension automata: a decidable class of hybrid automata. In Proceedings of the 6th International Conference on Computer-Aided Verification, pages 105–117, Standford, California, USA, 1994. Springer-Verlag.
W. Yi, P. Pettersson, and M. Daniels. Automatic verification of real-time communicating systems by constraint-solving. In Proceedings of the 7th International Conference on Formal Description Techniques, 1994.
Sergio Yovine. A Verification Tool for Real Time Systems. Int. Journal on Software Tools for Technology Transfer, 1(1–2):134–152, October 1997.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fersman, E., Pettersson, P., Yi, W. (2002). Timed Automata with Asynchronous Processes: Schedulability and Decidability. In: Katoen, JP., Stevens, P. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2002. Lecture Notes in Computer Science, vol 2280. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46002-0_6
Download citation
DOI: https://doi.org/10.1007/3-540-46002-0_6
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43419-1
Online ISBN: 978-3-540-46002-2
eBook Packages: Springer Book Archive