TELECOM ParisTech ETR'09

Présentations des interventions

• Jérôme Hugues et Franck Singhoff - Développement de systèmes à l'aide d'AADL - OCARINA/CHEDDAR
• Nicolas Halbwachs - Modélisation synchrone de systèmes complexes
• Jean-Paul Blanquart - Sûreté de fonctionnement des systèmes embarqués critiques : les enjeux industriels (domaine spatial)
• Laurent Fribourg - Vérification temporisée paramétrée
• François Laroussinie - Logiques temporelles et jeux concurrents temporisés
• Thierry Jéron - Génération de tests pour les systèmes réactifs et temporisés
• Iulian Ober - Modélisation UML et vérification pour systèmes temps réel
• José Ruiz - Le modèle de concurrence Ravenscar : principes et mise en oeuvre
• Pascal Gula - La sémantique d'exécution définie par AUTOSAR
• Thomas Nolte - Hierarchical scheduling of complex embedded real-time systems
• Isabelle Augé-Blum - Communications temps réel dans les WSN : protocoles MAC et routage

La complexité des systèmes embarqués temps réel nécessite un outillage complet pour pouvoir garantir que les besoins seront couverts. Le langage de modélisation AADL (Architecture Analysis and Design Language), publie dans sa version 2 en Janvier 2009 répond à un double objectif: permettre une description précise d'un système, c'est à dire non ambigüe et détaillé; permettre d'appliquer plusieurs analyses sur un modèle. Par ailleurs, il propose des mécanismes d'extension offrant la possibilité de raffiner la description au fur et à mesure que la conception du système progresse.

Dans cet exposé, nous présentons les concepts fondateurs du langage AADL, et montrons comment il répond aux besoins de modélisation et d'analyse. Au travers d'un cas d'étude, nous introduisons les blocs fondateurs de AADL, puis détaillons comment mener une analyse d'ordonnancement à l'aide de l'outil Cheddar développé à l'UBO/LISYC. une fois le modèle finalisé, nous montrons comment ajouter les blocs fonctionnels (sous programmes) attachés aux tâches du système en vue de la génération automatique du système à l'aide de l'outil Ocarina développé à Telecom ParisTech. En particulier, nous montrons comment cette étape permet de tirer partie d'une approche orientée modèle pour obtenir des analyses plus précises sur le système, en vue de raffiner le système.
Les exemples utilisés découlent de cas d'étude réalisés au cours de différents projets, dont notamment ASSERT et Flex-eWare.

 Programme |  haut

Le projet intégré européen ASSERT a concerné une méthodologie de développement d'applications embarquées, notamment dans le domaine spatial (lanceurs et satellites). Dans l'approche proposée, l'architecture matérielle et logicielle d'une application est décrite formellement au moyen d'un langage de description d'architectures (ADL), et les composants logiciels sont développés indépendemment de cette architecture. Ce développement séparé de l'architecture et du logiciel pose le problème de la validation précoce de l'application.

Nous avons proposé de résoudre ce problème en traduisant la description de l'architecture en un modèle exécutable, permettant la simulation et la validation conjointes avec le logiciel d'application. Plus spécifiquement, nous avons proposé une traduction du langage AADL (Architecture Analysis and Design Language) dans un langage synchrone tel que Scade ou Lustre. Le résultat est un modèle synchrone non déterministe, auquel les composants logiciels peuvent être intégrés, fournissant ainsi un modèle global de l'application. Les outils de simulation et de validation des programmes synchrones peuvent alors être appliqués à ce modèle. L'approche est illustrée sur une étude de cas dérivée d'une application réelle.

 Programme |  haut

L’augmentation de complexité et de criticité des systèmes, et en particulier des systèmes embarqués temps-réel, accroît les difficultés et les enjeux auxquels l’industrie doit répondre. Cet exposé donne un aperçu des enjeux industriels en termes de sûreté de fonctionnement des systèmes embarqués critiques. Nous illustrons ces enjeux dans le domaine spatial. Les principaux enjeux concernent :

• Les besoins de sûreté de fonctionnement et contraintes associées, que nous analysons pour les différents types de systèmes spatiaux et missions.
• Les processus et activités de sûreté de fonctionnement, avec les principaux enjeux que sont la formalisation et l’intégration dans un processus global d’ingénierie à base de modèles.
• Les fonctions et mécanismes de sûreté de fonctionnement (tolérance aux fautes) dont les méthodes de développement et de validation doivent s’adapter à une criticité et une complexité toujours croissantes.

 Programme |  haut

Avec le développement des réseaux des calculateurs embarqués (notamment dans l'automobile), les interactions conflictuelles et intempestives de service deviennent des sources courantes d'accident potentiel grave.
Une solution d'ingénierie classique pour harmoniser le fonctionnement global d'un système concurrent consiste à ajuster les échéances des différentes tâches accomplies par les composants pour réduire les sources de conflit, d'engorgement ou de blocage. Le réglage de ces paramètres temporels sert également à améliorer les performances et à diminuer le coût d'utilisation du système global.
Dans ce tutoriel, nous expliquerons comment le modèle des automates temporisés paramétrés peut contribuer, suivant ce principe, à la améliorer la sécurité et le rendement des réseaux des calculateurs embarqués.

 Programme |  haut

Voici quelques questions que l'on abordera dans cet exposé : Pourquoi utiliser des jeux dans le cadre de la vérification et la conception de systèmes informatiques ? À quoi peut nous servir la logique temporelle ? Qu'est-ce qu'une logique temporelle alternante ? Comment ajouter des contraintes temps-réel dans ces modèles ? Y a-t-il des algorithmes pour ces formalismes, et sont-ils efficaces ?

 Programme |  haut

L'objectif de cet exposé est d'introduire les principes du test de conformité pour les systèmes réactifs et les techniques de génération de tests correspondantes. Dans un premier temps, nous présenterons une théorie du test sur des modèles simples de systèmes de transitions ainsi que les algorithmes de génération de tests pour ces modèles basés sur une analyse de co-accessibilité. Nous évoquerons aussi l'extension de ces algorithmes à des modèles manipulant des données qui reposent alors sur une analyse approchée. Enfin, nous verrons comment étendre la théorie du test et les algorithmes de génération au modèle des automates temporisés.

 Programme |  haut

UML (Unified Modeling Language) est un langage standardisé très utilisé pour la spécification, la conception et/ou la documentation des systèmes logiciels. Il couvre différents aspects et phases du développement, allant de la spécification des exigences, à la description détaillée d'un modèle de conception, et jusqu'à la description du déploiement. Dans cet exposé nous allons aborder l'utilisation du langage UML pour la modélisation des systèmes temps réel, à travers des aspects spécifiques comme la modélisation du comportement et les différentes approches de spécification des propriétés temps-réel (profil MARTE, OMEGA, etc). Nous discuterons ensuite de la validation de propriétés fonctionnelles et non-fonctionnelles (e.g., d'ordonnancement) sur des modèles UML, par des techniques de simulation et de model checking, en considérant notamment l'exemple de la boîte à outils IFx.

 Programme |  haut

Le profil de Ravenscar est un sous-ensemble du modèle de concurrence de Ada, restreint pour assure le déterminisme, permettre l'analyse de temps de réponse et limiter l'utilisation de mémoire. Il permettre aussi l'utilisation de un système d'exécution petit et efficace. Le modèle de concurrence défini par le profil de Ravenscar est compatible avec l'utilisation des techniques et outils qui permettent la vérification statique des propriétés des programmes.
L'environnement de développement de GNAT Pro fournit un noyau d'exécution supportant le profil de Ravenscar pour des systèmes embarqués temps réel, qui a été développer pour les processeur embarqués sur les satellites de l'Agence Spatiale Européenne (ESA).
La présentation décrira le profil de Ravenscar, et fournira quelques détails de implémentation sur le système d'exécution développer pour les systèmes embarqués temps réel.

 Programme |  haut

AUTOSAR est actuellement largement intégré dans le domaine de l'industrie automobile en raison de ses nombreux avantages sur la conception traditionnelle, avantages qui incluent une normalisation de l'architecture logicielle. De plus, cette approche introduit un langage de description d'architecture, comprenant la définition d'un méta-modèle. Les éléments permettant de définir ce méta-modèle sont organisés en plusieurs catégories, l'une d'entre elles étant consacrée à la description des composants logiciels de l'application considérée. En outre, trois niveaux d'abstraction sont prévus pour chaque composant (SWC) ou module de logiciel de base (BSW) : l'interface, le comportement interne et l'implémentation.
Cet exposé présente en détails le second niveau, qui permet de définir la sémantique d'exécution des modules SWC ou BSW, ainsi que les possibilités d'ordonnancement en terme de configuration.

 Programme |  haut

 haut

Les réseaux de capteurs sans fils sont constitués de centaines (voire de milliers) de composants capables de mesurer des valeurs physiques de l'environnement, de les traiter et de communiquer via leur inteface radio. Les ressources embarquées dans un capteur (puissance de calcul, énergie) sont limitées, et les capteurs sont le plus souvant déployés de manière aléatoire sur la zone à surveiller. Dans le but d'économiser de l'énergie, les communications se font en mode ad-hoc multi-sauts, jusqu'à un noeud particulier (le puits) chargé de récolter les informations.
Dans ce contexte, et pour les applications le nécessitant, comment assurer des communications temps-réel?

Le but de ce papier est de faire un état de l'art sur les protocoles de communication de niveau MAC et routage permettant les communications temps-réel dans les réseaux de capteurs sans fils. Dans une première partie, les protocoles directement inspirés des protocoles MAC temps-réel filaires seront présentés, et nous verrons les limites de ces solutions.
Dans une seconde partie, les grandes classes de protocoles temps-réel de niveau MAC (accès aléatoire, accès contrôlé centralisé ou distribué) seront étudiées, en illustrant par un exemple dans chaque famile.
Dans une troisième partie, nous ferons de même pour les protocoles de routage, qui peuvent être basés sur des solutions hiérarchiques ou des solutions dites « à plat » (variantes du routage géographique).

Dans ces deux parties, les avantages et les limites de chacun protocole seront mis en évidence.
Enfin, en conclusion, les bonnes propriétés que doivent avoir les protocoles pour satisfaire à la fois les contraintes temporelles et les contraintes spécifiques aux réseaux de capteurs seront discutées.

 Programme |  haut