Ce travail porte sur le problème de la validation des logiciels réactifs synchrones par rapport à des propriétés de sûreté. Les propriétés de sûreté permettent de spécifier les comportements sûrs d'un logiciel. D'une manière générale, notre approche aborde la validation par le test. Dans ce cadre, nous avons défini une technique qui permet de déterminer, à partir des propriétés de sûreté seulement, toutes les données de test favorisant l'observation d'une violation de ces propriétés. Cette technique permet d'anticiper une violation future. Différentes heuristiques ont été implantées pour sélectionner les données de test de façon efficace. Notre proposition a été intégrée à l'outil Lutess. Ce dernier est capable de générer automatiquement et dynamiquement des données de test en s'appuyant sur divers guides. La capacité de nos heuristiques à guider le test vers des situations où la propriété de sûreté peut être violée a été évaluée sur une étude de cas significative proposée par un consortium d'industriels du secteur des télécommunications.

Ce travail s'inscrit dans le cadre des méthodes formelles et des outils pour la spécification, la programmation, la vérification et la validation des logiciels réactifs à l'aide du langage synchrone Lustre. Nous avons étendu l'environnement de développement actuel de ces logiciels en lui adjoignant des outils de validation de spécifications et de test de programmes. Nous proposons une technique de construction automatique d'un simulateur aléatoire de l'environnement externe du logiciel ainsi que d'un simulateur des comportements sûrs de ce dernier. Exécutés conjointement, ces deux simulateurs permettent, par observation, la validation des spécifications de l'environnement et des propriétés de sûreté. La simulation de l'environnement constitue également un moyen de test aléatoire du logiciel. Une variante de cette technique est le test des propriétés de sûreté. Ce type de test favorise l'exécution des comportements de l'environnement du logiciel qui peuvent mettre en évidence avec une plus grande probabilité des violations des propriétés de sûreté. Enfin, nous définissons des critères de couverture pour le test structurel en s'appuyant sur le réseau d'opérateurs associé à un programme Lustre. Les conditions d'exécution des composants du réseau satisfaisant les critères sont calculées automatiquement ce qui permet la génération automatique de données de test ainsi que la mesure du taux de couverture obtenu. Toutes ces techniques sont formellement définies. Une illustration de leur application sur un exemple de logiciel synchrone que nous avons développé à cet effet complète notre étude.

Cette thèse a pour cadre la vérification des systèmes réactifs de grande taille. Les systèmes réactifs sont des systèmes informatiques qui réagissent continûment à leur environnement physique, à une vitesse déterminée par cet environnement. Ils sont particulièrement utilisés dans le cadre du contrôle des systèmes critiques : transport, nucléaire, commande de processus industriels, communication... De par leur fonction, ils doivent impérativement satisfaire des contraintes strictes de fonctionnement. La vérification des systèmes réactifs de grande taille peut être effectuée en décomposant modulairement le programme. Des algorithmes de synthèse sont proposés, qui permettent de déterminer les sous-programmes les plus généraux, tels que le système complet satisfasse une propriété donnée. La vérification modulaire a été étendue aux cas des réseaux paramétrés de processus. L'utilisation d'observateurs synchrones permet de spécifier des propriétés sur un nombre quelconque de processus. La technique proposée consiste alors à exprimer un invariant de ce réseau à l'aide d'un plus petit ou d'un plus grand point fixe, et d'utiliser des techniques d'extrapolation pour en calculer une approximation régulière. Les cas des réseaux linéaires (ou en anneau) et des réseaux arborescents ont particulièrement été étudiés. L'ensemble des techniques et des algorithmes développés ont été implémentés dans un outil : a Boolean Automaton Network Grammar checker.

Esterel est un langage impératif concurrent pour la programmation des systèmes réactifs. A l'exception de l'instruction "pause", les primitives du langage s'exécutent sans consommer de temps logique. L'exécution se décompose donc en une suite d'instants. Dans ce contexte, les boucles peuvent poser deux types de problèmes: d'une part une boucle instantanée peut bloquer l'écoulement du temps; d'autre part un bloc de code peut être traversé plusieurs fois au cours du même instant, conduisant à un comportement du programme dit "schizophrène". Les boucles instantanées sont proscrites par la sémantique. Elles doivent donc être détectées par les compilateurs et les programmes correspondants doivent être rejetés. Par ailleurs, la compilation efficace des programmes schizophrènes est difficile. Ainsi, alors que plusieurs compilateurs pour Esterel sont disponibles, les algorithmes employés pour compiler les boucles ne sont ni portables, ni formellement spécifiés, et encore moins prouvés. Dans ce document, nous étudions les boucles en Esterel, établissant une correspondance formelle entre la sémantique opérationnelle du langage et l'implémentation concrète d'un compilateur. Après avoir spécifié les problèmes posés par les boucles, nous développons des techniques d'analyse statique efficaces pour les détecter dans un code Esterel quelconque. Puis, de façon à guérir la schizophrénie, c'est à dire transformer efficacement les programmes schizophrènes en programmes non schizophrènes, nous introduisons dans le langage une nouvelle primitive appelée "gotopause". Elle permet de transférer le contrôle d'un point du programme à un autre de façon non instantanée, mais sans contrainte de localité. Elle préserve le modèle de concurrence synchrone d'Esterel. Nous décrivons un premier algorithme qui, en dépliant les boucles à l'aide de cette nouvelle instruction, produit pour tout programme Esterel correct un programme non schizophrène équivalent. Enfin, en combinant analyse statique et réécriture, nous obtenons un préprocesseur qui rejette les boucles instantanées et guérit la schizophrénie, à la fois portable et très efficace. Nous l'avons implémenté. De plus, grâce à une approche formelle de bout en bout, nous avons pu prouver la correction de ce préprocesseur.

L'importance des systèmes temps-réels embarqués dans les sociétés industrialisées modernes en font un terrain d'application privilégié pour les méthodes formelles. La prépondérance des contraintes temporelles dans les spécifications de ces systèmes motive la mise au point de solutions spécifiques. Cette thèse s'intéresse à une classe de systèmes temps-réels incluant ceux développés avec la chaîne d'outils OASIS, développée au CEA LIST. Nos travaux portent sur la notion de délai de bout-en-bout, que nous proposons de modéliser comme une contrainte temporelle concernant l'influence du flot d'informations des entrées sur celui des sorties. Afin de répondre à la complexité croissante des systèmes temps-réels, nous étudions l'applicabilité de cette notion nouvelle au développement incrémental par raffinement et par composition. Le raffinement est abordé sous l'angle de la conservation de propriétés garantes de la correction du système au cours du processus de développement. Nous délimitons les conditions nécessaires et suffisantes à la conservation du délai de bout-en-bout lors d'un tel processus. De même, nous donnons des conditions suffisantes pour permettre le calcul du délai de bout-en-bout de manière compositionnelle. Combinés, ces résultats permettent d'établir un formalisme permettant la preuve du délai de bout-en-bout lors d'une démarche de développement incrémentale.

Ce document résume mon activité de recherche depuis 1991. Elle a porté sur deux thématiques connexes : la modélisation et la validation de langages métier de l'automatisme et le contrôle à distance de systèmes mécaniques sur des réseaux de communication non fiables. Le premier axe de recherche portait plus précisément sur la définition formelle des langages classiques de l'automatisme (langage à relais et Grafcet) à l'aide des formalismes synchrones tels que Signal ou Lustre. L'intérêt d'un tel travail était de pouvoir exprimer les différentes interprétations possibles d'un même programme afin de pouvoir les comparer ; les environnements développés autour des formalismes synchrones permettant alors la réalisation directe de simulateurs ainsi que l'ouverture vers des outils autorisant la validation des programmes. Dans ce dernier domaine, différentes pistes ont été étudiées avant de retenir une modélisation à l'aide d'automates temporisés permettant alors l'expression de propriétés temporelles sur les programmes modélisés. Le deuxième axe de travail avait et a pour objectif d'étudier la faisabilité de l'introduction des nouvelles technologies, et en particulier des technologies réseau, dans le contrôle supervisé de systèmes mécaniques. Le réseau est ici vu comme un réseau sans qualité de service, de type Internet, alors que l'une des préoccupations majeures des automaticiens est d'assurer une sécurité maximale. Dans un premier temps, nous avons proposé une architecture logicielle permettant la communication entre l'opérateur et le système à contrôler. Basée sur un noyau de services complété par des pilotes spécifiques aux applications cibles, elle est facilement extensible. Pour prendre en compte les aléas réseau, la méthodologie Gemma, utilisée en ingéniérie des automatismes, a été étendue afin d'intégrer des informations en provenance d'un capteur réseau. Ce dernier permet d'estimer la qualité de la connexion d'un bout à l'autre du système de communication et doit être pris en compte automatiquement, et en permanence, par le système afin d'assurer la sécurité du contrôle supervisé. Bien que différentes, ces deux thématiques se rejoignent sur de nombreux points : --- Le domaine d'application, c'est à dire le contrôle de systèmes en environnement de production industriel. D'un côté, on a cherché à assurer une meilleure qualité, de la spécification à l'implantation en passant par la vérification des applications. De l'autre en proposant l'utilisation des nouvelles technologies de communication pour améliorer la productivité globale de l'entreprise. --- L'utilisation et l'introduction des méthodes et des outils de l'informaticien auprès de la communauté des automaticiens. Dans mon premier domaine de recherche, par l'intermédiaire du monde dit "synchrone" et dans le deuxième par la mise en oeuvre des technologies autour de l'Internet. Dans les deux cas, les technologies informatiques se sont placées au service d'autres disciplines tout en essayant de faire ressortir les points difficiles et de proposer des solutions innovantes. --- Le souci permanent de construire des applications sûres et de valider, si possible de manière formelle, les résultats obtenus. Cet aspect est surtout visible dans le cadre de la première activité de recherche, mais des travaux, non encore achevés, ont également porté sur la validation de l'architecture logicielle proposée pour le contrôle à distance. Ils sont directement issus des connaissances et de l'expérience acquises dans le premier thème.

« Ce travail propose des solutions pour améliorer les environnements collaboratifs synchrones dans le cadre d'un apprentissage à distance. A travers des expériences d'activités collaboratives synchrones, un modèle a été définit pour représenter les interactions et les communications dans un groupe d'utilisateurs distribués. Ce modèle vise à supporter le développement d'un système de gestion des contenus et des communications. La représentation des flux d'informations dans un groupe d'élèves ouvre la voie au support de stratégies éducatives. D'un point de vue technique, cette représentation permet d'optimiser la qualité des communications selon des critères éducatifs. Le but de cet environnement est d'apporter une réponse équilibrée aux utilisateurs tant sur le plan technique qu'éducatif. Un tel environnement n'a pas été implémenté mais ce travail à participé à l'amélioration de l'environnement collaboratif PLATINE développé au LAAS-CNRS. »« Ce travail propose des solutions pour améliorer les environnements collaboratifs synchrones dans le cadre d'un apprentissage à distance. A travers des expériences d'activités collaboratives synchrones, un modèle a été définit pour représenter les interactions et les communications dans un groupe d'utilisateurs distribués. Ce modèle vise à supporter le développement d'un système de gestion des contenus et des communications. La représentation des flux d'informations dans un groupe d'élèves ouvre la voie au support de stratégies éducatives. D'un point de vue technique, cette représentation permet d'optimiser la qualité des communications selon des critères éducatifs. Le but de cet environnement est d'apporter une réponse équilibrée aux utilisateurs tant sur le plan technique qu'éducatif. Un tel environnement n'a pas été implémenté mais ce travail à participé à l'amélioration de l'environnement collaboratif PLATINE développé au LAAS-CNRS. » null null null

Reproduction de : Thèse de doctorat : Génie électrique : Lille 1 : 2006. / N° d'ordre (Lille 1) : 3913. Titre provenant de la page de titre du document numérisé. Bibliogr. p. 127-134.

polyentrefers (ou fractionnées) synchrones à bobinage global permettant la maximisation du couple ou de l'effort volumique. Le concept de machine polyentrefer est plus précisément appliqué à l'élaboration d'actionneurs linéaires multi-tiges, nouvelle architecture bien adaptée aux entraînements directs. Tout d'abord, une classification des différents actionneurs électromagnétiques permet de situer la place particulière occupée par les actionneurs polyentrefers, notamment ceux à bobinages globaux. Ensuite, une étude, basée sur des optimisations des paramètres géométriques, permet de mettre en évidence l'intérêt de ce type de topologie pour l'obtention de forces spécifiques et de dynamiques mécaniques très élevées. Une analyse aux lois de similitude, régissant les performances de ces actionneurs, est ensuite menée pour dégager leurs caractéristiques fondamentales. Puis, une étude des comportements mécaniques, prenant en compte, entre autres, les tolérances mécaniques (montage) et les efforts normaux (guidage), est ensuite effectuée. Ainsi, la possibilité de filtrer les ondulations d'efforts et de diminuer les forces parasites (composante normale) sans affecter l'effort utile est montrée. Cette approche aboutit à la structure multi-tiges. Enfin, un prototype est testé et permet de valider la faisabilité de cette technologie, ainsi que la justesse des modèles utilisés. Ce moteur, ne comportant que huit tiges pour un volume actif d'un litre, atteint un effort électromagnétique de 1000N en fonctionnement statique. Des abaques permettent d'estimer simplement les performances optimales d'actionneurs multi-tiges sous diverses contraintes mécaniques.

Une idée centrale en ingénierie des systèmes est de construire les systèmes complexes par assemblage de composants. Chaque composant a ses propres caractéristiques, suivant différents points de vue, chacun mettant en évidence différentes dimensions d'un système. Un problème central est de définir le sens la composition de composants hétérogènes afin d'assurer leur interopérabilité correcte. Une source fondamentale d'hétérogénéité est la composition de sous-systèmes qui ont des différentes sémantiques d'execution et d' interaction. À un extrême du spectre sémantique on trouve des composants parfaitement synchronisés par une horloge globale, qui interagissent par transactions atomiques. À l'autre extrême, on a des composants complètement asynchrones, qui s'éxécutent à des vitesses indépendantes et interagissent nonatomiquement. Entre ces deux extrêmes, il existe une variété de modèles intermédiaires (par exemple, les modèles globalement asynchrones et localement synchrones). Dans ce travail, on étudie la combinaison des systèmes synchrones et asynchrones. A ce fin, on utilise BIP (Behavior-Interaction-Priority), un cadre général à base de composants permettant la conception rigoureuse de systémes. On définit une extension de BIP, appelée BIP synchrone, déstiné à modéliser les systèmes flot de données synchrones. Les pas d'éxécution sont décrites par des réseaux de Petri acycliquemunis de données et des priorités. Ces réseaux de Petri sont utilisés pour modéliser des flux concurrents de calcul. Les priorités permettent d'assurer la terminaison de chaque pas d'éxécution. Nous étudions une classe des systèmes synchrones ''well-triggered'' qui sont sans blocage par construction et le calcul de chaque pas est confluent. Dans cette classe, le comportement des composants est modélisé par des 'graphes de flux modaux''. Ce sont des graphes acycliques représentant trois différents types de dépendances entre deux événements p et q: forte dépendance (p doit suivre q), dépendance faible (p peut suivre q) et dépendance conditionnelle (si p et q se produisent alors $p$ doit suivre q). On propose une transformation de modèles LUSTRE et MATLAB/Simulink discret à temps discret vers des systèmes synchrones ''well-triggered''. Ces transformations sont modulaires et explicitent les connexions entre composants sous forme de flux de données ainsi que leur synchronisation en utilisant des horloges. Cela permet d'intégrer des modèles synchrones dans les modèles BIP hétérogènes. On peut ensuite utiliser la validation et l'implantation automatique déjà disponible pour BIP. Ces deux traductions sont actuellement implementées et des résultats expérimentaux sont fournis. Pour les modèles BIP synchrones nous parvenons à générer du code efficace. Nous proposons deux méthodes: une implémentation séquentielle et une implémentation distribués. L'implémentation séquentielle consiste en une boucle infinie. L'implémentation distribuée transforme les graphes de flux modaux vers une classe particulieére de réseaux de Petri, que l'on peut transformer en réseaux de processus de Kahn. Enfin, on étudie la théorie de la conception de modeéles insensibles à la latence (latency-insensitive design, LID) qui traite le problème de latence des interconnexionsdans les systèmes synchrones. En utilisant la conception LID, les systèmes synchrones peuvent être "désynchronisés" en des réseaux de processus synchrones qui peuvent fonctionner à plus haute fréquence. Nous proposons un modèle permettant de construire des modéles insensibles à la latence en BIP synchrone, en représentant les mécanismes spécifiques d'interconnexion par des composants BIP synchrone.