Retour à la page d'accueil de l'action TOLÈRE
INRIA Rhône-Alpes, le 9 mars 2000
L'objectif de la réunion était de mieux connaître les techniques et outils de synthèse de contrôleurs discrets ou hybrides, tels qu'élaborés à VÉRIMAG et à l'INRIA-Rennes. Il s'agit pour le projet BIP de considérer leur applicabilité dans le cadre de systèmes de contrôle/commande, où le LAG a une expérience. Notre domaine d'application est plus particulièrement ciblé sur les systèmes robotiques, et notamment (mais pas seulement) en lien avec l'environnement de programmation ORCCAD.
La réunion a consisté en :
un double séminaire ouvert (dans l'amphi de l'UR, annoncé dans l'UR, sur Grenoble et dans les News) donné par Hervé Marchand (INRIA-Rennes) et Thao Dang (VÉRIMAG),
une réunion de discussion, dont les participants sont indiqués ci-après,
un séjour de deux jours et demi de Hervé Marchand.
Titres et résumés :
Hervé Marchand (IRISA/INRIA, Rennes) :
Synthèse de contrôleurs discrets dans l'environnement SIGNAL
Le langage SIGNAL est destiné à la conception et à la mise en oeuvre sure de systèmes réactifs temps réels. Certains domaines d'application exigent une grande fiabilité et de la sûreté de fonctionnement. Traditionnellement, ces exigences sont vérifiées a posteriori par des techniques de simulation et de vérification de propriétés. Le problème de la synthèse de contrôleur sur des systèmes à événements discrets est dual. Il consiste, à partir d'une spécification du système et d'un ensemble de propriétés attendues de celui-ci, à dériver/synthétiser un contrôleur qui, une fois placé dans son environnement, va contraindre le comportement du système de manière à garantir l'ensemble des propriétés.
Dans notre approche, la théorie du contrôle repose sur une représentation équationnelle de la partie logique d'un programme SIGNAL sous la forme d'un système dynamique polynômial dans Z/3Z. Nous montrerons comment à partir d'un tel système, il est possible de synthétiser un contrôleur de manière à ce que le système contrôlé vérifie a posteriori un objectif de commande logique. Nous présenterons également une théorie de la commande optimale, permettant de synthétiser des contrôleurs traduisant un critère qualitatif et non plus seulement logique. Finalement, nous présenterons, à travers un exemple, l'intégration de ces techniques dans l'environnement de programmation SIGNAL, à travers la description d'un prototype pour la conception d'automatismes et de logiciel sûrs les implémentant.
Thao Dang (VÉRIMAG, Grenoble) :
Systèmes hybrides : vérification et synthèse de contrôleurs
Dans la première partie nous présentons une méthode d'analyse d'atteignabilité des systèmes dynamiques définis par des équations différentielles linéaires. Cette méthode est basée sur un algorithme numérique qui approxime itérativement l'ensemble des états atteignables. Un avantage de cet algorithme est que l'accumulation d'erreur est significativement réduite par rapport à d'autres approches. Cela nous permet de traiter des systèmes dynamiques non-triviaux, des systèmes hybrides et des inclusions différentielles.
Dans la deuxième partie nous présentons une nouvelle méthodologie pour la synthèse automatique de contrôleurs par commutation (switching controllers) pour des systèmes hybrides. Notre but est de trouver des conditions pour lesquelles un contrôleur doit faire passer le système d'un mode de fonctionnement à un autre afin d'éviter certains mauvais états. Nous proposons un algorithme de synthèse basé sur le calcul des états atteignables et l'illustrons ensuite a travers quelques exemples.
Cette réunion a commencé, avant le séminaire, par l'exposé des activités du projet BIP et des utilisations envisagées de la synthèse, et s'est poursuivie après le séminaire, par une discussion sur ce qui pouvait être envisagé dans un futur proche.
Daniel Simon a fait un exposé sur les activités liées à la programmation de systèmes de contrôle/commande, autour d'ORCCAD. Il s'agit des aspects continus (de détermination et de programmation de la commande) comme discrets, avec détail des structures de tâches-commandes et de procédure, avec les événements qui y interviennent.
Eric Rutten a esquissé quelques utilisations possibles de la synthèse dans ce cadre, en mettant en évidence des événements et propriétés potentiellement utiles. L'intervention de la synthèse peut être envisagée à différents niveaux :
la gestion du comportement au niveau de la mission, par génération de procédures-commandes, avec des objectifs d'états à atteindre, ou par lesquels passer,
une forme de téléopération sûre, où une partie du comportement discret d'une application est gérée automatiquement par un contrôleur, le reste des possibilités étant laissé libre au choix de l'utilisateur, de manière interactive,
la gestion de modes de calcul d'une même tâche-commande, faisant commuter la mise en oeuvre de la commande en fonction de critères de performance ou de qualité, en introduisant éventuellement une notion de modes dégradés.
Bernard Espiau a décrit des sujets d'intérêt du projet BIP distincts d'ORCCAD, et présentant un caractère hybride potentiellement intéressant pour l'approche de VÉRIMAG, notamment le contrôle d'un double pendule.
En conclusion, il a été convenu que :
Eric Rutten et Hervé Marchand poursuivraient les points entamés lors de cette visite (voir plus loin)
Alain Girault, Eric Rutten et Oded Maler
Eric Rutten et Hassane Alla examineraient l'application des techniques du LAG (supervision et contrôle, forçage d'événements) au cas de tâches-commandes ; on pourrait organiser un exposé de Hassane Alla à l'INRIA Rhône-Alpes,
Bernard Espiau enverrait un document à Oded Maler concernant le double pendule.
Hervé Marchand de l'INRIA-Rennes, projet EP-ATR, est venu les 8, 9 et 10 mars 2000 montrer l'environnement de synthèse de contrôleurs discrets SIGNALI/SIGNAL. SIGALI est un outil de calcul formel de type model-checking, qui manipule des systèmes de transitions représentés par des fonctions polynômiales. Il comprend des fonctionnalités de synthèse de contrôleurs discrets élaborées au cours des dernières années. Un de ses intérêts particuliers est son intégration à l'environnement SIGNAL pour la simulation et l'exécution des contrôleurs synthétisés.
Eric Rutten et Hervé Marchand ont travaillé à :
des démos de l'environnement SIGALI/SIGNAL (les deux sont installés sur le compte de Eric Rutten)
une ébauche d'exemple « très petit », dans un but pédagogique, qui comprendrait un espace d'états tel qu'on puisse le représenter graphiquement (par exemple 16 états donc 4 variables d'état), ainsi que son évolution au cours du processus de synthèse progressive d'un contrôleur.
une réflexion sur :
Envoyez vos commentaires à Alain Girault à Alain.Girault@inrialpes.fr.
Dernière modification : 16 mars 2000