Deadline Analysis of AUTOSAR OS Periodic Tasks in the Presence of Interrupts

Yanhong Huang, Joao Ferreira, Guanhua He, Shengchao Qin, Jifeng He

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    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.
    Original languageEnglish
    Title of host publicationFormal Methods and Software Engineering. ICFEM 2013
    EditorsL. Groves , J. Sun
    PublisherSpringer Berlin
    Pages165-181
    ISBN (Electronic)9783642412028
    ISBN (Print)9783642412011
    DOIs
    Publication statusPublished - 2013
    EventFormal Methods and Software Engineering - 15th International Conference on Formal Engineering Methods - Queenstown, New Zealand
    Duration: 29 Oct 20131 Nov 2013
    Conference number: 15

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer, Berlin
    Volume8144

    Conference

    ConferenceFormal Methods and Software Engineering - 15th International Conference on Formal Engineering Methods
    Abbreviated titleICFEM 2013
    CountryNew Zealand
    CityQueenstown
    Period29/10/131/11/13

    Fingerprint Dive into the research topics of 'Deadline Analysis of AUTOSAR OS Periodic Tasks in the Presence of Interrupts'. Together they form a unique fingerprint.

  • Cite this

    Huang, Y., Ferreira, J., He, G., Qin, S., & He, J. (2013). Deadline Analysis of AUTOSAR OS Periodic Tasks in the Presence of Interrupts. In L. Groves , & J. Sun (Eds.), Formal Methods and Software Engineering. ICFEM 2013 (pp. 165-181). (Lecture Notes in Computer Science; Vol. 8144). Springer Berlin. https://doi.org/10.1007/978-3-642-41202-8_12