Contributions les plus significatives à la recherche

Algorithmes de synthèse de contrôleurs

J'ai développé avec mes collègues plusieurs algorithmes de synthèse de contrôleurs. Le premier algorithme est une amélioration de l'algorithme de synthèse de contrôleurs avec observation partielle proposé par Cieslak et al [IEEE Transactions on Automatic Control 40 (4)]. Le second algorithme est pertinent pour la synthèse de contrôleurs avec observation totale. Il inclut une stratégie de recherche basée sur un mécanisme ingénieux de retour arrière et ne requiert pas le modèle global du comportement libre du système [Journal of Algorithms 25 (1)]. Le troisième algorithme permet une meilleure compréhension de la relation entre des techniques du domaine de la théorie du contrôle et celles du domaine de l'intelligence artificielle. Ce travail constitue une avancée significative par rapport aux méthodes introduites dans le cadre théorique du contrôle des systèmes discrets développé initialement par Ramadge et Wonham. Cet algorithme est le premier qui intègre le traitement des propriétés de sûreté, de vivacité et de temps réel d'une manière uniforme en utilisant une logique temporelle [IEEE Transactions on Automatic Control 43 (11)].

Contrôle de systèmes à événements discrets paramétrés

Les algorithmes de synthèse de contrôleurs proposés dans la littérature scientifique comporte de sérieux désavantages lorsqu'ils sont appliqués sur des systèmes industriels, particulièrement sur des systèmes paramétrés (par ex. des réseaux de processus similaires). Deux de ces désavantages sont liés à l'extensibilité et à la complexité de calcul. Pour résoudre ces problèmes, j'ai proposé des méthodes de synthèse de contrôleurs qui intègrent des techniques d'abstraction dans des procédures de synthèse : une développée avec mon collègue Barbeau (maintenant à l'université de Carleton) et un étudiant au doctorat qui exploite les réseaux de Petri colorés et des spécifications de symétries [Discrete Event Dynamic Systems: Theory and Applications 9 (2)], et une autre qui est orientée vers le calcul de contrôleurs attribués à partie de modèles abstraits à la place d'un modèle concret [Journal of Systems and Software 60 (2)]. Cette dernière méthode requiert des transformations pour la réduction et la fusion. Afin que les transformations soient valides, elles doivent être bien fondées et exactes. Avec mon collègue Frappier, nous avons proposé des transformations exactes [LNCS 2178]. Obtenir des transformations bien fondées est un problème beaucoup plus difficile. Il n'a pas été résolu dans le cas général. Néanmoins, avec mon collègue Desharnais de l'Université Laval et un étudiant au doctorat, nous avons proposé des solutions pour les systèmes paramétrés à données bornées (MRS'2003) et pour des boucles de commande à rétroaction dérivées à partir de politiques de contrôle sur les états aussi bien dans le cas de l'observation totale [LNCS 3299] que dans le cas de l'observation partielle [CDC-ECC'05]. Basé sur ces derniers travaux, nous avons réalisé une étude plus approfondie sur le contrôle de systèmes à événements discrets paramétrés avec interconnexions des processus. Le résultat de cette recherche est une théorie complète sur le sujet [Discrete Event Dynamic Systems: Theory and Applications 19 (2)]. Durant la même période, nous avons examiné des procédures à base d'heuristiques afin de dériver des contrôleurs non bloquants [IECON'09].

Contrôle par délégation pour la composition de composants logiciels dynamiques

Dans le contrôle de systèmes à événements discrets, le contrôle est un contrôle par inhibition/permission. Un autre type de contrôle est possible, celui par délégation qui est à la base d'une théorie de composition de composants logiciels dynamiques, comme des agents. Avec un étudiant au doctorat, j'ai formulé un nouveau problème de formation d'une équipe d'agents. Les agents sont munis d'un comportement et leurs tâches ont des attributs avec des valeurs spécifiques. Le but est également un comportement avec des tâches, mais les valeurs de leurs attributs s'expriment comme des préférences. Le problème consiste à former une équipe robuste d'agents, sous la forme de compositions « agents-contrôleur » qui permettent de réaliser le but à moindre coût [LNAI 10413].

Une vue systémique pour le développement à base de composants logiciels

De nos jours, le développement à base de composants logiciels est un sujet de recherche très fertile principalement parce que les systèmes sont de plus en plus complexes et coûteux à développer. J'ai examiné avec un étudiant au doctorat, le développement à base de composants logiciels dans la perspective de la théorie des systèmes avec comme intention de synthétiser des observateurs (interfaces de composants) et des superviseurs (contrôleurs de composants). En plus, nous avons montré, à partir de trois opérateurs atomiques, comment ajouter du contrôle à un composant et comment assembler horizontalement et verticalement des composants réutilisables tout en maintenant des invariants requis par la théorie. Selon le meilleur de nos connaissances, c'est la première fois qu'une telle méthode formelle est utilisée pour résoudre des problèmes de contrôle dans le contexte du développement à base de composants logiciels, incluant la réutilisation. Premièrement, nous avons illustré notre approche à l'aide d'un système en ligne organisé hiérarchiquement à partir de services Web [LNCS 6921]. Deuxièmement, basé sur ces résultats, cette méthode extensible a été améliorée afin d'inclure un mécanisme d'instanciation et une dynamique abstraite dans le but de générer automatiquement du code pour des automates programmables comme ceux que l'on retrouve dans l'industrie [IEEE Transactions on Control Systems Technology]. Cette méthode a été appliquée avec succès dans la création d'une librairie de composants réutilisables et le contrôle d'une usine de production modulaire disponible dans notre laboratoire et semblable à celles rencontrées dans l'industrie. Cette usine comporte 44 composants et son espace d'états est estimé à 10³¹ états.

Exploration et application de la théorie du contrôle supervisé par une approche de satisfaisabilité de contraintes

La majorité des outils développés comme support à la théorie du contrôle des systèmes à événements discrets intègrent des diagrammes de décision binaire (BDD) à des algorithmes de calcul de points fixes afin de manipuler des modèles comportant d'immenses espaces d'états. Une autre technique de représentation symbolique associée à des outils de satisfaction de contraintes booléennes et principalement utilisée par des vérificateurs de modèles bornés est moins répandu. Notre équipe de recherche a formulé, d'une manière déclarative en Alloy, des modèles abstraits de plusieurs variantes de la théorie du contrôle des systèmes à événements discrets dans le but de démontrer la faisabilité de cette technique. Ce travail est original puisqu'il aide les débutants à développer une meilleure intuition de cette théorie, à explorer les modèles abstraits à partir de leurs propres instances pour obtenir des solutions à des problèmes de contrôle pratiques et ultimement à étendre la théorie. Puisque nos spécifications Alloy ont approximativement la même taille que les formulations mathématiques des variantes, effectuer du prototypage et appliquer une théorie de cette façon constitue une source de motivation et de créativité pour identifier de nouveaux problèmes et les résoudre. Premièrement, nous avons défini un modèle d'une théorie de contrôle hiérarchique dans le but d'obtenir des observateurs et des superviseurs de petits composants réutilisables. Parmi les 44 composants d'une usine de production modulaire, 75% d'entre eux ont été vérifiés avec succès par l'analyseur de Alloy [LNCS 6959]. Nous avons pu atteindre un tel niveau d'extensibilité avec Alloy en tirant avantage de cette théorie. Nous avons également été les premiers à proposer une solution Kodkod pour le calcul d'éléments suprémaux (de familles de langages ou de prédicats) [LNCS 7316]. Nous avons complètement reformulé la théorie du contrôle à base d'états dans un modèle Alloy et progressivement enrichi ce modèle par rapport à différentes extensions : observation partielle, structures en arborescence d'états et systèmes paramétrés [Science of Computer Programming 94 (2)]. Enfin, le modèle Alloy a été intégré dans un programme αRby. Le langage de programmation αRby, qui est une fusion de Alloy et Ruby, est assisté d'un engin de satisfaisabilité de formules logiques. Cette solution permet de résoudre des problèmes de contrôle plus aisément qu'en Alloy/Kodkod et tout simplement impossible en Alloy pur [International Journal on Sofware Tools for Technology Transfer]. Une comparaison de trois langages de programmation, incluant αRby, permet d'envisager d'autres paradigmes de programmation pour atteindre cet objectif [Journal of Computer Languages].

Sécurité fonctionnelle dans les systèmes d'information WEB

Dans un projet conjoint avec le Laboratoire d'algorithme, logique et complexité de l'Université Paris-Est, nous avons élaboré un cadre pour le développement de systèmes d'information Web fiables et sécures. Tout d'abord, basé sur la norme XACML de l'organisation OASIS, nous avons élaboré un méta modèle pour la conception de gestionnaires de politiques de contrôle d'accès [LNCS 6888]. Ensuite, nous avons proposé des solutions pour un noyau de sécurité conforme à l'architecture de l'OMG (architecture dirigée par des modèles). Les politiques de sécurité sont exprimées en EB³SEC. Ce langage est une extension de EB³, une méthode de spécification boîtes noires d'entités initialement développée avec mon collègue Frappier [Software and Systems Modeling 2 (2)], ou ASTD [Innovations in Systems and Software Engineering 4 (3)], une notation graphique des expressions de processus EB³. Les implémentations de politiques de sécurité sont correctes par construction puisque les spécifications formelles ASTD sont traduites en processus BPEL [International Journal of Systems and Service-Oriented Engineering 2 (2)] ou interprétées par des processus BPEL.

Synthèse de plans et synthèse de contrôleurs

L'expérience réalisée par un candidat au doctorat, supervisé conjointement avec mon collègue Kabanza, et effectué en collaboration avec la professeure Thiébaux du Australian National Laboratory [Electronic Notes in Theoretical Computer Science 149 (2)], est basée sur un travail de recherche antérieur qui établit une meilleure compréhension des liens entre les techniques du domaine de la théorie du contrôle et celles de la planification. Ce travail de recherche, mené avec Barbeau (de l'université de Carleton) et mon collègue Kabanza met en évidence une méthode qui étend l'approche traditionnelle de planification par chaînage avant dans le but de calculer des plans réactifs, lesquels sont des machines à états qui comportent des cycles et des événements incontrôlables. De tels plans sont plus appropriés pour les agents réactifs que les plans conventionnels [Artificial Intelligence 95 (1)]. Ce travail, qui est une suite de celui décrit dans un article de conférence (IJCAI'1995), est encore cité de nos jours. D'autres liens entre les techniques du domaine de la théorie du contrôle et celles de la composition d'agents basées sur une forme particulière de planification ont également été établis [SMC 2015].