A Parameterized Formal Model for the Analysis of Preemption-Threshold Scheduling in Real-Time Systems

Résumé

Time-Critical systems are both complex and critical. Therefore, thorough verification processes of such systems must be performed, including behavior and timing correctness. These systems are usually designed as a set of several interacting tasks and sharing one or more processors. Several scheduling policies have been proposed to manage the dispatch of these tasks for these shared resources so as to respect their predefined deadlines. In this context, preemption threshold scheduling algorithms have been proposed to improve real-time schedulability by managing preemptiveness of tasks. The advantage of these algorithms highly depends on a proper assignment of a set of scheduling attributes, which are priority and preemption threshold. In this paper, we propose a high-level parameterized formal model for the description, analysis and comparison of preemptive, non-preemptive and threshold-based scheduling policies. This model allows to formally verify a set of timing-constraints, in particular schedulability analysis as well as to provide a set of experimental results based on real-time executions. A stochastic version of our model is also proposed allowing to define probabilistic features and to model stochastic real-time tasks, scheduling mechanisms or energy consumption.

Citer ce document

Accès au document

Ce document est hébergé sur son dépôt institutionnel d'origine.

Auteur(s)

Statistiques

Consultations : 1

Téléchargements : 0