Skip to main content
Top
Published in: International Journal on Software Tools for Technology Transfer 1/2023

19-01-2023 | General

An evaluation of approaches to model checking real-time task schedulability analysis

Authors: Madoda Nxumalo, Nils Timm, Stefan Gruner

Published in: International Journal on Software Tools for Technology Transfer | Issue 1/2023

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

This article is a follow-up contribution that extends the conference paper (Nxumalo, in: Laarman, Sokolova (eds)Model Checking Software - 27th International Symposium, 2021) which presented the spotlight abstraction method to enable an efficient model checking of schedulability properties of real-time operating systems. Our approach is based on iterative spotlight abstraction whereby the real-time task queue is divided into a so-called spotlight and a shade. Initially, an abstract state space model is generated from the spotlight, which contains a small number of tasks that appear at the front of the queue and the shade contains the remaining tasks. The schedulability of the spotlight tasks is model checked, whereas the behavior of the shade is summarized, and the result is saved for later re-use. If this result is still inconclusive, more tasks are iteratively brought from the shade into the spotlight, with which the model checker can proceed. These steps are repeated until a decisive schedulability result is obtained. In this article, we enrich the encoding of real-time systems into timed automata by separating operations over clock variables from operations based on other variables such as Boolean and integers. We enforce to maintain a reasonable size of the spotlight model by applying counter abstraction to the tasks that were previously confirmed schedulable in the previous iterations. We compare our approach against Timestool and RTLib, an Uppaal template, in the analysis of the schedulability of real-time tasks for the First-In-First-Out and Shortest-Deadline-First scheduling policies. Empirical results show that our approach can handle more tasks than Timestool and RTLib.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Footnotes
1
To avoid any mis-understanding at this point: Our analysis technique is designed only for those systems which can be completely analyzed ‘statically’ before their actual deployment; here, we are thus not dealing with any ‘on-the-fly’ schedulability analysis at run-time by means of an auxiliary analysis process within the ‘core’ of some rtos itself. For this reason, the queue in our formal model contains only formal representations of the tasks of interest (instead of actual processes in the form of their concrete process control blocks).
 
2
Worst case of the analysis: The entire queue is eventually in the spotlight and the shade is \(\{\}\).
 
3
We borrow the notation assume(e) from three valued model checking where assume(e) is a guard and e is an expression.
 
4
Setting the run-time of a task to 0 at ‘enqueue’ presumes a FIFO scheduling system in which it is not; possible to re-enqueue an un-finished task.
 
Literature
1.
go back to reference Abdeddaïm, Y., Maler, O.: Preemptive job-shop scheduling using stopwatch automata. In: Tools and Algorithms for the Construction and Analysis of Systems, 8th International Conference, TACAS 2002, Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2002, Grenoble, France, April 8-12, 2002, Proceedings. pp. 113–126 (2002). https://doi.org/10.1007/3-540-46002-0_9 Abdeddaïm, Y., Maler, O.: Preemptive job-shop scheduling using stopwatch automata. In: Tools and Algorithms for the Construction and Analysis of Systems, 8th International Conference, TACAS 2002, Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2002, Grenoble, France, April 8-12, 2002, Proceedings. pp. 113–126 (2002). https://​doi.​org/​10.​1007/​3-540-46002-0_​9
2.
go back to reference Amnell, T., Fersman, E., Mokrushin, L., Pettersson, P., Yi, W.: TIMES: a tool for schedulability analysis and code generation of real-time systems. In: Formal Modeling and Analysis of Timed Systems: First International Workshop, FORMATS 2003, Marseille, France, September 6-7, 2003. Revised Papers. pp. 60–72 (2003). https://doi.org/10.1007/978-3-540-40903-8_6 Amnell, T., Fersman, E., Mokrushin, L., Pettersson, P., Yi, W.: TIMES: a tool for schedulability analysis and code generation of real-time systems. In: Formal Modeling and Analysis of Timed Systems: First International Workshop, FORMATS 2003, Marseille, France, September 6-7, 2003. Revised Papers. pp. 60–72 (2003). https://​doi.​org/​10.​1007/​978-3-540-40903-8_​6
5.
go back to reference Bengtsson, J., Yi, W.: Timed automata: semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets, Advances in Petri Nets [This tutorial volume originates from the 4th Advanced Course on Petri Nets, ACPN 2003, held in Eichstätt, Germany in September 2003. In addition to lectures given at ACPN 2003, additional chapters have been commissioned]. Lecture Notes in Computer Science, vol. 3098, pp. 87–124. Springer (2003). https://doi.org/10.1007/978-3-540-27755-2_3 Bengtsson, J., Yi, W.: Timed automata: semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets, Advances in Petri Nets [This tutorial volume originates from the 4th Advanced Course on Petri Nets, ACPN 2003, held in Eichstätt, Germany in September 2003. In addition to lectures given at ACPN 2003, additional chapters have been commissioned]. Lecture Notes in Computer Science, vol. 3098, pp. 87–124. Springer (2003). https://​doi.​org/​10.​1007/​978-3-540-27755-2_​3
7.
go back to reference Bertout, A., Forget, J., Olejnik, R.: Minimizing a real-time task set through task clustering. In: Jan, M., Hedia, B.B., Goossens, J., Maiza, C. (eds.) 22nd International Conference on Real-Time Networks and Systems, RTNS ’14, Versaille, France, October 8-10, 2014. p. 23. ACM (2014). https://doi.org/10.1145/2659787.2659820 Bertout, A., Forget, J., Olejnik, R.: Minimizing a real-time task set through task clustering. In: Jan, M., Hedia, B.B., Goossens, J., Maiza, C. (eds.) 22nd International Conference on Real-Time Networks and Systems, RTNS ’14, Versaille, France, October 8-10, 2014. p. 23. ACM (2014). https://​doi.​org/​10.​1145/​2659787.​2659820
9.
go back to reference Bouyer, P., Gastin, P., Herbreteau, F., Sankur, O., Srivathsan, B.: Zone-based verification of timed automata: extrapolations, simulations and what next? In: Bogomolov, S., Parker, D. (eds.) Formal Modeling and Analysis of Timed Systems - 20th International Conference, FORMATS 2022, Warsaw, Poland, September 13-15, 2022, Proceedings. Lecture Notes in Computer Science, vol. 13465, pp. 16–42. Springer (2022). https://doi.org/10.1007/978-3-031-15839-1_2 Bouyer, P., Gastin, P., Herbreteau, F., Sankur, O., Srivathsan, B.: Zone-based verification of timed automata: extrapolations, simulations and what next? In: Bogomolov, S., Parker, D. (eds.) Formal Modeling and Analysis of Timed Systems - 20th International Conference, FORMATS 2022, Warsaw, Poland, September 13-15, 2022, Proceedings. Lecture Notes in Computer Science, vol. 13465, pp. 16–42. Springer (2022). https://​doi.​org/​10.​1007/​978-3-031-15839-1_​2
10.
go back to reference Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) Computer Aided Verification, 12th International Conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000, Proceedings. Lecture Notes in Computer Science, vol. 1855, pp. 154–169. Springer (2000). https://doi.org/10.1007/10722167_15 Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) Computer Aided Verification, 12th International Conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000, Proceedings. Lecture Notes in Computer Science, vol. 1855, pp. 154–169. Springer (2000). https://​doi.​org/​10.​1007/​10722167_​15
11.
go back to reference Dierks, H., Kupferschmid, S., Larsen, K.G.: Automatic abstraction refinement for timed automata. In: Raskin, J., Thiagarajan, P.S. (eds.) Formal Modeling and Analysis of Timed Systems, 5th International Conference, FORMATS 2007, Salzburg, Austria, October 3-5, 2007, Proceedings. Lecture Notes in Computer Science, vol. 4763, pp. 114–129. Springer (2007). https://doi.org/10.1007/978-3-540-75454-1_10 Dierks, H., Kupferschmid, S., Larsen, K.G.: Automatic abstraction refinement for timed automata. In: Raskin, J., Thiagarajan, P.S. (eds.) Formal Modeling and Analysis of Timed Systems, 5th International Conference, FORMATS 2007, Salzburg, Austria, October 3-5, 2007, Proceedings. Lecture Notes in Computer Science, vol. 4763, pp. 114–129. Springer (2007). https://​doi.​org/​10.​1007/​978-3-540-75454-1_​10
12.
go back to reference Fersman, E., Mokrushin, L., Pettersson, P., Yi, W.: Schedulability analysis using two clocks. In: Garavel, H., Hatcliff, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 9th International Conference, TACAS 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings. Lecture Notes in Computer Science, vol. 2619, pp. 224–239. Springer (2003). https://doi.org/10.1007/3-540-36577-X_16 Fersman, E., Mokrushin, L., Pettersson, P., Yi, W.: Schedulability analysis using two clocks. In: Garavel, H., Hatcliff, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 9th International Conference, TACAS 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings. Lecture Notes in Computer Science, vol. 2619, pp. 224–239. Springer (2003). https://​doi.​org/​10.​1007/​3-540-36577-X_​16
13.
go back to reference Fersman, E., Pettersson, P., Yi, W.: Timed automata with asynchronous processes: schedulability and decidability. In: Katoen, J., Stevens, P. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 8th International Conference, TACAS 2002, Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2002, Grenoble, France, April 8-12, 2002, Proceedings. Lecture Notes in Computer Science, vol. 2280, pp. 67–82. Springer (2002). https://doi.org/10.1007/3-540-46002-0_6 Fersman, E., Pettersson, P., Yi, W.: Timed automata with asynchronous processes: schedulability and decidability. In: Katoen, J., Stevens, P. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 8th International Conference, TACAS 2002, Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2002, Grenoble, France, April 8-12, 2002, Proceedings. Lecture Notes in Computer Science, vol. 2280, pp. 67–82. Springer (2002). https://​doi.​org/​10.​1007/​3-540-46002-0_​6
14.
go back to reference Govind, R., Herbreteau, F., Srivathsan, B., Walukiewicz, I.: Revisiting local time semantics for networks of timed automata. In: Fokkink, W.J., van Glabbeek, R. (eds.) 30th International Conference on Concurrency Theory, CONCUR 2019, August 27-30, 2019, Amsterdam, the Netherlands. LIPIcs, vol. 140, pp. 16:1–16:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019). https://doi.org/10.4230/LIPIcs.CONCUR.2019.16 Govind, R., Herbreteau, F., Srivathsan, B., Walukiewicz, I.: Revisiting local time semantics for networks of timed automata. In: Fokkink, W.J., van Glabbeek, R. (eds.) 30th International Conference on Concurrency Theory, CONCUR 2019, August 27-30, 2019, Amsterdam, the Netherlands. LIPIcs, vol. 140, pp. 16:1–16:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019). https://​doi.​org/​10.​4230/​LIPIcs.​CONCUR.​2019.​16
16.
go back to reference Herbreteau, F., Srivathsan, B., Walukiewicz, I.: Lazy abstractions for timed automata. In: Sharygina, N., Veith, H. (eds.) Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings. Lecture Notes in Computer Science, vol. 8044, pp. 990–1005. Springer (2013). https://doi.org/10.1007/978-3-642-39799-8_71 Herbreteau, F., Srivathsan, B., Walukiewicz, I.: Lazy abstractions for timed automata. In: Sharygina, N., Veith, H. (eds.) Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings. Lecture Notes in Computer Science, vol. 8044, pp. 990–1005. Springer (2013). https://​doi.​org/​10.​1007/​978-3-642-39799-8_​71
18.
20.
go back to reference Laroussinie, F., Larsen, K.G.: CMC: A tool for compositional model-checking of real-time systems. In: Budkowski, S., Cavalli, A.R., Najm, E. (eds.) Formal Description Techniques and Protocol Specification, Testing and Verification, FORTE XI / PSTV XVIII’98, IFIP TC6 WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE XI) and Protocol Specification, Testing and Verification (PSTV XVIII), 3-6 November, 1998, Paris, France. IFIP Conference Proceedings, vol. 135, pp. 439–456. Kluwer (1998) Laroussinie, F., Larsen, K.G.: CMC: A tool for compositional model-checking of real-time systems. In: Budkowski, S., Cavalli, A.R., Najm, E. (eds.) Formal Description Techniques and Protocol Specification, Testing and Verification, FORTE XI / PSTV XVIII’98, IFIP TC6 WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE XI) and Protocol Specification, Testing and Verification (PSTV XVIII), 3-6 November, 1998, Paris, France. IFIP Conference Proceedings, vol. 135, pp. 439–456. Kluwer (1998)
22.
go back to reference McManis, J., Varaiya, P.: Suspension automata: A decidable class of hybrid automata. In: Dill, D.L. (ed.) Computer Aided Verification, 6th International Conference, CAV ’94, Stanford, California, USA, June 21-23, 1994, Proceedings. Lecture Notes in Computer Science, vol. 818, pp. 105–117. Springer (1994) McManis, J., Varaiya, P.: Suspension automata: A decidable class of hybrid automata. In: Dill, D.L. (ed.) Computer Aided Verification, 6th International Conference, CAV ’94, Stanford, California, USA, June 21-23, 1994, Proceedings. Lecture Notes in Computer Science, vol. 818, pp. 105–117. Springer (1994)
23.
go back to reference Nxumalo, M., Timm, N., Gruner, S.: Spotlight abstraction in model checking real-time task schedulability. In: Laarman, A., Sokolova, A. (eds.) Model Checking Software - 27th International Symposium, SPIN 2021, Virtual Event, July 12, 2021, Proceedings. Lecture Notes in Computer Science, vol. 12864, pp. 63–80. Springer (2021). https://doi.org/10.1007/978-3-030-84629-9_4 Nxumalo, M., Timm, N., Gruner, S.: Spotlight abstraction in model checking real-time task schedulability. In: Laarman, A., Sokolova, A. (eds.) Model Checking Software - 27th International Symposium, SPIN 2021, Virtual Event, July 12, 2021, Proceedings. Lecture Notes in Computer Science, vol. 12864, pp. 63–80. Springer (2021). https://​doi.​org/​10.​1007/​978-3-030-84629-9_​4
24.
go back to reference Roussanaly, V., Sankur, O., Markey, N.: Abstraction refinement algorithms for timed automata. In: Dillig, I., Tasiran, S. (eds.) Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I. Lecture Notes in Computer Science, vol. 11561, pp. 22–40. Springer (2019). https://doi.org/10.1007/978-3-030-25540-4_2 Roussanaly, V., Sankur, O., Markey, N.: Abstraction refinement algorithms for timed automata. In: Dillig, I., Tasiran, S. (eds.) Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I. Lecture Notes in Computer Science, vol. 11561, pp. 22–40. Springer (2019). https://​doi.​org/​10.​1007/​978-3-030-25540-4_​2
27.
go back to reference Sorea, M.: Lazy approximation for dense real-time systems. In: Lakhnech, Y., Yovine, S. (eds.) Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, Joint International Conferences on Formal Modelling and Analysis of Timed Systems, FORMATS 2004 and Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT 2004, Grenoble, France, September 22-24, 2004, Proceedings. Lecture Notes in Computer Science, vol. 3253, pp. 363–378. Springer (2004). https://doi.org/10.1007/978-3-540-30206-3_25 Sorea, M.: Lazy approximation for dense real-time systems. In: Lakhnech, Y., Yovine, S. (eds.) Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, Joint International Conferences on Formal Modelling and Analysis of Timed Systems, FORMATS 2004 and Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT 2004, Grenoble, France, September 22-24, 2004, Proceedings. Lecture Notes in Computer Science, vol. 3253, pp. 363–378. Springer (2004). https://​doi.​org/​10.​1007/​978-3-540-30206-3_​25
28.
go back to reference Stallings, W.: Operating Systems - Internals and Design Principles (7th ed.). Pitman (2011) Stallings, W.: Operating Systems - Internals and Design Principles (7th ed.). Pitman (2011)
Metadata
Title
An evaluation of approaches to model checking real-time task schedulability analysis
Authors
Madoda Nxumalo
Nils Timm
Stefan Gruner
Publication date
19-01-2023
Publisher
Springer Berlin Heidelberg
Published in
International Journal on Software Tools for Technology Transfer / Issue 1/2023
Print ISSN: 1433-2779
Electronic ISSN: 1433-2787
DOI
https://doi.org/10.1007/s10009-022-00693-9

Other articles of this Issue 1/2023

International Journal on Software Tools for Technology Transfer 1/2023 Go to the issue

Premium Partner