| English home page | Page d'accueil | Participants | Comptes-rendu | Résultats |
Contraintes pour le logiciel embarqué
Le logiciel embarqué prend une part croissante dans la gestion de nombreux systèmes en contrôlant de plus en plus leur fonctionnement de façon automatique. Présents depuis longtemps dans des applications coûteuses (spatiales, aéronautiques, militaires...) où ils prennent une importance considérable, ils apparaissent dans des domaines grand public, tel que l'assistance à la conduite automobile. Les caractéristiques principales de ces systèmes sont :
dualité contrôle/commande : ces systèmes présentent d'une part un aspect commande, lois modélisées par des équations différentielles en temps échantillonné, et d'autre part un aspect contrôle de ces lois de commande, représenté par des systèmes à événements discrets ;
temps réel critique : une défaillance du système liée au non respect de contraintes temporelles peut conduire à une catastrophe humaine, écologique ou financière ;
ressources limitées : ces logiciels sont embarqués et disposent donc d'une puissance de calcul ainsi que d'une mémoire limitées, que ce soit pour des raisons de poids, de volume, de consommation énergétique (véhicules autonomes), de durcissement aux radiations (nucléaire, spatial), ou de prix (applications grand public) ;
architecture répartie et hétérogène : ces applications sont le plus souvent réparties, d'une part pour fournir une puissance de calcul importante et d'autre part, pour rapprocher les capteurs et actionneurs de cette puissance de calcul.
La programmation synchrone [Hal93] fournit des méthodes de spécification et des outils de vérification formelle qui apportent des réponses intéressantes aux besoins ci-dessus constatés. Ces méthodes sont basées : sur la modélisation des systèmes à base d'automates, sur leur spécification à l'aide de langages de haut niveau formellement définis, et enfin sur l'analyse théorique de ces modèles en vue d'obtenir des méthodes de preuve formelle.
Cependant, les aspects suivants, très importants vu les domaines d'application, ne sont pas pris en compte par la programmation synchrone :
La répartition : les langages synchrones sont certes des langages parallèles, mais ce parallélisme d'expression sert uniquement à faciliter la tâche du concepteur et n'est a priori pas lié au parallélisme d'exécution (celui du système). Ainsi, les compilateurs des langages synchrones produisent du code centralisé. Ceci permet de faire la mise au point du programme en termes de valeurs numériques, de la vérification formelle en termes d'ordre sur les événements qui entrent et sortent du système, ainsi que diverses optimisations. Afin d'obtenir un code final réparti optimisé minimisant le matériel, on peut utiliser la méthodologie "Adéquation Algorithme/Architecture" [Sor94] développée à Rocquencourt dans le projet Sosso qui conserve les propriétés montrées avec les langages synchrones.
La tolérance aux pannes : un système embarqué étant par nature critique, il est essentiel d'assurer que son programme de contrôle/commande est tolérant aux pannes. Cela peut même être une motivation pour la répartition de ce programme. Dans ce cas, au minimum la perte d'un site ne doit pas provoquer la perte de l'ensemble de l'application (dégradation douce).
La conformité de la mise en oeuvre à la spécification : outre la vérification formelle de propriétés de sûreté sur l'application (que les langages synchrones permettent au niveau du modèle du programme), il faut également s'assurer que la spécification du système est complète et correcte. C'est un problème rendu encore plus ardu par les contraintes de répartition et de tolérance aux pannes.
En résumé, les langages synchrones permettent de programmer les systèmes embarqués en offrant plusieurs avantages : prise en compte des contraintes temporelles, vérification formelle, programmation élégante et sûre grâce à l'hypothèse de synchronisme. Les techniques modernes de répartition permettent ensuite de produire automatiquement du code réparti. Mais la tolérance aux pannes du programme réparti final n'est pas assurée. C'est ce point délicat et important que nous nous proposons de traiter dans le cadre d'une collaboration entre les projets Bip et Sosso.
Présentation des logiciels impliqués
Les approches et méthodologies considérées plus haut reposent sur des logiciels qui sont des supports concrets permettant de réaliser des systèmes critiques embarqués avec des temps de développement et un niveau de sûreté de conception raisonnables.
L'environnement Orccad [SECK93] (pour Open Robot Controller CAD) est un logiciel de haut niveau dont l'expressivité est bien adaptée à la spécification d'applications robotiques combinant l'aspect contrôle et l'aspect commande. Il est développé conjointement par les projets Icare à Sophia-Antipolis et Bip à Grenoble, ainsi que les moyens robotiques de Grenoble. Dans Orccad, une action élémentaire est modélisée par une Tâche-Robot (TR), qui est une loi de commande encapsulée dans un comportement logique réactif. Les TRs constituent l'interface entre les aspects temps continu (en fait discrétisé) et événements discrets. Les lois de commande sont réalisées par l'assemblage de modules constituant un graphe flot de données. Le comportement local est quant à lui codé en Esterel [BG92]. Ces actions élémentaires sont ensuite composées en Procédures-Robot (PR) de complexité croissante jusqu'à l'application complète. Le programme des PRs, également codé en Esterel, décrit le comportement nominal de la mission ainsi que tous les traitements d'exception prédéfinis. L'utilisation d'Esterel pour la spécification de tous les aspects logiques de l'application permet de bénéficier de l'environnement de preuve formelle (FC2Tools et Xeve) associé. Un prototype de laboratoire est en cours d'intégration. Enfin le code généré est pour l'instant mono-processeur, les systèmes cibles étant VxWorks et Solaris.
L'environnement SynDEx [Sor94] (pour Synchronized Distributed Executive), développé par le projet Sosso à Rocquencourt, est un logiciel d'aide à l'implantation multi-composants d'applications spécifiées à l'aide de langages synchrones. Il supporte la méthodologie « Adéquation Algorithme/Architecture ». SynDEx prend en compte les contraintes de temps réel et d'embarquabilité qui doivent être satisfaites par l'application. L'algorithme de commande ou de traitement de signal et des images est donné sous la forme d'un graphe flot de données conditionné, provenant par exemple de la compilation d'un programme écrit avec les langages synchrones, selon le format DC. L'architecture cible est également décrite avec un graphe sous forme de composants programmables et/ou de circuits spécialisés reliés par des média de communication. Des heuristiques rapides permettent d'effectuer automatiquement une distribution et un ordonnancement principalement statique des tâches sur l'architecture matérielle, éventuellement hétérogène, en optimisant la durée d'exécution globale de l'algorithme et en construisant l'exécutif temps réel réparti minimal nécessaire à l'implantation du programme. Il permet également d'optimiser l'architecture cible.
Axes de travail
Pour les quatre axes, nous avons indiqué les personnes plus particulièrement impliquées :
Maîtriser les aspects contrôle/commande (Sorel et Simon). Dans de nombreux systèmes informatiques, et en particulier les systèmes embarqués servant à contrôler un processus physique, l'activité du ou des calculateurs de bord est partagée entre une activité calculatoire généralement périodique (calcul d'une loi de commande) et une activité de type contrôle (changement de mode de marche, traitement d'exception ...) relevant de la problématique des systèmes à événements discrets et des systèmes réactifs. La sûreté de conception reposant notamment sur la possibilité d'effectuer des vérifications formelles des programmes, elle nécessite une coopération de ces deux aspects et une modélisation rigoureuse globale de leur comportement. Bien que complémentaires ils sont néanmoins actuellement traités de manière séparée dans le domaine de la robotique. Il serait intéressant de rapprocher les deux points de vue sous un modèle unifié. Un certain nombre de problèmes doivent être étudiés attentivement, en particulier :
modélisation de la coopération contrôle/commande à l'aide d'un modèle de graphes unifié flot de donnée/flot de contrôle avec prise en compte des contraintes temps-réel multiples (plusieurs contraintes de latence et de cadence),
préemption et enchaînement d'actions multi-tâches dans un contexte temps-réel réparti,
utilité du format DC des langages synchrones comme modèle commun.
Proposer des solutions pour rendre le code réparti tolérant aux pannes (Sorel et Girault). Cela concerne deux aspects : d'une part la prise en compte des défaillances au niveau des algorithmes en effectuant des changements de modes de plus en plus dégradés, et d'autre part au niveau de l'architecture en prévoyant de la redondance matérielle et/ou logicielle avec vote pour les processeurs et les médias de communication, ou encore l'utilisation de composants matériels spécifiques pour implanter les parties les plus critiques du logiciel. Par exemple, pour éviter que le blocage d'un noeud de l'application répartie ne provoque le blocage de l'application entière, on peut imaginer un sous-réseau de communication dédié aux détections de défaillances et chargé de faire basculer l'application vers un mode dégradé. Il faut également garder à l'esprit les impératifs de performance qui doivent se dégrader le moins possible.
Proposer des solutions pour assurer que la spécification du problème est complète (Simon et Girault). Dans l'état actuel d'Orccad, les divers traitements d'exception sont directement programmés en langage synchrone (Esterel), cette phase de spécification et de codage étant suivie d'une phase de vérification formelle à l'aide de FC2Tools et Xeve. Si certaines propriétés génériques sont automatiquement vérifiées grâce aux structures du système, les propriétés spécifiques à une application donnée sont vérifiées manuellement, avec tous les risques d'oubli que cela comporte. La prise en compte de contraintes de répartition et de tolérance aux pannes va encore amplifier ce risque. Une alternative consiste à synthétiser le contrôle à partir de contraintes exprimées de façon aussi symbolique que possible. Il nous semble que des techniques de synthèse de contrôleur dérivant des théories de Ramadge et Wonham [RW87] peuvent avantageusement être appliquées au contexte particulier d'Orccad.
Coupler Orccad et SynDEx (Sorel, Simon et Girault). Le but est de proposer un environnement logiciel unique cohérent depuis la spécification du système, prenant en compte les aspects tolérance aux pannes aussi bien au niveau logiciel que matériel, jusqu'à l'implantation optimisée fonctionnant en temps réel. Il s'agit d'étudier les possibilités d'unifier leurs sémantiques respectives en fonction des modèles vus ci-dessus avec comme intermédiaire le format DC auquel le compilateur Esterel s'interface, et qui est accepté comme spécification d'algorithme par SynDEx.
Domaines d'application
Les deux projets sont actuellement impliqués dans les applications suivantes :
Robotique sous-marine : le contrôle-commande d'un système d'intervention sous-marine est caractérisé par la présence de nombreux degrés de libertés et de capteurs et par l'enchaînement de nombreux modes de marche. Le système est naturellement réparti (fond/surface), l'une des principales contraintes de tolérance aux pannes étant qu'une perte de liaison (partielle ou totale) entre la surface et le fond ne doit pas entraîner la perte du système immergé. La spécification même du problème est délicate.
Véhicules semi-automomes : il faut par exemple que la panne d'un des contrôleurs de roue soit détectée par les autres contrôleurs et le contrôleur central et entraîne l'arrêt d'urgence du véhicule.
D'autres applications principalement dans le domaine des transports, automobile grand public, ferroviaire et aérien sont envisageables.
Points forts de l'action incitative TOLÈRE
Le problème du code réparti automatiquement et tolérant aux pannes pose un réel challenge scientifique.
Le problème de la synthèse du contrôle dans les systèmes à événements discrets reste lui aussi largement ouvert et difficile.
Projet Bip : Alain Girault (04 76 61 53 51), Daniel Simon (04 76 61 53 28), Eric Rutten (04 76 61 54 02) et Catalin Dima.
Projet Sosso : Yves Sorel (01 39 63 52 60) et Christophe Lavarenne (01 39 63 55 80).
[BG92] G. Berry and G. Gonthier. The Esterel synchronous programming language: Design, semantics, implementation. Science of Computer Programming, 19(2):87-152, 1992.
[Hal93] N. Halbwachs. Synchronous programming of reactive systems. Kluwer Academic Pub., 1993.
[RW87] P.J. Ramadge and W.M. Wonham. Supervisory control of a class of discrete event processes. SIAM Journal on Control and Optimization, 25(1):206-230, janvier 1987.
[SECK93] D. Simon, B. Espiau, E. Castillo, and K. Kapellos. Computer-aided design of a generic robot controller handling reactivity and real-time control issues. IEEE Transactions on Control Systems Technology, 1(4), décembre 1993.
[Sor94] Y. Sorel. Massively parallel computing systems with real-time constraints, the "algorithm/architecture adequation" methodology. In Massively Parallel Computing Systems Conference, Ischia, Italy, mai 1994.
Le projet Solidor de l'Irisa travaille également sur la tolérance aux pannes pour les systèmes critiques. Leur projet Hades attaque le problème sous l'angle des systèmes répartis, et est en l'occurrence bien plus avancé que notre projet Tolère.