Model-based Schedulability Analysis

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.

The two latest papers which where written in cooperation with Insup Lee and Linh Thi Xuan Phan:

Related research with a process algebra based approach: PACoR


Comments are closed.