Vérification et Ordonnancement temps réel sous contrainte d'énergie
La presentationLes automates temporisés sont des automates finis munis d'un ensemble d'horloges à valeur réelles qui croissent uniformément dans le temps. Ces horloges permettent de mesurer le temps écoulé dans un état et de contraindre les prises de transition entre états. Ce modèle est donc un automate à espace d'états infini qui permet de modéliser facilement les systèmes temps réel. L'utilisation des automates temporisé et du model checking pour la résolution de problèmes d'ordonnancement a été largement étudiée. Récemment, une nouvelle problématique autour des automates temporisés a été proposée: "le problème d'accessibilité sous contraintes d'énergie". Le but est de montrer si il existe une trace d'exécution dans l'automate qui maintienne positives la valeur d'un ensemble de variables. Dans cet exposé, je commencerai par une présentation de la problématique d'accessibilité sous contraintes d'énergie, puis je montrerai le parallèle avec le problème d'ordonnancement sous contraintes d'énergie. Enfin, je définirai un problème spécifique d'ordonnancement temps réel sous contrainte d'énergie et proposerai une approche basée sur le model checking temporisé pour le résoudre.
Contact
Yasmina Abdeddaïm est enseignant-chercheur au département Systèmes Embarqués d'ESIEE Paris. Son travail de recherche porte sur la vérification et les automates temporisés, et elle s'intéresse particulièrement à l'utilisation de ces outils pour l'ordonnancement temps réel.
 | ABDEDDAÏM YasminaOffice: 4254 ESIEE ParisTel: +33 45 92 65 91 www: Email: encrypted |
Département Systèmes Embarqués
ESIEE Paris
Cité Descartes - BP 99
93162 Noisy-le-Grand Cedex