2012 | OriginalPaper | Buchkapitel
Schedulability of Herschel-Planck Revisited Using Statistical Model Checking
verfasst von : Alexandre David, Kim Guldstrand Larsen, Axel Legay, Marius Mikučionis
Erschienen in: Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Schedulability analysis is a main concern for several embedded applications due to their safety-critical nature. The classical method of response time analysis provides an efficient technique used in industrial practice. However, the method is based on conservative assumptions related to execution and blocking times of tasks. Consequently, the method may falsely declare deadline violations that will never occur during execution. This paper is a continuation of previous work of the authors in applying extended timed automata model checking (using the tool UPPAAL) to obtain more exact schedulability analysis, here in the presence of non-deterministic computation times of tasks given by intervals [BCET,WCET]. Considering computation
intervals
makes the schedulability of the resulting task model undecidable. Our contribution is to propose a combination of model checking techniques to obtain some guarantee on the (un)schedulability of the model even in the presence of undecidability.
Two methods are considered: symbolic model checking and statistical model checking. Symbolic model checking allows to conclude schedulability – i.e. absence of deadline violations – for varying sizes of BCET. However, the symbolic model checking technique is over-approximating for the considered task model and can therefore not be used for
dis
proving schedulability. As a remedy, we show how statistical model checking may be used to generate concrete counter examples witnessing non-schedulability. In addition, we apply statistical model checking to obtain more informative performance analysis – e.g. expected response times – when the system
is
schedulable.
The methods are demonstrated on a complex satellite software system yielding new insights useful for the company.