< Retour au sommaire

Proven implementation of multiprocessor real-time scheduling policies

Khaoula Boukir le

Lieu: https://rdv5.rendez-vous.renater.fr/semainaire-lsl

Keywords: Real-time scheduling policy, Real-time operating system, Scheduler implementation, Model-checking

Implementing a new scheduling policy within a real-time operating system is not an easy task. Moving from an abstract literary specification of a policy to its implementation within a real platform requires making choices of realization and considering various constraints inherent to the latter. Consequently, a scheduler implementation work shall imperatively be supported by a verification study allowing to bring a level of confidence by validating the conformity of the behavior of the implemented scheduler compared to its original specification.

In this seminar, I present my previous thesis work in which I used of formal methods for the verification of real-time scheduler implementations. I proposed a “model-checking” approach, which I conducted on global scheduler implementations carried out on Trampoline, a real-time operating system compli- ant with OSEK/VDX and AUTOSAR standards. For each implementation, a model describing its behavior is elaborated with finite state and timed machines. This model is stimulated by generators producing indeterministic scenarios of scheduling events in order to observe the reaction of the implementation under various situations. The verification is then conducted by examining the satisfaction of a set of specified requirements according to the expected behavior of the implementation as stipulated in the literature.

This approach allowed the verification of the functional correction of the behavior of two implementations of global schedulers in Trampoline: G-EDF and EDF-US. However, its modular and generic character allows to consider its use for other policies and in other operating systems.