Abstract
AUTOSAR, the open and emerging global standard for automotive embedded systems, offers a timing protection mechanism to protect tasks from missing their deadlines. However, in practice, it is difficult to predict when a deadline is violated, because a task missing its deadline may be caused by unrelated tasks or by the presence of interrupts. In this paper, we propose an abstract formal model to represent AUTOSAR OS programs with timing protection. We are able to determine schedulability properties and to calculate constraints on the allowed time that interrupts can take for a given task in a given period. We implement our model in Mathematica and give a case study to illustrate the utility of our method. Based on the results, we believe that our work can help designers and implementors of AUTOSAR OS programs check whether their programs satisfy crucial timing properties.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
AUTOSAR. Specification of Operating System V3.1.1 R3.1 Rev 0002 (2012), http://www.autosar.org/ (last accessed: July 1, 2013)
OSEK/VDX, http://www.osek-vdx.org/ (last accessed: July 1, 2013)
Arctic Core — the open-source AUTOSAR embedded platform, http://www.arccore.com/ (last accessed: July 1, 2013)
Wilhelm, R., Engblom, J., Ermedahl, A., Holsti, N., Thesing, S., Whalley, D., Bernat, G., Ferdinand, C., Heckmann, R., Mitra, T., Mueller, F., Puaut, I., Puschner, 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) (2008)
Tuch, H.: Formal Memory Models for Verifying C Systems Code. Ph.D. Thesis. University of NSW, Australia (2008)
Regehr, J., Reid, A., Webb, K.: Eliminating stack overflow by abstract interpretation. In: EMSOFT (2003)
Leyva-del-Foyo, L.E., Mejia-Alvarez, P., de Niz, D.: Predictable Interrupt Management for Real Time Kernels over conventional PC Hardware. In: RTAS (2006)
Wolfram Research, Inc., Mathematica, Version 8.0, Champaign, IL (2010).
Bertrand, D., Faucou, S., Trinquet, Y.: An analysis of the AUTOSAR OS timing protection mechanism. In: ETFA (2009)
Hladik, P.E., Deplanche, A.M., Faucou, S., Trinquet, Y.: Adequacy between AUTOSAR OS specification and real-time scheduling theory. In: SIES (2007)
Liu, C.L., Layland, J.W.: Scheduling Algorithms for Multiprogramming in a Hard-Real-Time Environment. Jounal of the Assocaition for Computing Macheinery 20(1) (1973)
Lehoczky, J.P.: Fixed priority scheduling of periodic task sets with arbitrary deadlines. In: RTSS (1990)
Harbour, M.G., Klein, M.H., Lehoczky, J.P.: Fixed Priority Scheduling of Periodic Tasks with Varying Execution Priority. In: RTSS (1991)
Katcher, D.I., Arakawa, H., Strosnider, J.K.: Engineering and analysis of fixed priority schedulers. IEEE Transactions on Software Engineering (1993)
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 2003. LNCS, vol. 2791, pp. 60–72. Springer, Heidelberg (2004)
Fersman, E., Wang, Y.: A Generic Approach to Schedulability Analysis of Real Time Tasks. Nordic Journal of Computing 11(2) (2004)
Krcal, P., Wang, Y.: Decidable and Undecidable Problems in Schedulability Analysis Using Timed Automata. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 236–250. Springer, Heidelberg (2004)
Fersman, E., Mokrushin, L., Pettersson, P., Wang, Y.: Schedulability Analysis of Fixed-Priority Systems Using Timed Automata. Journal of Theoretical Computer Science 354(2) (2006)
Brylow, D., Palsberg, J.: Deadline Analysis of Interrupt-Driven Software. IEEE Transactions on Software Engineering (2004)
Schwarz, M.D., Seidl, H., Vojdani, V., Lammich, P., Muller-Olm, M.: Static analysis of interrupt-driven programs synchronized via the priority ceiling protocol. In: POPL (2011)
Feng, X., Shao, Z., Guo, Y., Dong, Y.: Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads. J. Autom. Reasoning 42(2-4) (2009)
Zhao, Y., Huang, Y., He, J., Liu, S.: Formal Model of Interrupt Program from a Probabilistic Perspective. In: ICECCS (2011)
Shi, J., Zhu, H., He, J., Fang, H., Huang, Y., Zhang, X.: ORIENTAIS: Formal Verified OSEK/VDX Real-Time Operating System. In: ICECCS (2012)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Huang, Y., Ferreira, J.F., He, G., Qin, S., He, J. (2013). Deadline Analysis of AUTOSAR OS Periodic Tasks in the Presence of Interrupts. In: Groves, L., Sun, J. (eds) Formal Methods and Software Engineering. ICFEM 2013. Lecture Notes in Computer Science, vol 8144. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-41202-8_12
Download citation
DOI: https://doi.org/10.1007/978-3-642-41202-8_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-41201-1
Online ISBN: 978-3-642-41202-8
eBook Packages: Computer ScienceComputer Science (R0)