Schedulability of Herschel-Planck Revisited Using Statistical Model Checking

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

35 Citations (Scopus)

Abstract

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 disproving 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.
Original languageEnglish
Title of host publicationLeveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies : 5th International Symposium, ISoLA 2012, Heraklion, Crete, Greece, October 15-18, 2012, Proceedings, Part II
EditorsTiziana Margaria, Bernhard Steffen
Number of pages15
PublisherSpringer
Publication date18 Oct 2012
Pages293-307
ISBN (Print)978-3-642-34031-4
ISBN (Electronic)978-3-642-34032-1
DOIs
Publication statusPublished - 18 Oct 2012
EventLeveraging Applications of Formal Methods, Verification and Validation: Applications and Case Studies - Amirandes Hotel, Heraclion, Crete, Greece
Duration: 14 Oct 201219 Oct 2012

Conference

ConferenceLeveraging Applications of Formal Methods, Verification and Validation
LocationAmirandes Hotel
Country/TerritoryGreece
CityHeraclion, Crete
Period14/10/201219/10/2012
SeriesLecture Notes in Computer Science
Volume7610
ISSN0302-9743

Keywords

  • schedulability analysis
  • statistical model checking
  • timed automata
  • UPPAAL

Fingerprint

Dive into the research topics of 'Schedulability of Herschel-Planck Revisited Using Statistical Model Checking'. Together they form a unique fingerprint.

Cite this