nach oben

Cluster Computing

Erschienen in:

01.02.2018

An improved formalization analysis approach to determine schedulability of global multiprocessor scheduling based on symbolic safety analysis and statistical model checking in smartphone systems

verfasst von: Haibin Cai, Hao Wu

Erschienen in: Cluster Computing | Sonderheft 2/2019

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Modern smart phones are typically equipped with multicore processors. In this paper, we address the problem of determining schedulability of a real-time periodic taskset with fixed release offsets and possible release jitters on a multicore processor with global Fixed-Priority (FP) or EDF (Earliest Deadline First) scheduling algorithms, using the model-checker UPPAAL for Timed Automata. In addition to yes/no schedulability analysis for hard real-time systems, we also apply statistical model checking to estimate the probability of unschedulability for soft real-time systems, described with two statistical parameters (confidence and accuracy).

Nächster Artikel Research on a large-scale community detection algorithm based on non-weighted graph

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren

Davis, R.I., Burns, A.: A survey of hard real-time scheduling for multiprocessor systems. ACM Comput. Surv. 43(4), 35 (2011)

Tindell, K.: Adding time-offsets to schedulability analysis. Technical report, University of York (1994)

Yomsi, P.M., Bertrand, D., Navet, N., Davis, R.L.: Controller area network (CAN): response time analysis with offsets. In: WFCS, pp. 43–52 (2012)

Amnell, T., Fersman, E., Mokrushin, L., Pettersson, P., Wang, Y.: Times: a tool for schedulability analysis and code generation of real-time systems. In: Larsen, K.G., Niebert, P. (eds.) FORMATS. Lecture Notes in Computer Science, vol. 2791, pp. 60–72. Springer (2003)

Fersman, E., Mokrushin, L., Petersson, P., Wang, Y.: Schedulability analysis of fixed-priority systems using timed automata. Theor. Comput. Sci. 354(2), 301–317

Waszniowski, L., Hanzalek, Z.: Formal verification of multitasking applications based on timed automata model. Real-Time Syst. 38(1), 39–65 (2008)

UPPAAL HELP. http://www.uppaal.org/ (2016)

Cicirelli, F., Furfaro, A., Nigro, L., Pupo, F.: Development of a schedulability analysis framework based on ptpn and uppaal with stopwatches. In: Boukerche, A., Cahill, V., El-Saddik, A., Theodoropoulos, G.K., Walshe, R. (eds.) DS-RT:57-64. IEEE Computer Society (2012)

Aske Wiid, B., Hansen, M.R., Madsen, J.: Models and formal verification of multiprocessor system-on-chips. J. Log. Algebraic Program. 77(1–2), 1–19 (2008)

10.

David, A., Illum, J., Larsen, K.G., Skou, A.: Model-based framework for schedulability analysis using uppaal 4.1. In: Model-based Design for Embedded Systems, pp. 93–119 (2010)

11.

Baker, T.P., Cirinei, M.: Brute-force determination of multiprocessor schedulability for sets of sopradic hard-deadline tasks. In: Tovar, E., Tsigas, P., Fouchal, H. (eds.) OPODIS, vol. 4878, pp. 62–75. Springer (2007)

12.

Cordovilla, M., Boniol, F., Noulard, E., Pagetti, C.: Multiprocessor schedulability analyser. In: Chu, W.C., Wong, E.W., Palakal, M.J., Hung, C.-C. (eds.) SAC, pp. 735–741. ACM (2011)

13.

Boudjadar, A., David, A., Kim, J.H., Kim, L.G., Mikucionis, M., Nyman, U., Skou, A.: Hierarchical scheduling framework based on compositional analysis using UPPAAL. In: Fiadeiro, J.L. (ed.) Proceedings of the Formal Aspects of Component Software, pp. 61–78. Springer (2014)

14.

David, A., Larsen, K.G., Legay, A., Mikucionis, M.: Schedulability of Herschel-Planck revisited using statistical model checking. In: Margaria, T. (ed.) Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies, pp. 293–307. Springer (2012)

15.

Oguzcan, O., Broenink, J.F., Mader, A.: Schedulability analysis of timed CSP models using the pat model checker. In: Communicating Process Architectures. Open Channel Publishing Ltd (2012)

16.

Carnevali, L., Pinzuti, A., Vicario, E.: Compositional verification for hierarchical scheduling of real-time systems. IEEE Trans. Softw. Eng. 39(5), 638–657 (2013)

17.

Ericsson, C., Wall, A., Yi, W.: Timed automata as task models for event-driven systems. In: Proceedings of Nordic Workshop on Programming Theory (1998)

18.

Fersman, E., Pettersson, P., Yi, W.: Timed automata with asynchronous processed: schedulability and decidability. In: Proceedings of TACAS02. LNCS, vol. 2280, pp. 67–82 (2002)

19.

Schmitz, M.T., Al-Hashimi, B.M., Eles, P.: System-Level Design Techniques for Energy-Efficient Embedded Systems. Springer (2004). https://doi.org/10.1007/b106642

20.

Clarke, EM., Zuliani, P.: Statistical model checking for cyber-physical systems. In: Proceedings of the 9th International Conference on Automated Technology for Verification and Analysis (ATVA’11), pp. 1–12. Taipei, Taiwan, 11–14 Oct 2011

21.

David, A., Larsen, K.G., Legay, A., Mikucionis, M.: Schedulability of Herschel revisited using statistical model checking. Int. J. Softw. Tools Technol. Transf. 17(2), 187–199 (2015)

22.

Christensen, S., Kristensen, L., Mailund, T.: A sweep-line method for state space exploration. In: TACAS, pp. 450–464 (2001)

23.

Cassez, F., Larsen, K.G.: The impressive power of stopwatches. In: Palamidessi, C. (ed.) CONCUR. Lecture Notes in Computer Science, vol. 1877, pp. 138–152 (2000)

Titel: An improved formalization analysis approach to determine schedulability of global multiprocessor scheduling based on symbolic safety analysis and statistical model checking in smartphone systems
verfasst von: Haibin Cai
Hao Wu
Publikationsdatum: 01.02.2018
Verlag: Springer US
Erschienen in: Cluster Computing / Ausgabe Sonderheft 2/2019
Print ISSN: 1386-7857
Elektronische ISSN: 1573-7543
DOI: https://doi.org/10.1007/s10586-017-1319-0

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Weitere Artikel der Sonderheft 2/2019

Repeated game analysis of power suppliers based on dynamic coopetition process and slightly altruistic factor

Modelling the spice parameters of SOI MOSFET using a combinational algorithm

Evaluation method based on neural network differential evolution

Study on the sealing integrity of cement sheath during volume fracturing of shale gas of horizontal well

A secure and efficient cluster based location aware routing protocol in MANET

Local weighted regression statistical analysis based mathematical education evaluation

Premium Partner