Direction de recherche : Béatrice BÉRARD

Co-encadrement : DUTHEILLET Claude & THIERRY-MIEG Yann

Conception semi-automatique de contrôleurs avec VeriJ

Lorsqu'un système ouvert ne respecte pas une spécification, notamment concernant la sûreté de fonctionnement, une solution possible consiste à restreindre le système avec un contrôleur pour atteindre l'objectif, lorsque cela est possible. Deux approches sont utilisées pour construire un tel contrôleur. La première, qui consiste en un processus manuel où un expert définit un contrôleur, est sujette à erreurs. La seconde repose sur des méthodes formelles et synthétise automatiquement un contrôleur correct, s'il en existe un. Cependant, les outils de synthèse existants résolvent principalement le problème pour des systèmes décrits dans des formalismes de bas niveau, qui présentent un investissement conséquent en apprentissage pour les ingénieurs du logiciel. De plus, la synthèse automatique ne passe pas bien à l'échelle pour des grands systèmes. Enfin, le contrôleur généré automatiquement est généralement très grand, ce qui rend son interprétation difficile, et il ne peut pas être adapté aisément lorsque des paramètres du système sont modifiés.
Afin de favoriser l'adoption de la théorie du contrôle dans les processus industriels, nous définissons un nouveau langage de programmation appelé VeriJ, sous la forme d'un sous-ensemble de Java auquel sont ajoutées des constructions supplémentaires dédiées à la supervision. Nous fournissons avec VeriJ un outil, basé sur la transformation de modèles, qui prend en entrée un programme VeriJ et produit un système de transitions étiqueté (LTS), représentant la sémantique du programme. Un moteur pour ce système de transitions est intégré dans l'outil afin de permettre le test de contrôlabilité et la synthèse de contrôleur pour des programmes VeriJ. Ceci réduit donc le fossé entre les programmes de type Java et la synthèse formelle de contrôleurs.
Nous proposons de combiner la synthèse automatique avec une conception centrée sur l'utilisateur en définissant une approche itérative, incrémentale et semi-automatique pour la conception de contrôleur. Dans ce processus, les utilisateurs peuvent modéliser, simuler et exécuter un système (incluant éventuellement un contrôle partiel), dans un environnement de développement Java. L'outil de synthèse fournit aux utilisateurs des diagnostiques sur le programme courant et peut générer des contrôleurs en VeriJ, lorsque cela est possible. Cette approche évite partiellement les problèmes de passage à l'échelle et de lisibilité des contrôleurs générés. L'illustration d'un tel processus sur un exemple significatif, provenant des systèmes de transport automatisés, montre qu'il est possible de combiner: i) les bénéfices résultant des environnements de développement évolués pour Java, avec ii) des performances comparables à celles des outils existants.
Pour pallier le problème d'explosion combinatoire de l'espace d'états, nous intégrons également un module de contrôle à un outil symbolique efficace (ITS/SDD) utilisant une variante de diagrammes de décision, les Set Decision Diagrams. Ceci permet de vérifier la contrôlabilité de systèmes modélisés par des réseaux de Petri (temporels) et une perspective importante de ce travail est d'utiliser ce travail pour améliorer les performances de VeriJ.

Publications 2010-2022