STR - Systèmes Temps Réels

L'équipe STR développe des méthodes, techniques et outils pour la conception, la vérification et la réalisation de systèmes informatiques temps réel et en particulier dans le domaine de l’embarqué critique.

Responsable : Didier Lime
Pôle(s) de recherche :
SLS
CCS

Regroupant des chercheurs de l'Université de Nantes, de l'École Centrale de Nantes et du CNRS, l'équipe STR se positionne sur l'ensemble du cycle de développement des systèmes temps réel, et principalement de leur aspect logiciel. Elle développe ainsi des travaux originaux alliant méthodes formelles, sûreté de fonctionnement, plateformes d'exécutions, et ordonnancement temps réel. Ces travaux sont en grande majorité mis-en-œuvre en pratique dans des logiciels disponibles librement sur http://www.rts-software.org

 

Thématiques
Supports d’exécution
Systèmes d'exploitation temps réel

L'équipe Système Temps-Réel développe Trampoline, un système d'exploitation temps-réel compatible OSEK/VDX et AUTOSAR 4 distribué sous licence libre. Le développement de Trampoline a démarré en 2005 et a été soutenu par deux FUI : O4A Pilote et O4AII. Le développement de Trampoline a été entrepris pour satisfaire deux objectifs :

disposer d'un système d'exploitation qui soit à la fois libre et compatible avec une norme employée dans l'industrie. À ce titre, Trampoline est utilisé pour l'enseignement et est utilisé industriellement par la société See4sys Technologie et fait partie de l'offre de logiciels de base AUTOSAR de Dassault Systems.

disposer d'un support permettant le prototypage des travaux de recherche.

Trampoline est exploité dans deux ANR : Respected et ImpRo.

TRAMPOLINE : http://trampoline.rts-software.org

Mémoires transactionnelles

Les mémoires transactionnelles apparaissent aujourd'hui comme une solution prometteuse pour gérer les accès concurrents aux variables partagées sur des plate-formes d'exécution multicoeur. Contrairement aux approches à base de verrouillage (ex : sémaphores, spinlocks, etc.) qui, du fait des attentes liées aux verrous, ré-introduisent de la séquentialité d'exécution dans l'application, les mécanismes à base de mémoire transactionnelle permettent d'exploiter au maximum les capacités d'exécution parallèle des plate-formes multicoeur.

Dans ce contexte, nous nous intéressons à :

la conception et l'analyse de protocoles non bloquants à base de mémoire transactionnelle adaptés aux systèmes temps réel dur (garanties de progression de type wait-free) ;
STM-HRT : http://stmhrt.rts-software.org

la mise en oeuvre de tels protocoles au sein d’un système d’exploitation temps réel.
TRAMPOLINE : http://trampoline.rts-software.org

la proposition d'une méthodologie de vérification formelle de la validité fonctionnelle de ces protocoles par des approches de model-checking.

 


Ordonnancement
Ordonnancement Multiprocesseurs

Les architectures matérielles multiprocesseur et notamment multicoeur sont maintenant de plus en plus déployées au sein des systèmes temps réel embarqués. Le problème de l’ordonnancement des différentes tâches applicatives se complique alors puisqu’à l’allocation temporelle des ressources d’exécution, doivent s’ajouter des règles pour leur allocation spatiale, le tout dans la garantie du respect des contraintes temporelles d’exécution. Depuis plus d’une dizaine d’années, cette problématique suscite un fort intérêt de la part de la communauté scientifique de l’ordonnancement temps réel et de nombreuses techniques ont été proposées (ordonnancement partitionné, ordonnancement global, ordonnancement hybride ou semi-partitionné). Parmi celles-ci et les plus récentes, se distinguent des stratégies optimales en ce sens qu’elles permettent théoriquement une utilisation totale des ressources matérielles (ordonnancement mettant en avant à différents degrés la propriété de « fairness »). Toutefois cette optimalité est généralement obtenue au prix d’algorithmes peu performants, donnant lieu à de nombreux réordonnancements, préemptions et migrations de tâche. Or l’impact de ceux-ci est indéniable sur les prochaines architectures matérielles multiprocesseur/multicoeur pour l’embarqué affichant une hiérarchie mémoire de deux voire trois niveaux de cache, avec des coûts d’utilisation différents.

Dans ce contexte, nos centres d'intérêt relèvent de :

l’évaluation et la comparaison des performances de ces politiques variées. Pour cela, nous nous appuyons sur notre plate-forme logicielle de simulation de politique d'ordonnancement temps réel multiprocesseur appelée STORM "Simulation TOol for Real-time Multiprocessor scheduling". De par son ouverture, il y est aisé d’étendre ses bibliothèques, en particulier celle déjà bien riche de ses politiques d’ordonnancement.
STORM : http://storm.rts-software.org

l’amélioration de politiques d’ordonnancement global optimales de sorte à en maîtriser la surcharge (contrôler le nombre de ré-ordonnancements, préemptions et migrations) sans en affecter l’optimalité ;

la proposition de nouvelles heuristiques de partitionnement basées sur le fractionnement de tâches (« task splitting » en anglais) permettant d'atteindre des taux d'utilisation du système proches de ceux offerts par des approches semi-partitionnées, sans induire de coûts de migration ;

la définition de politique(s) d’ordonnancement « conduite(s) par les caches » dont les règles intègrent directement le surcoût temporel lié à la gestion des caches induite par les décisions d’ordonnancement ;

la mise en oeuvre de telles politiques au sein d’un système d’exploitation temps réel.

TRAMPOLINE : http://trampoline.rtssoftware.org

 

Ordonnancement et Autonomie Énergétique

Dans les capteurs intelligents sans fil, on constate que les contraintes temporelles sont de plus en plus souvent associées à des contraintes énergétiques. Les interventions humaines sont aussi limitées voire interdites parce que ces systèmes sont soit inaccessibles soit déployés en trop grand nombre ou en environnement hostile. Ils fonctionnent avec des batteries ou/et des super-condensateurs qui se rechargent continûment grâce à une source d’énergie renouvelable, par exemple l’énergie solaire, l’énergie piézo-électrique,… Concevoir de tels systèmes embarqués, entièrement autonomes, nécessite la résolution de problèmes multidisciplinaires liés à la récolte de l’énergie ambiante, son stockage et son utilisation, de façon à assurer une autonomie d’une à une dizaine d’années et ce, tout en maintenant un niveau de performance acceptable au système de traitement temps réel.

La problématique que nous traitons en particulier concerne la recherche et la validation de mécanismes dédiés au système d’exploitation, en charge d’adapter au mieux l’activité du (ou des) processeur au profil de la source d’énergie ambiante pour garantir ce qu’il est convenu d’appeler la « neutralité énergétique ».

Pour les applications temps réel dites à contraintes strictes, il s’agit de déterminer les conditions portant sur la taille minimale du réservoir d’énergie qui garantira à la fois la neutralité énergétique et le respect des contraintes temporelles exprimées en termes d’échéances. Cela suppose aussi de concevoir des mécanismes d’ordonnancement et de gestion dynamique de puissance tenant compte dynamiquement de l’énergie consommée ainsi que de l’énergie produite.

En ce qui concerne les applications dites à contraintes fermes, l’ordonnancement des tâches devra permettre d’optimiser un critère de Qualité de Service, ici le ratio d’échéances satisfaites, lorsque l’énergie disponible s’avère insuffisante pour satisfaire la totalité des contraintes temporelles sur toute la durée de vie de l’application.

 


Méthodes formelles

Les membres du thème méthodes formelles s’intéressent à la modélisation rigoureuse (mathématique) des systèmes, à la vérification automatique ou semi-automatique de leur correction, et à la synthèse de systèmes corrects par construction.

En particulier, pour les systèmes dans lesquels le temps doit être pris en compte explicitement, des formalismes comme les réseaux de Petri temporels ou les automates temporisés sont utilisés.

Parmi les thèmes récents étudiés figurent les systèmes temporisés répartis et l’exploitation de la concurrence, ainsi que les systèmes temporisés paramétrés. Ces derniers permettent de modéliser un système en laissant certaines grandeurs temporelles (délai de transmission, période d’activation, etc.) non spécifiées et c’est le processus de vérification qui déterminera l’ensemble des valeurs possibles permettant de satisfaire les propriétés désirées.

Un outil, appelé Roméo, permet la mise en oeuvre des techniques développées dans le cadre des travaux effectués sur le thème méthodes formelles.

Roméo permet notamment la modélisation de systèmes à travers un langage proche des réseaux de Petri temporisés, l’utilisation de paramètres temporels, la modélisation de préemptions, et la vérification de propriétés exprimées dans une logique temporelle temporisée et paramétrée.

Roméo est utilisé de façon pédagogique pour plusieurs cours de niveau master 2 mais aussi dans le cadre de collaborations industrielles :

Sodius: vérification d’un langage de spécification de haut-niveau (EFFBD)
BA Systèmes : routage d'AGV
Dassault Aviation