Abstract
Schedulability analysis is one of the most important issues in developing and analyzing real-time systems. Given a task system where each task is characterized by a worst-case execution time (WCET) and a relative deadline, the schedulability analysis is decidable. However in reality, it is difficult to calculate the WCET of a complex task, even after it is abstracted to a formal model, e.g., timed automata (TAs). This paper proposes a schedulability analysis method without the information of the WCET, by introducing a model named timed regular task automata (TRTAs). Each task is described by a TA, a starting point with a clock valuation, a status and a relative deadline. A test is performed on each TA for an under-approximation of the WCET. The system may still be unschedulable under the approximation. A further schedulability checking is then performed by encoding to the reachability problem of nested timed automata (NeTAs). The methodology is thus sound and complete.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Buttazzo, G.C.: Hard Real-Time Computing Systems: Predictable Scheduling Algorithms and Applications. Springer, New York (2004)
Fersman, E., Krcal, P., Pettersson, P., Wang, Y.: Task automata: schedulability, decidability and undecidability. Inform. Comput. 205(8), 1149–1172 (2007)
Wilhelm, R., Engblom, J., Ermedahl, A., Holsti, N., Thesing, S., Whalley, D.B., Bernat, G., Ferdinand, C., Heckmann, R., Mitra, T., Mueller, F., Puaut, I., Puschner, P.P., Staschulat, J., Stenström, P.: The worst-case execution-time problem - overview of methods and survey of tools. ACM Trans. Embed. Comput. Syst. 7(3), 1–53 (2008)
Ericsson, C., Wall, A., Wang, Y.: Timed automata as task models for event-driven systems. In: Proceedings of the 6th International Conference on Real-Time Computing Systems and Applications (RTCSA 1999), pp. 182–189. IEEE Computer Society (1999)
Li, G., Cai, X., Ogawa, M., Yuen, S.: Nested timed automata. In: Braberman, V., Fribourg, L. (eds.) FORMATS 2013. LNCS, vol. 8053, pp. 168–182. Springer, Heidelberg (2013). doi:10.1007/978-3-642-40229-6_12
Li, G., Ogawa, M., Yuen, S.: Nested timed automata with frozen clocks. In: Sankaranarayanan, S., Vicario, E. (eds.) FORMATS 2015. LNCS, vol. 9268, pp. 189–205. Springer, Heidelberg (2015). doi:10.1007/978-3-319-22975-1_13
Wang, Y., Li, G., Yuen, S.: Nested timed automata with various clocks. Sci. Found. China 24(2), 51–68 (2016)
Choffrut, C., Goldwurm, M.: Timed automata with periodic clock constraints. J. Autom. Lang. Comb. 5(4), 371–404 (2000)
Altisen, K., Gössler, G., Pnueli, A., Sifakis, J., Tripakis, S., Yovine, S.: A framework for scheduler synthesis. In: Proceedings of the 20th IEEE Real-Time Systems Symposium (RTSS 1999), pp. 154–163. IEEE Computer Society (1999)
Abdeddam, Y., Maler, O.: Job-Shop Scheduling Using Timed Automata? Springer, Berlin (2001)
Fehnker, A.: Scheduling a steel plant with timed automata. In: Proceedings of the Sixth International Conference on Real-Time Computing Systems and Applications, pp. 280–286 (1999)
Fersman, E., Pettersson, P., Yi, W.: Timed automata with asynchronous processes: schedulability and decidability. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 67–82. Springer, Heidelberg (2002). doi:10.1007/3-540-46002-0_6
Trivedi, A., Wojtczak, D.: Recursive timed automata. In: Bouajjani, A., Chin, W.-N. (eds.) ATVA 2010. LNCS, vol. 6252, pp. 306–324. Springer, Heidelberg (2010). doi:10.1007/978-3-642-15643-4_23
Benerecetti, M., Minopoli, S., Peron, A.: Analysis of timed recursive state machines. In: Proceedings of the 17th International Symposium on Temporal Representation and Reasoning (TIME 2010), pp. 61–68. IEEE Computer Society (2010)
Benerecetti, M., Peron, A.: Timed recursive state machines: expressiveness and complexity. Theor. Comput. Sci. 625, 85–124 (2016)
Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)
Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. Inform. Comput. 111(2), 193–244 (1994)
Abdulla, P.A., Atig, M.F., Stenman, J.: Dense-timed pushdown automata. In: Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science (LICS 2012), pp. 35–44. IEEE Computer Society (2012)
Kozen, D.C.: Automata and Computability. Springer, New York (1951)
Acknowledgements
This work is supported by National Natural Science Foundation of China with grant No. 61472240, 61672340, 61472238, and the NSFC-JSPS bilateral joint research project with grant No. 61511140100.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing AG
About this paper
Cite this paper
Fang, B., Li, G., Sun, D., Cai, H. (2016). Schedulability Analysis of Timed Regular Tasks by Under-Approximation on WCET. In: Fränzle, M., Kapur, D., Zhan, N. (eds) Dependable Software Engineering: Theories, Tools, and Applications. SETTA 2016. Lecture Notes in Computer Science(), vol 9984. Springer, Cham. https://doi.org/10.1007/978-3-319-47677-3_10
Download citation
DOI: https://doi.org/10.1007/978-3-319-47677-3_10
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-47676-6
Online ISBN: 978-3-319-47677-3
eBook Packages: Computer ScienceComputer Science (R0)