Widening the Schedulability Hierarchical Scheduling Systems

Jalil Boudjadar*, Alexandre David, Jin Hyun Kim, Kim Guldstrand Larsen, Marius Mikučionis, Ulrik Nyman, Arne Skou

*Corresponding author for this work

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

11 Citations (Scopus)
326 Downloads (Pure)


This paper presents a compositional approach for schedulability analysis of hierarchical systems, which enables to prove more systems schedulable by having richer and more detailed scheduling models. We use a lightweight method (statistical model checking) for design exploration, easily assuring high confidence in the correctness of the model. A satisfactory design can be proved schedulable using the computation costly method (symbolic model checking). In order to analyze a hierarchical scheduling system compositionally, we introduce the notion of a stochastic supplier modeling the supply of resources in each component. We specifically investigate two different techniques to widen the set of provably schedulable systems: 1) a new supplier model; 2) restricting the potential task offsets. We also provide a way to estimate the minimum resource supply (budget) that a component is required to provide.
Original languageEnglish
Title of host publicationFormal Aspects of Component Software : 11th International Symposium, FACS 2014, Bertinoro, Italy, September 10-12, 2014, Revised Selected Papers
EditorsIvan Lanese, Eric Madelaine
Number of pages18
Publication date2015
ISBN (Print)978-3-319-15316-2
ISBN (Electronic)978-3-319-15317-9
Publication statusPublished - 2015
EventThe 11th International Symposium on Formal Aspects of Component Software - http://www.ceub.it/, Bertinoro, Italy
Duration: 10 Sept 201412 Sept 2014
Conference number: 11


ConferenceThe 11th International Symposium on Formal Aspects of Component Software
SeriesLecture Notes in Computer Science


Dive into the research topics of 'Widening the Schedulability Hierarchical Scheduling Systems'. Together they form a unique fingerprint.

Cite this