Schedulability of Herschel revisited using statistical model checking

Alexandre David, Kim Guldstrand Larsen, Axel Legay, Marius Mikučionis

Research output: Contribution to journalJournal articleResearchpeer-review

10 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]. Computation intervals with preemptive schedulers make the schedulability analysis 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. Since the model uses stop-watches, the reachability problem becomes undecidable so we are using an over-approximation technique. We can safely conclude that the system is schedulable for varying values of BCET. For the cases where deadlines are violated, we use polyhedra to try to confirm the witnesses. Our alternative method to confirm non-schedulability uses statistical model-checking (SMC) to generate counter-examples that are always realizable. Another use of the SMC technique is to do performance analysis on schedulable configurations to obtain, e.g., expected response times. The methods are demonstrated on a complex satellite software system yielding new insights useful for the company.
Original languageEnglish
JournalInternational Journal on Software Tools for Technology Transfer
Volume17
Issue number2
Pages (from-to)187-199
Number of pages13
ISSN1433-2779
DOIs
Publication statusPublished - 2015

Keywords

  • statistical model checking
  • symbolic model checking
  • performance analysis
  • Schedulability Analysis

Fingerprint Dive into the research topics of 'Schedulability of Herschel revisited using statistical model checking'. Together they form a unique fingerprint.

Cite this