A Unified Formalism for Monoprocessor Schedulability Analysis Under Uncertainty

  • Étienne AndréEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10471)


The schedulability analysis of real-time systems (even on a single processor) is a very difficult task, which becomes even more complex (or undecidable) when periods or deadlines become uncertain. In this work, we propose a unified formalism to model monoprocessor schedulability problems with several types of tasks (periodic, sporadic, or more complex), most types of schedulers (including \(\mathsf {EDF}\), \(\mathsf {FPS}\) and \(\mathsf {SJF}\)), with or without preemption, in the presence of uncertain timing constants. Although the general case is undecidable, we exhibit a large decidable subclass. We demonstrate the expressive power of our formalism on several examples, allowing also for robust schedulability.


Schedulability analysis Real-time systems Timing parameters 


  1. 1.
    Abdeddaïm, Y., Maler, O.: Preemptive job-shop scheduling using stopwatch automata. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 113–126. Springer, Heidelberg (2002). doi: 10.1007/3-540-46002-0_9 CrossRefGoogle Scholar
  2. 2.
    Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)CrossRefzbMATHMathSciNetGoogle Scholar
  3. 3.
    Alur, R., Henzinger, T.A., Vardi, M.Y.: Parametric real-time reasoning. In: STOC, pp. 592–601. ACM (1993)Google Scholar
  4. 4.
    André, É.: What’s decidable about parametric timed automata? In: Artho, C., Ölveczky, P.C. (eds.) FTSCS 2015. CCIS, vol. 596, pp. 52–68. Springer, Cham (2016). doi: 10.1007/978-3-319-29510-7_3 CrossRefGoogle Scholar
  5. 5.
    André, É., Fribourg, L., Kühne, U., Soulat, R.: IMITATOR 2.5: a tool for analyzing robustness in scheduling problems. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 33–36. Springer, Heidelberg (2012). doi: 10.1007/978-3-642-32759-9_6 CrossRefGoogle Scholar
  6. 6.
    André, É., Lipari, G., Sun, Y.: Verification of two real-time systems using parametric timed automata. In: WATERS (2015)Google Scholar
  7. 7.
    Bagnara, R., Hill, P.M., Zaffanella, E.: The parma polyhedra library: toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Program. 72(1–2), 3–21 (2008)CrossRefMathSciNetGoogle Scholar
  8. 8.
    Bérard, B., Haddad, S., Jovanović, A., Lime, D.: Parametric interrupt timed automata. In: Abdulla, P.A., Potapov, I. (eds.) RP 2013. LNCS, vol. 8169, pp. 59–69. Springer, Heidelberg (2013). doi: 10.1007/978-3-642-41036-9_7 CrossRefGoogle Scholar
  9. 9.
    Bouyer, P., Markey, N., Sankur, O.: Robustness in timed automata. In: Abdulla, P.A., Potapov, I. (eds.) RP 2013. LNCS, vol. 8169, pp. 1–18. Springer, Heidelberg (2013). doi: 10.1007/978-3-642-41036-9_1 CrossRefGoogle Scholar
  10. 10.
    Cassez, F., Larsen, K.: The impressive power of stopwatches. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 138–152. Springer, Heidelberg (2000). doi: 10.1007/3-540-44618-4_12 CrossRefGoogle Scholar
  11. 11.
    Cimatti, A., Palopoli, L., Ramadian, Y.: Symbolic computation of schedulability regions using parametric timed automata. In: RTSS, pp. 80–89. IEEE Computer Society (2008)Google Scholar
  12. 12.
    Fang, B., Li, G., Sun, D., Cai, H.: Schedulability analysis of timed regular tasks by under-approximation on WCET. In: Fränzle, M., Kapur, D., Zhan, N. (eds.) SETTA 2016. LNCS, vol. 9984, pp. 147–162. Springer, Cham (2016). doi: 10.1007/978-3-319-47677-3_10 CrossRefGoogle Scholar
  13. 13.
    Fersman, E., Krcál, P., Pettersson, P., Yi, W.: Task automata: schedulability, decidability and undecidability. Inf. Comput. 205(8), 1149–1172 (2007)CrossRefzbMATHMathSciNetGoogle Scholar
  14. 14.
    Hune, T., Romijn, J., Stoelinga, M., Vaandrager, F.W.: Linear parametric model checking of timed automata. J. Logic Algebr. Program. 52–53, 183–220 (2002)CrossRefzbMATHMathSciNetGoogle Scholar
  15. 15.
    Jovanović, A., Lime, D., Roux, O.H.: Integer parameter synthesis for timed automata. IEEE Trans. Softw. Eng. 41(5), 445–461 (2015)CrossRefzbMATHGoogle Scholar
  16. 16.
    Miller, J.S.: Decidability and complexity results for timed automata and semi-linear hybrid automata. In: Lynch, N., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 296–310. Springer, Heidelberg (2000). doi: 10.1007/3-540-46430-1_26 CrossRefGoogle Scholar
  17. 17.
    Norström, C., Wall, A., Yi, W.: Timed automata as task models for event-driven systems. In: RTCSA, pp. 182–189. IEEE Computer Society (1999)Google Scholar
  18. 18.
    Sun, Y., Soulat, R., Lipari, G., André, É., Fribourg, L.: Parametric schedulability analysis of fixed priority real-time distributed systems. In: Artho, C., Ölveczky, P.C. (eds.) FTSCS 2013. CCIS, vol. 419, pp. 212–228. Springer, Cham (2014). doi: 10.1007/978-3-319-05416-2_14 CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  1. 1.Université Paris 13, LIPN, CNRS, UMR 7030VilletaneuseFrance

Personalised recommendations