As part of the CRAFTERS project I have been involved in applying model checking techniques to schedulability analysis problems. More specifically, modeling scheduling systems as Timed Automata and using Uppaal for model checking and statistical model checking.
All of the research is set in a context of hierarchical scheduling systems. FACS 2013 is the first paper and gives an overview of the approach. ERTS² 2014 is more abstract and deals with simulations of energy consumption on multi-core systems. TASE 2014 presents the concepts of degree of schedulability for mixed-criticality scheduling systems. This concept is given in terms of the two factors 1) Percentage of Missed Deadlines (PoMD); and 2) Degradation of the Quality of Service (DoQoS). TASE 2014 deals with schedulability of sporadic tasks under triggering patterns modeled as continuous distributions. CBSE 2015 goes more into detail with the same context as TASE 2014. ISORC 2015 revisits sporadic tasks but with discretely sampled probabilities. ICAASE 2014 applies some of our techniques to an avionics case study. FACS 2014 analyses two techniques for achieving better resource utilization in a scheduling component. Most recently we have published two journal papers: Science of Computer Programming (2015) which is a extended version of the FACS 2013 paper and Science of Computer Programming (2016) which is an extended version of FACS 2014.
The work has been created in particular close cooperation with Jalil Boudjadar and Jin Hyun Kim. The cooperation has also involved Kim G. Larsen, Arne Skou, Marius Mickučionis, Alexandre David.
- FACS 2013: Hierarchical Scheduling Framework Based on Compositional Analysis Using Uppaal (.pdf) (bibtex)
- ERTS² 2014: Schedulability and Energy Efficiency for Multi-core Hierarchical Scheduling Systems (.pdf) (bibtex)
- TASE 2014: Degree of Schedulability of Mixed-Criticality Real-time Systems with Probabilistic Sporadic Tasks (.pdf) (bibtex)
- ICAASE 2014: Compositional Schedulability Analysis of An Avionics System Using UPPAAL (.pdf) (bibtex)
- FACS 2014: Widening the Schedulability Hierarchical Scheduling Systems. (.pdf) (bibtex)
- SCP (journal) 2015: A reconfigurable framework for compositional schedulability and power analysis of hierarchical scheduling systems with frequency scaling (.pdf) (bibtex)
- SCP (journal) 2016: Statistical and exact schedulability analysis of hierarchical scheduling systems (.pdf) (bibtex)
The two latest papers which where written in cooperation with Insup Lee and Linh Thi Xuan Phan:
- ISORC 2015: Flexible Framework for Statistical Schedulability Analysis of Probabilistic Sporadic Tasks (.pdf) (bibtex)
- CBSE 2015: Quantitative Schedulability Analysis of Continuous Probability Tasks in a Hierarchical Context (.pdf) (bibtex)
Related research with a process algebra based approach: PACoR
Comments are closed.