Supports d’exécution

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

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 proposition d'une méthodologie de vérification formelle de la validité fonctionnelle de ces protocoles par des approches de model-checking.

Ordonnancement

L’adoption massive des architectures matérielles multiprocesseurs/multicoeurs pour les plates-formes d’exécution des systèmes temps réel embarqués nous a engagés, depuis plusieurs années, à nous intéresser à l’ordonnancement temps réel multiprocesseur. Après avoir mené diverses études d’évaluation et de comparaison de ses nombreuses politiques d’ordonnancement par une approche par simulation, nos recherches se sont orientées vers le problème de leur mise en œuvre au sein d’un système d’exploitation temps réel, à savoir Trampoline (le système d’exploitation temps réel développé par notre équipe). Outre l’étude de la faisabilité d’implémentation de nouvelles politiques d’ordonnancement multiprocesseur dans Trampoline, l’objectif fixé est aussi de l’accompagner d’un travail de vérification formelle permettant de garantir la correction tant fonctionnelle que temporelle des ordonnanceurs implémentés.

Pour commencer, l’implémentation des politiques d’ordonnancement global G-EDF et EDF-US a été réalisée, la première reposant sur des priorités fixes pour les travaux tandis que la seconde mixe priorités fixes pour les tâches et fixes pour les travaux. Pour chacune d’entre elles, la modélisation formelle construite à partir du code source de Trampoline à l’aide d’automates temporisés a été étendue aux composants liés à l’ordonnancement. Un ensemble d’exigences comportementales à satisfaire par chacun d’entre eux a été spécifié et conduit à l’élaboration de modèles d’observateurs. Des tests d’accessibilité de certains de leurs états permettent enfin de statuer sur le respect des exigences et plus généralement, la correction de la politique d’ordonnancement considérée.

Cette démarche qui se veut la plus générique et la plus sûre possible réclame maintenant d’être éprouvée plus largement, notamment vis-à-vis de l’implémentation de politiques d’ordonnancement plus élaborées, notamment celles qui visent l’optimalité.

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, est la cible principale pour la mise en oeuvre des techniques développées dans le cadre du 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, Dassault aviation, Thales Research, Huawei).

Protocoles et réseaux de l’Internet des Objets

L’Internet des Objets regroupe un ensemble conséquent de protocoles de réseau sans fil aux portées variables allant du périmètre personnel (WPAN) à la longue portée basse consommation (LPWAN) permettant d’adresser un grand nombre de cas d’usage. Dans l’équipe, nous nous intéressons à cet ensemble technologique en questionnant les notions d’interopérabilité, de consommation d’énergie, de compatibilité au protocole Internet (au travers notamment de l’initiative SCHC à l’IETF), de sécurité et d’adéquation algorithmes-architectures matérielles. Les cas d’usage du moment concernent notamment les réseaux de capteurs au sein d’un micro-centre de données pour optimiser le système refroidissement et valoriser la chaleur produite ou encore l’aide à l’adaptation des populations subsahariennes au changement climatique. L’Internet des Objets concerne aussi pour nous des objets sous-marins (Internet of Underwater Things, IoUT) avec des applications dans le génie océanique ou la surveillance maritime d’éco-systèmes. Il s’agit pour cet axe de recherche de concevoir des protocoles niveau 2 ou niveau 3 (et au-delà) adaptés aux communications acoustiques qui sont largement utilisées dans le contexte sous-marin. L’adaptation de systèmes embarqués existants est aussi dans les prérogatives du thème pour vérifier in situ les mécanismes proposés lors de campagnes d’expérimentations en mer. Le thème compte de nombreuses collaborations académiques et industrielles, nationales et internationales.

contact : Benoît Parrein, Maître de Conférences, Nantes Université : benoit.parrein@ls2n.fr